Nakano Proposition 2 in SWI-Prolog (Was: How to make cyclic terms)

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