Path: ...!3.eu.feeder.erje.net!feeder.erje.net!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:37:44 +0100
Message-ID: <vlofuo$21qlu$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 9 Jan 2025 12:37:44 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2157246"; 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:icQEsnJgdhPZZq6JdYvu2bdL834=
In-Reply-To: <vlofkd$21qfv$1@solani.org>
X-User-ID: eJwFwYEBwAAEA7CXDC3Oweb/E5bA+HDDCToOV2ztlckA+Cln8vS46aJTdMkSs36vPTIFtecwIFTflZ0fQHIU2w==
Bytes: 4312
Lines: 112

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