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

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

?- X = M:(α⇒(β⇒γ)).
X = M:α⇒β⇒γ.

?- X = M:α⇒β⇒γ.
X = M:α⇒β⇒γ.

?- (X:Y) = M:α⇒β⇒γ.
X = M,
Y = α⇒β⇒γ.

?- s(S).
S = λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))).

?- o(O).
O = app(λ(x, app(x, x)), λ(x, app(x, x))).

?- atom(x).
true.

?- atom(app(x,x)).
false.

?- isvar(x).
true.

?- atom(i).
true.

?- atom(o).
true.

?- i(I),ti(TI).
I = λ(x, x),
TI = α⇒α.

?- i(I) , ti(TI) , ⊢ I : TI.
I = λ(x, x),
TI = α⇒α ;
false.

?- k(M) , tk(Τ) , ⊢ M : Τ.
M = λ(x, λ(y, x)),
Τ = α⇒β⇒α ;
false.

?- s(M) , ts(Τ) , ⊢ M : Τ.
M = λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))),
Τ = (α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ

?- i(I) , ⊢ I : TI.
I = λ(x, x),
TI = _A⇒_A ;
false.

?- k(M) , ⊢ M : Τ.
M = λ(x, λ(y, x)),
Τ = _A⇒_⇒_A

?- s(M) , ⊢ M : Τ.
M = λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))),
Τ = (_A⇒_B⇒_C)⇒(_A⇒_B)⇒_A⇒_C ;
false.

?- trace.
true.

[trace]  ?- s(M) , ⊢ M : Τ.
   Call: (11) s(_11270) ?
   Exit: (11) s(λ(x, λ(y, λ(z, app(app(x, z), app(y, z)))))) ?
   Call: (11) ⊢λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))):_11276 ?
   Call: (12) []⊢λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))):_11276 ?
   Call: (13) isvar(λ(x, λ(y, λ(z, app(app(x, z), app(y, z)))))) ?
   Call: (14) atom(λ(x, λ(y, λ(z, app(app(x, z), app(y, z)))))) ?
   Fail: (14) atom(λ(x, λ(y, λ(z, app(app(x, z), app(y, z)))))) ?
   Fail: (13) isvar(λ(x, λ(y, λ(z, app(app(x, z), app(y, z)))))) ?
   Redo: (12) []⊢λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))):_11276 ?
   Call: (13) [x:_17448]⊢λ(y, λ(z, app(app(x, z), app(y, z)))):_17450 ?
   Call: (14) isvar(λ(y, λ(z, app(app(x, z), app(y, z))))) ?
   Call: (15) atom(λ(y, λ(z, app(app(x, z), app(y, z))))) ?
   Fail: (15) atom(λ(y, λ(z, app(app(x, z), app(y, z))))) ?
   Fail: (14) isvar(λ(y, λ(z, app(app(x, z), app(y, z))))) ?
   Redo: (13) [x:_17448]⊢λ(y, λ(z, app(app(x, z), app(y, z)))):_17450 ?
   Call: (14) [y:_21128, x:_17448]⊢λ(z, app(app(x, z), app(y, z))):_21130 ?
   Call: (15) isvar(λ(z, app(app(x, z), app(y, z)))) ?
   Call: (16) atom(λ(z, app(app(x, z), app(y, z)))) ?
   Fail: (16) atom(λ(z, app(app(x, z), app(y, z)))) ?
   Fail: (15) isvar(λ(z, app(app(x, z), app(y, z)))) ?
   Redo: (14) [y:_21128, x:_17448]⊢λ(z, app(app(x, z), app(y, z))):_21130 ?
   Call: (15) [z:_24808, y:_21128, x:_17448]⊢app(app(x, z), app(y, z)):_24810 ?
   Call: (16) isvar(app(app(x, z), app(y, z))) ?
   Call: (17) atom(app(app(x, z), app(y, z))) ?
   Fail: (17) atom(app(app(x, z), app(y, z))) ?
   Fail: (16) isvar(app(app(x, z), app(y, z))) ?
   Redo: (15) [z:_24808, y:_21128, x:_17448]⊢app(app(x, z), app(y, z)):_24810 ?
   Call: (16) [z:_24808, y:_21128, x:_17448]⊢app(x, z):_28494⇒_24810 ?
   Call: (17) isvar(app(x, z)) ?
   Call: (18) atom(app(x, z)) ?
   Fail: (18) atom(app(x, z)) ?
   Fail: (17) isvar(app(x, z)) ?
   Redo: (16) [z:_24808, y:_21128, x:_17448]⊢app(x, z):_28494⇒_24810 ?
   Call: (17) [z:_196, y:_172, x:_148]⊢x:_240⇒_226⇒_198 ?
   Call: (18) isvar(x) ?
   Call: (19) atom(x) ?
   Exit: (19) atom(x) ?
   Exit: (18) isvar(x) ?
   Call: (18) lists:member(x:_240⇒_226⇒_198, [z:_196, y:_172, x:_148]) ?
   Exit: (18) lists:member(x:_240⇒_226⇒_198, [z:_196, y:_172, x:_240⇒_226⇒_198]) ?
   Exit: (17) [z:_196, y:_172, x:_240⇒_226⇒_198]⊢x:_240⇒_226⇒_198 ?
   Call: (17) [z:_196, y:_172, x:_240⇒_226⇒_198]⊢z:_240 ?
   Call: (18) isvar(z) ?
   Call: (19) atom(z) ?
   Exit: (19) atom(z) ?
   Exit: (18) isvar(z) ?
   Call: (18) lists:member(z:_240, [z:_196, y:_172, x:_240⇒_226⇒_198]) ?
   Exit: (18) lists:member(z:_196, [z:_196, y:_172, x:_196⇒_226⇒_198]) ?
   Exit: (17) [z:_196, y:_172, x:_196⇒_226⇒_198]⊢z:_196 ?
   Exit: (16) [z:_196, y:_172, x:_196⇒_226⇒_198]⊢app(x, z):_226⇒_198 ?
   Call: (16) [z:_196, y:_172, x:_196⇒_226⇒_198]⊢app(y, z):_226 ?
   Call: (17) isvar(app(y, z)) ?
   Call: (18) atom(app(y, z)) ?
   Fail: (18) atom(app(y, z)) ?
   Fail: (17) isvar(app(y, z)) ?
   Redo: (16) [z:_196, y:_172, x:_196⇒_226⇒_198]⊢app(y, z):_226 ?
   Call: (17) [z:_196, y:_172, x:_196⇒_226⇒_198]⊢y:_15520⇒_226 ?
   Call: (18) isvar(y) ?
   Call: (19) atom(y) ?
   Exit: (19) atom(y) ?
   Exit: (18) isvar(y) ?
   Call: (18) lists:member(y:_15520⇒_226, [z:_196, y:_172, x:_196⇒_226⇒_198]) ?
   Exit: (18) lists:member(y:_15520⇒_226, [z:_196, y:_15520⇒_226, x:_196⇒_226⇒_198]) ?
   Exit: (17) [z:_196, y:_15520⇒_226, x:_196⇒_226⇒_198]⊢y:_15520⇒_226 ?
   Call: (17) [z:_196, y:_15520⇒_226, x:_196⇒_226⇒_198]⊢z:_15520 ?
   Call: (18) isvar(z) ?
   Call: (19) atom(z) ?
   Exit: (19) atom(z) ?
   Exit: (18) isvar(z) ?
   Call: (18) lists:member(z:_15520, [z:_196, y:_15520⇒_226, x:_196⇒_226⇒_198]) ?
   Exit: (18) lists:member(z:_196, [z:_196, y:_196⇒_226, x:_196⇒_226⇒_198]) ?
   Exit: (17) [z:_196, y:_196⇒_226, x:_196⇒_226⇒_198]⊢z:_196 ?
   Exit: (16) [z:_196, y:_196⇒_226, x:_196⇒_226⇒_198]⊢app(y, z):_226 ?
   Exit: (15) [z:_196, y:_196⇒_226, x:_196⇒_226⇒_198]⊢app(app(x, z), app(y, z)):_198 ?
   Exit: (14) [y:_196⇒_226, x:_196⇒_226⇒_198]⊢λ(z, app(app(x, z), app(y, z))):_196⇒_198 ?
   Exit: (13) [x:_196⇒_226⇒_198]⊢λ(y, λ(z, app(app(x, z), app(y, z)))):(_196⇒_226)⇒_196⇒_198 ?
   Exit: (12) []⊢λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))):(_196⇒_226⇒_198)⇒(_196⇒_226)⇒_196⇒_198 ?
   Exit: (11) ⊢λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))):(_196⇒_226⇒_198)⇒(_196⇒_226)⇒_196⇒_198 ?
M = λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))),
Τ = (_A⇒_B⇒_C)⇒(_A⇒_B)⇒_A⇒_C

?- ω(M), ⊢ M : Τ.
M = λ(x, app(x, x)),
Τ = _S1⇒_A, % where
    _S1 = _S1⇒_A

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

?- X = f(Y), Y = g(X).
X = f(g(X)),
Y = g(X).

?- X = f(X).
false.

?- X = f(Y), Y = g(X).
false.

?- ω(M), ⊢ M : Τ.
false.

?- s(M) , ⊢ M : Τ.
M = λ(x, λ(y, λ(z, app(app(x, z), app(y, z))))),
Τ = (_A⇒_B⇒_C)⇒(_A⇒_B)⇒_A⇒_C ;
false.

?- c(0,C0).
C0 = λ(f, λ(x, x))

?- c(1,M).
M = λ(f, λ(x, app(f, x)))

?- c(5,M).
M = λ(f, λ(x, app(f, app(f, app(f, app(f, app(f, x)))))))

?- c(1,M) , ⊢ M : Τ.
M = λ(f, λ(x, app(f, x))),
Τ = (_A⇒_B)⇒_A⇒_B

?- c(2,M) , ⊢ M : Τ.
M = λ(f, λ(x, app(f, app(f, x)))),
Τ = (_A⇒_A)⇒_A⇒_A

?- c(5,M) , ⊢ M : Τ.
M = λ(f, λ(x, app(f, app(f, app(f, app(f, app(f, x))))))),
Τ = (_A⇒_A)⇒_A⇒_A

?- c(5,M) , nat(Nat), ⊢ M : Nat.
M = λ(f, λ(x, app(f, app(f, app(f, app(f, app(f, x))))))),
Nat = (α⇒α)⇒α⇒α