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: A miraculous match? (Was: Honoring Raymond Smullyan)
Date: Thu, 9 Jan 2025 11:52:11 +0100
Organization: A noiseless patient Spider
Lines: 105
Message-ID: <vlo9os$2dkpd$11@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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 09 Jan 2025 11:52:13 +0100 (CET)
Injection-Info: dont-email.me; posting-host="e9d42356b81d42d02d68289eca9ecab3";
	logging-data="2544429"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1++q/H7fzUGPkE0LS1hGDfQceLwQLrti10="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:imrUA72bw1Zeak0LC/2WaZdutHU=
In-Reply-To: <vlme6h$2dkpc$3@dont-email.me>
Content-Language: en-GB
Bytes: 4478

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

-Julio