Re: Honoring Raymond Smullyan

Julio wrote:
 > Why do you care so much about simply-typed?
What makes you think I care about simply-typed?
It was part of the MSE question you moron:
 > I'm having trouble understanding the Wikipedia article
 > on Simply typed lambda calculus.
 >
 > 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.
https://math.stackexchange.com/q/1927260/1482376
It explicitly says Simply typed lambda calculus.
I verbatim posted this question in the thread here.
Whats wrong with you moron?
Can't you stay on topic?
Bye
Julio Di Egidio schrieb:

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...
 -Julio