On 08/01/2025 18:55, Julio Di Egidio wrote:
On 08/01/2025 18:45, Julio Di Egidio wrote:
On 08/01/2025 10:31, Mild Shock wrote:
Julio Di Egidio schrieb:
On 08/01/2025 01:10, Mild Shock wrote:
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8
Define Smullyan.
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Let `F : forall (X Y : Type), X -> Y`, then we can
(almost) write `F F`. Simple seems simple, it just
doesn't end well:
```coq
(** There exists a function
from any type to any type! *)
Axiom F : forall (X Y : Type), X -> Y.
(** Any two types: might be False False if
that's all there is, an uninhabited type. *)
Parameters (T U : Type).
(** Now we can prove False. *)
Definition absurd : False :=
F (T -> U) False (F T U).
```
Thats System F and not simple types. also
known as the polymorphic lambda-calculus
or second-order lambda-calculus, it is an
extension of simply typed lambda-calculus.
It's as simple as a mocking bird... :)
Why do you care so much about simply-typed? If not as a foundation
for the theory of functional languages: yet xx is an object of
interest in its own right, simply beyond the simply-typed.
But in simple types itself, th self application
x x has no type. You can try yourself:
/* Typed Variable */
typeof(_:A, B) :-
unify_with_occurs_check(A, B).
/* Modus Ponens */
typeof((S*T), B) :-
typeof(S, (A -> B)),
typeof(T, A).
And then the query:
?- X=_:_, typeof((X*X), T).
false.
The query will though succeed if you remove
the occurs check.
Which is more interesting: what it is, not what it is not.
With plain unification (on SWI):
```
?- X=_:_, typeof((X*X), T).
X = _:_S1, % where
_S1 = (_S1->T).
```
That is also somewhat reminiscent of Coq's result, except that here
the type is a ground and cyclic term (a "cyclic type"?), as such not
even polymorphic... Nor, OTOH, can I think of a way to construct a
cyclic term in Coq.
Correction: it's not really ground since T isn't...
Anyway, looking back at the Coq term for `absurd`, i.e. `F (T -> U)
False (F T U)`, unifying the parameter `U` with `False` would be no
prob, and unifying `T` with `T->U` would give the exact same cyclic term
as `_S1` above.
A miraculous match? A significant one?
(But I still wouldn't know how to create a cyclic term proper in Coq or
in fact in any total functional language, despite the mechanism
underlying conversion/definitional equality is logical unification, and
we can even somewhat access it in Coq, via the definition of `eq`/reflexivity.)
On 08/01/2025 18:45, Julio Di Egidio wrote:
On 08/01/2025 10:31, Mild Shock wrote:
Julio Di Egidio schrieb:
On 08/01/2025 01:10, Mild Shock wrote:
Hi,
Now you can listen to Bird songs for a minute:
2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8
Define Smullyan.
A little quiz:
Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
A: Hardly, because xx has no simple type.
Right?
Let `F : forall (X Y : Type), X -> Y`, then we can
(almost) write `F F`. Simple seems simple, it just
doesn't end well:
```coq
(** There exists a function
from any type to any type! *)
Axiom F : forall (X Y : Type), X -> Y.
(** Any two types: might be False False if
that's all there is, an uninhabited type. *)
Parameters (T U : Type).
(** Now we can prove False. *)
Definition absurd : False :=
F (T -> U) False (F T U).
```
Thats System F and not simple types. also
known as the polymorphic lambda-calculus
or second-order lambda-calculus, it is an
extension of simply typed lambda-calculus.
It's as simple as a mocking bird... :)
Why do you care so much about simply-typed? If not as a foundation
for the theory of functional languages: yet xx is an object of
interest in its own right, simply beyond the simply-typed.
But in simple types itself, th self application
x x has no type. You can try yourself:
/* Typed Variable */
typeof(_:A, B) :-
unify_with_occurs_check(A, B).
/* Modus Ponens */
typeof((S*T), B) :-
typeof(S, (A -> B)),
typeof(T, A).
And then the query:
?- X=_:_, typeof((X*X), T).
false.
The query will though succeed if you remove
the occurs check.
Which is more interesting: what it is, not what it is not.
With plain unification (on SWI):
```
?- X=_:_, typeof((X*X), T).
X = _:_S1, % where
_S1 = (_S1->T).
```
That is also somewhat reminiscent of Coq's result, except that here
the type is a ground and cyclic term (a "cyclic type"?), as such not
even polymorphic... Nor, OTOH, can I think of a way to construct a
cyclic term in Coq.
Correction: it's not really ground since T isn't...
(But I still wouldn't know how to create a cyclic term proper in Coq
or in fact in any total functional language, despite the mechanism
underlying conversion/definitional equality is logical unification,
and we can even somewhat access it in Coq, via the definition of
`eq`/reflexivity.)
Julio Di Egidio schrieb:
(But I still wouldn't know how to create a cyclic term proper in Coq
or in fact in any total functional language, despite the mechanism
underlying conversion/definitional equality is logical unification,
and we can even somewhat access it in Coq, via the definition of
`eq`/reflexivity.)
See here:
A Modality for Recursion
Hiroshi Nakano - 2000 - Zitiert von: 237 https://www602.math.ryukoku.ac.jp/~nakano/papers/modality-lics00.pdf
Even if you disband cyclic terms in your
model, like if you adhere to a strict Herband model.
If the Herband model has an equality which is a
congruence relation ≌. Nakano's paper contains
an inference rule for a congruence relation ≌.
When you have such a congruence relation, you can
of course derive things like for example for a certain
exotic recursive type C, that the following holds:
C ≌ C -> A
You can then produce the Curry Paradox in simple
types with congruence. And then ultimately derive:
|- (λx.x x)(λx.x x): A
As in Proposition 2 of Nakano's paper.
Hi,
are you saying that System F is inconsistent?
I didn't say anything about System F.
All the Prolog examples I posted were simple types.
Whats wrong with you? Can you point anything
I said originally about System F?
Otherwise you can read yourself about System F
I am not baby sitting on System F.
Bye
Julio Di Egidio schrieb:
On 09/01/2025 13:23, Mild Shock wrote:
Julio Di Egidio schrieb:
(But I still wouldn't know how to create a cyclic term proper in
Coq or in fact in any total functional language, despite the
mechanism underlying conversion/definitional equality is logical
unification, and we can even somewhat access it in Coq, via the
definition of `eq`/reflexivity.)
See here:
A Modality for Recursion
Hiroshi Nakano - 2000 - Zitiert von: 237
https://www602.math.ryukoku.ac.jp/~nakano/papers/modality-lics00.pdf
Even if you disband cyclic terms in your
model, like if you adhere to a strict Herband model.
If the Herband model has an equality which is a
congruence relation ≌. Nakano's paper contains
an inference rule for a congruence relation ≌.
When you have such a congruence relation, you can
of course derive things like for example for a certain
exotic recursive type C, that the following holds:
C ≌ C -> A
You can then produce the Curry Paradox in simple
types with congruence. And then ultimately derive:
|- (λx.x x)(λx.x x): A
As in Proposition 2 of Nakano's paper.
Besides that I can now say for sure that there is no such thing as a
(first-class) cyclic term in Coq (*), or in any total functional
language I'd surmise, you have copiously posted and belaboured on what
I had already derived, and have not actually answered the question:
Can you read at all? -- No, seriously, the question is: are you saying
that System F is inconsistent? As that's what my (formally verified)
proof derives from that axiom F.
(*) <https://proofassistants.stackexchange.com/questions/4612>
-Julio
Hi,
I told you a dozen times that the scope of
this thread is simple types. Why don't you
open a separate thread for your fetish
System T and/or Coq. I really don't care
about System T. You can play online with
System T here:
https://crypto.stanford.edu/~blynn/lambda/systemf.html
Bye
are you saying that System F is inconsistent?
On 09/01/2025 13:23, Mild Shock wrote:
Julio Di Egidio schrieb:
(But I still wouldn't know how to create a cyclic term proper in Coq
or in fact in any total functional language, despite the mechanism
underlying conversion/definitional equality is logical unification,
and we can even somewhat access it in Coq, via the definition of
`eq`/reflexivity.)
See here:
A Modality for Recursion
Hiroshi Nakano - 2000 - Zitiert von: 237
https://www602.math.ryukoku.ac.jp/~nakano/papers/modality-lics00.pdf
Even if you disband cyclic terms in your
model, like if you adhere to a strict Herband model.
If the Herband model has an equality which is a
congruence relation ≌. Nakano's paper contains
an inference rule for a congruence relation ≌.
When you have such a congruence relation, you can
of course derive things like for example for a certain
exotic recursive type C, that the following holds:
C ≌ C -> A
You can then produce the Curry Paradox in simple
types with congruence. And then ultimately derive:
|- (λx.x x)(λx.x x): A
As in Proposition 2 of Nakano's paper.
Besides that I can now say for sure that there is no such thing as a (first-class) cyclic term in Coq (*), or in any total functional
language I'd surmise, you have copiously posted and belaboured on what I
had already derived, and have not actually answered the question:
Can you read at all? -- No, seriously, the question is: are you saying
that System F is inconsistent? As that's what my (formally verified)
proof derives from that axiom F.
(*) <https://proofassistants.stackexchange.com/questions/4612>
-Julio
I told you a dozen times that the scope of
this thread is simple types.
Corr.: System T ~~> System F
Mild Shock schrieb:
Hi,
I told you a dozen times that the scope of
this thread is simple types. Why don't you
open a separate thread for your fetish
System T and/or Coq. I really don't care
about System T. You can play online with
System T here:
https://crypto.stanford.edu/~blynn/lambda/systemf.html
Bye
On 09/01/2025 17:05, Mild Shock wrote:
I told you a dozen times that the scope of
this thread is simple types.
Define scope and thread.
You are simply a waste of time. (EOD.)
-Julio
Maybe you are so simple minded, that
you don't anderstand that "simple" is
essential in forming the technical term:
"simple types"
We call "simply types" not because we want
to highly that we think they are "simple".
Its simply that "simply types" is a terminology
in its own just like "natural numbers" or
"simgular matrix". This is called compound
term formation:
https://en.wikipedia.org/wiki/Compound_%28linguistics%29
Do you get it now? Or still not getting it?
Mild Shock schrieb:
You are a fucking moron. You can even
not separate a dozen terms. Its relatively
simple to tell the things appart:
- Simple Types ( λ→ )
The simply typed lambda calculus λ→, a form of type theory,
is a typed interpretation of the lambda calculus with only
one type constructor → that builds function types.
https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
- System F
Whereas simply typed lambda calculus has variables
ranging over terms, and binders for them, System F
additionally has variables ranging over types,
https://en.wikipedia.org/wiki/System_F
Whats so difficult for you moron to understand?
Julio Di Egidio schrieb:
On 09/01/2025 17:05, Mild Shock wrote:
I told you a dozen times that the scope of
this thread is simple types.
Define scope and thread.
You are simply a waste of time. (EOD.)
-Julio
You are a fucking moron. You can even
not separate a dozen terms. Its relatively
simple to tell the things appart:
- Simple Types ( λ→ )
The simply typed lambda calculus λ→, a form of type theory,
is a typed interpretation of the lambda calculus with only
one type constructor → that builds function types. https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
- System F
Whereas simply typed lambda calculus has variables
ranging over terms, and binders for them, System F
additionally has variables ranging over types, https://en.wikipedia.org/wiki/System_F
Whats so difficult for you moron to understand?
Julio Di Egidio schrieb:
On 09/01/2025 17:05, Mild Shock wrote:
I told you a dozen times that the scope of
this thread is simple types.
Define scope and thread.
You are simply a waste of time. (EOD.)
-Julio
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 715 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 01:14:45 |
| Calls: | 12,098 |
| Calls today: | 6 |
| Files: | 15,003 |
| Messages: | 6,517,862 |