Welcome to SWI-Prolog (threaded, 64 bits, version 8.4.2)
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).

?- true.

?- [x : α ⇒ β ⇒ γ, y : α ⇒ β] = X.
X = [x:α⇒β⇒γ, y:α⇒β].

?- true.

?- [x : α ⇒ β ⇒ γ, y : α ⇒ β] = X.
X = [x:α⇒β⇒γ, y:α⇒β].

?- true.

?- [x : α ⇒ β ⇒ γ, y : α ⇒ β] = X.
X = [x:α⇒β⇒γ, y:α⇒β].

?- [x : α ⇒ β ⇒ γ, y : α ⇒ β] ⊢ x : T.
T = α⇒β⇒γ ;
false.

?- ERROR: /home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinf.pro:25:8: Syntax error: Operator expected
true.

?- ERROR: /home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinf.pro:25:8: Syntax error: Operator expected
true.

?- ERROR: /home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinf.pro:25:8: Syntax error: Operator expected
true.

?- Warning: /home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinf.pro:25:
Warning:    Singleton variables: [Ρ]
true.

?- true.

?- true.

?- true.

?- i(I).
I = λ(x, x).

?- k(K).
K = λ(x, λ(y, x)).

?- omega(Omega).
Omega = λ(x, x@x)@λ(x, x@x).

?- true.

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

?- k(K), ⊢ I : T.
  C-c C-c
Action (h for help) ? Unknown option (h for help)
Action (h for help) ? a
abort
% Execution Aborted
?- k(K), ⊢ K : T.
K = λ(x, λ(y, x)),
T = _A⇒_⇒_A ;
false.

?- s(S), ⊢ S : T.
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_A⇒_B⇒_C)⇒(_A⇒_B)⇒_A⇒_C Unknown action: [ (h for help)
Action? a

?- Warning: /home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinf.pro:33:
Warning:    Singleton variables: [Τ,Ρ,Σ]
true.

?- Warning: /home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinf.pro:33:
Warning:    Singleton variables: [Γ,M,Τ,T,Ρ,Σ]
true.

?- s(S), ⊢ S : T.
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_A⇒_B⇒_C)⇒(_A⇒_B)⇒_A⇒_C ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_A⇒_B⇒_C)⇒(_⇒_B)⇒_A⇒_C ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_A⇒_⇒_B)⇒_⇒_A⇒_B ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_A⇒_⇒_B)⇒_⇒_A⇒_B ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_A⇒_⇒_B)⇒_⇒_A⇒_B ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_⇒_A⇒_B)⇒(_C⇒_A)⇒_C⇒_B ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_⇒_A⇒_B)⇒(_⇒_A)⇒_⇒_B ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_⇒_⇒_A)⇒_⇒_⇒_A ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_⇒_⇒_A)⇒_⇒_⇒_A ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_⇒_⇒_A)⇒_⇒_⇒_A ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒(_A⇒_)⇒_A⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒(_⇒_)⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒(_A⇒_)⇒_A⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒(_⇒_)⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒(_A⇒_)⇒_A⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒(_⇒_)⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ ;
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T = _⇒_⇒_⇒_ 

?- true.

?- s(S), ⊢ S : T.
S = λ(x, λ(y, λ(z, x@z@(y@z)))),
T =  (_A⇒_B⇒_C)⇒(_A⇒_B)⇒_A⇒_C ;
false.

?- k(K), ⊢ K : T.
K = λ(x, λ(y, x)),
T = _A⇒_⇒_A ;
false.

?- ω(W), ⊢ W : T.
W = λ(x, x@x),
T = _S1⇒_A, % where
    _S1 = _S1⇒_A   C-c C-c
Action (h for help) ? a
abort
% Execution Aborted
?- X = f(X).
X = f(X).

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

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

?- ERROR: /home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinf.pro:1:
ERROR:    catch/3: Unknown procedure: set_occurs_check/1
Warning: /home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinf.pro:1:
Warning:    Goal (directive) failed: user:set_occurs_check(true)
true.

?- true.

?- X = f(X).
false.

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

?- true.

?- ω(W), ⊢ W : T.
false.

?- c0(C0), ⊢ C0: T.
C0 = λ(f, λ(x, x)),
T = _⇒_A⇒_A ;
false.

?- c1(C1), ⊢ C1: T.
C1 = λ(f, λ(x, f@x)),
T =  (_A⇒_B)⇒_A⇒_B ;
false.

?- c2(C2), ⊢ C2: T.
C2 = λ(f, λ(x, f@(f@x))),
T =  (_A⇒_A)⇒_A⇒_A ;
false.

?- c0(C0), c1(C1),  ⊢ C0: T, ⊢ C1:T.
C0 = λ(f, λ(x, x)),
C1 = λ(f, λ(x, f@x)),
T =  (_A⇒_A)⇒_A⇒_A ;
false.

?- true.

?- true.

?- ti(TI), ⊢ I : TI.
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted
?- ti(TI), ⊢ I : TI.
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted
?- trace.
true.

[trace]  ?- ti(TI), ⊢ I : TI.
   Call: (11) ti(_2758) ? 
   Exit: (11) ti(α⇒α) ? 
   Call: (11) ⊢_2762:α⇒α ? 
   Call: (12) []⊢_2762:α⇒α ? 
   Call: (13) _2762:α⇒α∈[] ? 
   Call: (14) lists:member(_2762:α⇒α, []) ? 
   Fail: (14) lists:member(_2762:α⇒α, []) ? 
   Fail: (13) _2762:α⇒α∈[] ? 
   Redo: (12) []⊢_2762:α⇒α ? 
   Call: (13) []⊢_8698:_8710⇒α⇒α ? 
   Call: (14) _8698:_8710⇒α⇒α∈[] ? 
   Call: (15) lists:member(_8698:_8710⇒α⇒α, []) ? 
   Fail: (15) lists:member(_8698:_8710⇒α⇒α, []) ? 
   Fail: (14) _8698:_8710⇒α⇒α∈[] ? 
   Redo: (13) []⊢_8698:_8710⇒α⇒α ? 
   Call: (14) []⊢_12238:_12250⇒_8710⇒α⇒α ? 
   Call: (15) _12238:_12250⇒_8710⇒α⇒α∈[] ? 
   Call: (16) lists:member(_12238:_12250⇒_8710⇒α⇒α, []) ? 
   Fail: (16) lists:member(_12238:_12250⇒_8710⇒α⇒α, []) ? 
   Fail: (15) _12238:_12250⇒_8710⇒α⇒α∈[] ? 
   Redo: (14) []⊢_12238:_12250⇒_8710⇒α⇒α ? 
   Call: (15) []⊢_15778:_15790⇒_12250⇒_8710⇒α⇒α ? 
   Call: (16) _15778:_15790⇒_12250⇒_8710⇒α⇒α∈[] ? 
   Call: (17) lists:member(_15778:_15790⇒_12250⇒_8710⇒α⇒α, []) ? 
   Fail: (17) lists:member(_15778:_15790⇒_12250⇒_8710⇒α⇒α, []) ? 
   Fail: (16) _15778:_15790⇒_12250⇒_8710⇒α⇒α∈[] ? 
   Redo: (15) []⊢_15778:_15790⇒_12250⇒_8710⇒α⇒α ? 
   Call: (16) []⊢_19318:_19330⇒_15790⇒_12250⇒_8710⇒α⇒α ? 
   Call: (17) _19318:_19330⇒_15790⇒_12250⇒_8710⇒α⇒α∈[] ? 
   Call: (18) lists:member(_19318:_19330⇒_15790⇒_12250⇒_8710⇒α⇒α, []) ? 
   Fail: (18) lists:member(_19318:_19330⇒_15790⇒_12250⇒_8710⇒α⇒α, []) ? 
   Fail: (17) _19318:_19330⇒_15790⇒_12250⇒_8710⇒α⇒α∈[] ? 
   Redo: (16) []⊢_19318:_19330⇒_15790⇒_12250⇒_8710⇒α⇒α ? 
   Call: (17) []⊢_22858:_22870⇒_19330⇒_15790⇒_12250⇒_8710⇒α⇒α ? a
% Execution Aborted
[trace]  ?-    Call: (19) prolog_load_file(user:'/home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinf.pro', [expand(false), expand(true)]) ? a
% Execution Aborted
[trace]  ?- trade.
Correct to: "trace"? y
true.

[trace]  ?- notrace.
true.

[debug]  ?-   C-c C-c
Action (h for help) ? a
abort
% Execution Aborted
[debug]  ?- 
|    .
ERROR: Unknown procedure: ? / 0 (DWIM could not correct goal)
[debug]  ?- a
|    .
ERROR: Unknown procedure: a/0 (DWIM could not correct goal)
[debug]  ?- help.


  C-c C-ca
Action (h for help) ? abort
Thread 1 (main): foreign predicate system:ground/1 did not clear exception: 
	$aborted
  C-c C-c  C-c C-c
WARNING: By typing Control-C twice, you have forced an asynchronous
WARNING: interrupt.  Your only SAFE operations are: c(ontinue), p(id),
WARNING: s(stack) and e(xit).  Notably a(abort) often works, but
WARNING: leaves the system in an UNSTABLE state

Action (h for help) ? 
Unknown option (h for help)
Action (h for help) ? a
abort
Warning: /usr/lib/swi-prolog/library/socket.pl:171:
Warning:    Execution Aborted
% Execution Aborted
[debug]  ?-   C-c C-c
Action (h for help) ? h
Options:
a:           abort         b:           break
c:           continue      e:           exit
g:           goals         s:           C-backtrace
t:           trace         p:		  Show PID
h (?):       help
Action (h for help) ? trace.
trace
continue (trace mode)

  C-c C-c
Action (h for help) ? a
abort
% Execution Aborted
[debug]  ?- ti(TI), ⊢ I : TI.
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted
[debug]  ?- trace.
true.

[trace]  ?- ti(TI), ⊢ I : TI.
   Call: (11) ti(_3116) ?   C-c C-c
Action (h for help) ? a
EOF: exit (status 4)

Process prolog exited abnormally with code 4