Path: ...!news.misty.com!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: Nakano Proposition 2 in SWI-Prolog (Was: How to make cyclic
 terms)
Date: Thu, 9 Jan 2025 13:45:24 +0100
Message-ID: <vlogd4$21qtd$1@solani.org>
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>
 <vloa2b$2dkpd$12@dont-email.me> <vlof4t$21qd0$1@solani.org>
 <vlofkd$21qfv$1@solani.org> <vlofuo$21qlu$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 9 Jan 2025 12:45:24 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2157485"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101
 Firefox/128.0 SeaMonkey/2.53.20
Cancel-Lock: sha1:rfWJ1MpXvfw3ViNBvPWSfdI27tk=
X-User-ID: eJwFwYEBADAEA7CbjOqcg/H/CUugLt40hxsWu5Dm1TJeWiQyJzpGRU+wEC8roTo8KWx5ez1Ka/liB8gPUJAV3w==
In-Reply-To: <vlofuo$21qlu$1@solani.org>
Bytes: 4870
Lines: 139


In Nakano's paper the congruence relation leads
to a cyclic type for the given recursive type C:

C ≌ C -> A

Since in definition 11 of ≌, the paper has an
expansion rule for recursive types:

μX.A ≌ A[μX.A/X]

So if the recursive type is:

C = μX.(X -> A)

I am allowed to form:

(X -> A)[C/X] = C -> A

And hence derive:

C ≌ C -> A

LoL

Mild Shock schrieb:
> Hi,
> 
> In SWI-Prolog, the example doesn't need System F
> or Nakano Recursive Types. It simply works with
> the congruence relation itself,
> 
> if you want to bar that the Curry Paradox emerges,
> you have to replace the de Bruijn Variable clause,
> by an unify_with_occurs_check/2 based rule:
> 
> /* de Bruijn Variable */
> typeof(N, L, A) :- integer(N),
>     nth0(N, L, B),
>     unify_with_occurs_check(A, B).
> 
> Now the program uses another congruence relation
> among Prolog terms. And the example doesn't work anymore.
> Now already the self application fails:
> 
> ?- typeof(lam(0*0), [], A).
> false.
> 
> Needless to say that subsequently the Curry
> Paradox fails as well:
> 
> ?- typeof(lam(0*0)*lam(0*0), [], A).
> false.
> 
> Bye
> 
> P.S.: What are de Bruijn indexes:
> 
> In mathematical logic, the de Bruijn index is a tool
> invented by the Dutch mathematician Nicolaas Govert
> de Bruijn for representing terms of lambda calculus
> without naming the bound variables.
> https://en.wikipedia.org/wiki/De_Bruijn_index
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Or in SWI-Prolog:
>>
>> /* de Bruijn Variable */
>> typeof(N, L, A) :- integer(N),
>>     nth0(N, L, A).
>> /* de Bruijn abstraction */
>> typeof(lam(S), L, A -> B) :-
>>     typeof(S, [A|L], B).
>> /* Modus Ponens */
>> typeof((S*T), L, B) :-
>>     typeof(S, L, (A -> B)),
>>     typeof(T, L, A).
>>
>> ?- typeof(lam(0*0), [], A).
>> A = (_S1->_A), % where
>>      _S1 = (_S1->_A).
>>
>> ?- typeof(lam(0*0)*lam(0*0), [], A).
>> true.
>>
>> The last query gives simply true without A constrained.
>> You could also try this here instantiating A, and
>> you will see it works for any A:
>>
>> ?- typeof(lam(0*0)*lam(0*0), [], a).
>> true.
>>
>> ?- typeof(lam(0*0)*lam(0*0), [], (a->b)).
>> true.
>>
>> ?- typeof(lam(0*0)*lam(0*0), [], (b->a)).
>> true.
>>
>> Bye
>>
>> Mild Shock schrieb:
>>>
>>> See here:
>>>
>>> A Modality for Recursion
>>> Hiroshi Nakano - 2000 - Zitiert von: 237
>>> https://www602.math.ryukoku.ac.jp/~nakano/papers/modality-lics00.pdf
>>>
>>> Even if you disband cyclic terms in your
>>> model, like if you adhere to a strict Herband model.
>>> If the Herband model has an equality which is a
>>>
>>> congruence relation ≌. Nakano's paper contains
>>> an inference rule for a congruence relation ≌.
>>> When you have such a congruence relation, you can
>>>
>>> of course derive things like for example for a certain
>>> exotic recursive type C, that the following holds:
>>>
>>> C ≌ C -> A
>>>
>>> You can then produce the Curry Paradox in simple
>>> types with congruence. And then ultimately derive:
>>>
>>> |- (λx.x x)(λx.x x): A
>>>
>>> As in Proposition 2 of Nakano's paper.
>>>
>>> Julio Di Egidio schrieb:
>>>>> (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.)
>>>
>>
>