Re: Honoring Raymond Smullyan

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.