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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)