Welcome to SWI-Prolog (threaded, 64 bits, version 7.6.4)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.

For online help and background, visit http://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).

?- isI(I), isItype(Itype), types([], isa(I, IType)).
I = λ(x, x),
Itype = arr(α, α),
IType = arr(_5812, _5812) 

?- isI(I), isIType(IType), types([], isa(I, IType)).
I = λ(x, x),
IType = arr(α, α) 
?- isI(I), isKType(KType), types([], isa(I, KType)).
false.

?- isΩ(Ω), isIType(IType), types([], isa(Ω, IType)).
Ω = app(λ(x, app(x, x)), λ(x, app(x, x))),
IType = arr(α, α) ;
false.

?- isΩ(Ω), isIType(IType), types(isa(Ω, IType)).
Ω = app(λ(x, app(x, x)), λ(x, app(x, x))),
IType = arr(α, α) ;
false.

?- isω(M), isIType(IType), types(isa(M, IType)).
M = λ(x, app(x, x)),
IType = arr(α, α) ;
false.

?- trace.
true.

[trace]  ?- isω(M), isIType(IType), types(isa(M, IType)).
   Call: (9) isω(_11118) ? 
   Exit: (9) isω(λ(x, app(x, x))) ? 
   Call: (9) isIType(_11122) ? 
   Exit: (9) isIType(arr(α, α)) ? 
   Call: (9) types(isa(λ(x, app(x, x)), arr(α, α))) ? 
   Call: (10) types([], isa(λ(x, app(x, x)), _11596)) ? 
   Call: (11) lists:member(isa(λ(x, app(x, x)), _11596), []) ? 
   Fail: (11) lists:member(isa(λ(x, app(x, x)), _11596), []) ? 
   Redo: (10) types([], isa(λ(x, app(x, x)), _11596)) ? 
   Call: (11) types([isa(x, _11600)], isa(app(x, x), _11602)) ? 
   Call: (12) lists:member(isa(app(x, x), _11602), [isa(x, _11600)]) ? 
   Fail: (12) lists:member(isa(app(x, x), _11602), [isa(x, _11600)]) ? 
   Redo: (11) types([isa(x, _11600)], isa(app(x, x), _11602)) ? 
   Call: (12) types([isa(x, _11600)], isa(x, arr(_11630, _11602))) ? 
   Call: (13) lists:member(isa(x, arr(_11630, _11602)), [isa(x, _11600)]) ? 
   Exit: (13) lists:member(isa(x, arr(_11630, _11602)), [isa(x, arr(_11630, _11602))]) ? 
   Exit: (12) types([isa(x, arr(_11630, _11602))], isa(x, arr(_11630, _11602))) ? 
   Call: (12) types([isa(x, arr(_11630, _11602))], isa(x, _11630)) ? 
   Call: (13) lists:member(isa(x, _11630), [isa(x, arr(_11630, _11602))]) ? 
   Exit: (13) lists:member(isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), _11602), _11602), _11602), _11602), _11602), _11602)), [isa(x, arr(arr(arr(arr(arr(arr(..., ...), _11602), _11602), _11602), _11602), _11602))]) ? n
M = λ(x, app(x, x)),
IType = arr(α, α) 
?- α = arr(α, β).
false.

?- X = arr(X, α).

?- X = f(f(f(f(X)))).

?- true.

?- X = f(f(f(f(X)))).
false.

?- trace.
true.

[trace]  ?- isω(M), isIType(IType), types(isa(M, IType)).
   Call: (9) isω(_16864) ? 
   Exit: (9) isω(λ(x, app(x, x))) ? 
   Call: (9) isIType(_16868) ? 
   Exit: (9) isIType(arr(α, α)) ? 
   Call: (9) types(isa(λ(x, app(x, x)), arr(α, α))) ? 
   Call: (10) types([], isa(λ(x, app(x, x)), arr(α, α))) ? 
   Call: (11) lists:member(isa(λ(x, app(x, x)), arr(α, α)), []) ? 
   Fail: (11) lists:member(isa(λ(x, app(x, x)), arr(α, α)), []) ? 
   Redo: (10) types([], isa(λ(x, app(x, x)), arr(α, α))) ? 
   Call: (11) types([isa(x, α)], isa(app(x, x), α)) ? 
   Call: (12) lists:member(isa(app(x, x), α), [isa(x, α)]) ? 
   Fail: (12) lists:member(isa(app(x, x), α), [isa(x, α)]) ? 
   Redo: (11) types([isa(x, α)], isa(app(x, x), α)) ? 
   Call: (12) types([isa(x, α)], isa(x, arr(_17370, α))) ? 
   Call: (13) lists:member(isa(x, arr(_17370, α)), [isa(x, α)]) ? 
   Fail: (13) lists:member(isa(x, arr(_17370, α)), [isa(x, α)]) ? 
   Redo: (12) types([isa(x, α)], isa(x, arr(_17370, α))) ? 
   Fail: (12) types([isa(x, α)], isa(x, arr(_17370, α))) ? 
   Redo: (11) types([isa(x, α)], isa(app(x, x), α)) ? 
   Fail: (11) types([isa(x, α)], isa(app(x, x), α)) ? 
   Fail: (10) types([], isa(λ(x, app(x, x)), arr(α, α))) ? 
   Fail: (9) types(isa(λ(x, app(x, x)), arr(α, α))) ? 
false.

?- isΩ(Ω), isIType(IType), types(isa(Ω, IType)).
Ω = app(λ(x, app(x, x)), λ(x, app(x, x))),
IType = arr(α, α) 
?- isω(M), isIType(IType), types(isa(M, IType)).
false.

?- isΩ(Ω), isIType(IType), types(isa(Ω, IType)).
Ω = app(λ(x, app(x, x)), λ(x, app(x, x))),
IType = arr(α, α) 
?- trace.
true.

[trace]  ?- isΩ(Ω), isIType(IType), types(isa(Ω, IType)).
   Call: (9) isΩ(_20120) ? 
   Call: (10) isω(_20602) ? 
   Exit: (10) isω(λ(x, app(x, x))) ? 
   Exit: (9) isΩ(app(λ(x, app(x, x)), λ(x, app(x, x)))) ? 
   Call: (9) isIType(_20124) ? 
   Exit: (9) isIType(arr(α, α)) ? 
   Call: (9) types(isa(app(λ(x, app(x, x)), λ(x, app(x, x))), arr(α, α))) ? 
   Call: (10) types([], isa(app(λ(x, app(x, x)), λ(x, app(x, x))), arr(α, α))) ? 
   Call: (11) lists:member(isa(app(λ(x, app(x, x)), λ(x, app(x, x))), arr(α, α)), []) ? 
   Fail: (11) lists:member(isa(app(λ(x, app(x, x)), λ(x, app(x, x))), arr(α, α)), []) ? 
   Redo: (10) types([], isa(app(λ(x, app(x, x)), λ(x, app(x, x))), arr(α, α))) ? 
   Call: (11) types([], isa(λ(x, app(x, x)), arr(_20638, arr(α, α)))) ? 
   Call: (12) lists:member(isa(λ(x, app(x, x)), arr(_20638, arr(α, α))), []) ? 
   Fail: (12) lists:member(isa(λ(x, app(x, x)), arr(_20638, arr(α, α))), []) ? 
   Redo: (11) types([], isa(λ(x, app(x, x)), arr(_20638, arr(α, α)))) ? 
   Call: (12) types([isa(x, _20638)], isa(app(x, x), arr(α, α))) ? 
   Call: (13) lists:member(isa(app(x, x), arr(α, α)), [isa(x, _20638)]) ? 
   Fail: (13) lists:member(isa(app(x, x), arr(α, α)), [isa(x, _20638)]) ? 
   Redo: (12) types([isa(x, _20638)], isa(app(x, x), arr(α, α))) ? 
   Call: (13) types([isa(x, _20638)], isa(x, arr(_20668, arr(α, α)))) ? 
   Call: (14) lists:member(isa(x, arr(_20668, arr(α, α))), [isa(x, _20638)]) ? 
   Exit: (14) lists:member(isa(x, arr(_20668, arr(α, α))), [isa(x, arr(_20668, arr(α, α)))]) ? 
   Exit: (13) types([isa(x, arr(_20668, arr(α, α)))], isa(x, arr(_20668, arr(α, α)))) ? 
   Call: (13) types([isa(x, arr(_20668, arr(α, α)))], isa(x, _20668)) ? 
   Call: (14) lists:member(isa(x, _20668), [isa(x, arr(_20668, arr(α, α)))]) ? 
   Exit: (14) lists:member(isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α))), [isa(x, arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))]) ? 
   Exit: (13) types([isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))], isa(x, arr(arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))) ? 
   Exit: (12) types([isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))], isa(app(x, x), arr(α, α))) ? 
   Exit: (11) types([], isa(λ(x, app(x, x)), arr(arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))) ? 
   Call: (11) types([], isa(λ(x, app(x, x)), arr(arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))) ? 
   Call: (12) lists:member(isa(λ(x, app(x, x)), arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α))), []) ? 
   Fail: (12) lists:member(isa(λ(x, app(x, x)), arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α))), []) ? 
   Redo: (11) types([], isa(λ(x, app(x, x)), arr(arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))) ? 
   Call: (12) types([isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))], isa(app(x, x), arr(α, α))) ? 
   Call: (13) lists:member(isa(app(x, x), arr(α, α)), [isa(x, arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))]) ? 
   Fail: (13) lists:member(isa(app(x, x), arr(α, α)), [isa(x, arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))]) ? 
   Redo: (12) types([isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))], isa(app(x, x), arr(α, α))) ? 
   Call: (13) types([isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))], isa(x, arr(_20722, arr(α, α)))) ? 
   Call: (14) lists:member(isa(x, arr(_20722, arr(α, α))), [isa(x, arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))]) ? 
   Exit: (14) lists:member(isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α))), [isa(x, arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))]) ? 
   Exit: (13) types([isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))], isa(x, arr(arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))) ? 
   Call: (13) types([isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))], isa(x, arr(arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))) ? 
   Call: (14) lists:member(isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α))), [isa(x, arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))]) ? 
   Exit: (14) lists:member(isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α))), [isa(x, arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))]) ? 
   Exit: (13) types([isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))], isa(x, arr(arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))) ? 
   Exit: (12) types([isa(x, arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))], isa(app(x, x), arr(α, α))) ? 
   Exit: (11) types([], isa(λ(x, app(x, x)), arr(arr(arr(arr(arr(arr(arr(arr(..., ...), arr(..., ...)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)), arr(α, α)))) ? 
   Exit: (10) types([], isa(app(λ(x, app(x, x)), λ(x, app(x, x))), arr(α, α))) ? 
   Exit: (9) types(isa(app(λ(x, app(x, x)), λ(x, app(x, x))), arr(α, α))) ? 
Ω = app(λ(x, app(x, x)), λ(x, app(x, x))),
IType = arr(α, α) 
[trace]  ?-   C-c C-c
Action (h for help) ? a
abort
% Execution Aborted

?- arr(X, arr(α, α)) = X.
false.

?- isΩ(Ω), isIType(IType), types(isa(Ω, IType)).
false.

?- isY(Y), isIType(IType), types(isa(Y, IType)).
false.

?- isY(Y), types(isa(Y, arr(arr(α, α), α))).
false.

?- isI(I), types(isa(I, IType)).
I = λ(x, x),
IType = arr(_5328, _5328) 
?- isI(K), types(isa(K, KType)).
K = λ(x, x),
KType = arr(_5706, _5706) 
?- isK(K), types(isa(K, KType)).
K = λ(x, λ(y, x)),
KType = arr(_6124, arr(_6148, _6124)) 
?- isKs(K), types(isa(Ks, KsType)).
ERROR: Out of local stack

?- isKs(Ks), types(isa(Ks, KsType)).
Ks = λ(x, λ(y, y)),
KsType = arr(_26259974, arr(_26259998, _26259998)) 
?- isS(S), types(isa(S, SType)).
S = λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))),
SType = arr(arr(_26260462, arr(_26260492, _26260464)), arr(arr(_26260462, _26260492), arr(_26260462, _26260464))) ;
false.

?- isω(M), types(isa(M, T)).
false.

?- isΩ(M), types(isa(M, T)).
false.

?- isω(M), typeable(M).
false.

?- isΩ(M), typeable(M).
false.

?- isY(M), typeable(M).
false.

?- types(isa(λ(x, λ(x, app(x, x)))), T).
ERROR: Out of trail stack
   Exception: (1,048,184) types(isa(λ(x, λ(x, app(x, x)))), isa(_45132236, arr(_45132248, arr(_45132230, arr(_45132212, arr(_45132194, arr(_45132176, arr(_45132158, arr(_45132140, arr(..., ...)))))))))) ? 
[PROLOG SYSTEM ERROR:  Thread 1 (main) at Tue Apr 28 11:17:36 2020
	After down phase: relocation_cells = 10481799; relocated_cells = 11055902
[While in 21-th garbage collection]


?- types(isa(λ(x, λ(x, app(x, x)))), T).
false.