Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: A miraculous match? (Was: Honoring Raymond Smullyan)
Date: Thu, 9 Jan 2025 11:57:14 +0100
Organization: A noiseless patient Spider
Lines: 108
Message-ID: <vloa2b$2dkpd$12@dont-email.me>
References: <vlkfq7$1vh4j$1@solani.org> <vlkrge$2dkpc$1@dont-email.me>
 <vllgli$2039r$1@solani.org> <vlmdk8$2dkpd$6@dont-email.me>
 <vlme6h$2dkpc$3@dont-email.me> <vlo9os$2dkpd$11@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 09 Jan 2025 11:57:15 +0100 (CET)
Injection-Info: dont-email.me; posting-host="e9d42356b81d42d02d68289eca9ecab3";
	logging-data="2544429"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18zSbCoDW30qFOgGQ7VTv2JrtLfX7zzh3U="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:i7R0gd6jG7Fajrau5Raehwz0FS4=
In-Reply-To: <vlo9os$2dkpd$11@dont-email.me>
Content-Language: en-GB
Bytes: 4722

On 09/01/2025 11:52, Julio Di Egidio wrote:
> 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.)

Although maybe a coinductive definition...

-Julio