Hi,
The stanford solution to self application
looks quite different than Julios. Here
is the stanford solution:
\x:forall X.X->X.x[forall X.X->X] x
https://crypto.stanford.edu/~blynn/lambda/systemf.html
And here is Julios solution:
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).
```
Whats the difference between the two solutions?
Lets rewrite Julios solution in System F.
He has a combinator 'F' with this type:
'F' : forall X.forall Y.(X -> Y)
His last statement has an expression:
(F T U) which reduces to a type (T -> U).
His last statement has a further expression:
(F (T -> U) False) which reduces to ((T -> U) -> False
Combining these two expressions, has the type False:
(F (T -> U) False (F T U)) : False
Whats the name of this construction?
Bye
Julio Di Egidio schrieb:
On 09/01/2025 17:07, Mild Shock wrote:
Dear Julio
I told you a dozen times that the scope of
You truly are just a spamming piece of shit.
Indeed now go back to sleep until I post my next one sporadic thing,
then back to spamming your insanely automatic stupid shit all over the
place for a couple of weeks, i.e. just as it's need to make me go away
in disgust.
You fucking piece of retarded shit, I wish you, chat GTP, and the whole fucking corporate nazi-retarded interest that is paying the job an incorporated ass cancer.
*Plonk*
-Julio
my thread is simple types. Why don't you
open a separate thread for your fetish
System F and/or Coq. I really don't care
about System F. You can play online with
System F here:
https://crypto.stanford.edu/~blynn/lambda/systemf.html
Get some Brains!
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)