Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.2.3)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.

For help, use ?- help(Topic). or ?- apropos(Word).

?- true.

?- loves(john, mary).
true.

?- loves(john, X).
X = mary.

?- loves(X, Y).
X = john,
Y = mary.

?- true.

?- loves(X, mary).
X = john ;
X = tom.

?- loves(tom, Y).
Y = mary.

?- true.

?- true.

?- loves(john, X).
X = mary ;
X = john ;
X = tom ;
false.

?- true.

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

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

?- k(K).
ERROR: toplevel: Undefined procedure: k/1 (DWIM could not correct goal)
?- true.

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

?- true.

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

?- true.

?- omega(O).
O = app(lam(x, app(x, x)), lam(x, app(x, x))).

?- true.

?- ti(X).
X = arrow(alpha, alpha).

?- tk(X).
X = arrow(alpha, arrow(beta, alpha)).

?- [1, 2, 3]
|    .
ERROR: is_absolute_file_name/1: Type error: `text' expected, found `1' (an integer)
ERROR: is_absolute_file_name/1: Type error: `text' expected, found `2' (an integer)
ERROR: is_absolute_file_name/1: Type error: `text' expected, found `3' (an integer)
true.

?- L = [1, 2, 3].
L = [1, 2, 3].

?- [X|T] = [1, 2, 3].
X = 1,
T = [2, 3].

?- [X|T] = [].
false.

?- member(1, [1, 2, 3]).
true ;
false.

?- member(X, [1, 2, 3]).
X = 1 ;
X = 2 ;
X = 3.

?- member(1, L).
L = [1|_G2993] ;
L = [_G2992, 1|_G2996] ;
L = [_G2992, _G2995, 1|_G2999] ;
L = [_G2992, _G2995, _G2998, 1|_G3002] ;
L = [_G2992, _G2995, _G2998, _G3001, 1|_G3005] ;
L = [_G2992, _G2995, _G2998, _G3001, _G3004, 1|_G3008] ;
L = [_G2992, _G2995, _G2998, _G3001, _G3004, _G3007, 1|_G3011] 

?- member(X, Y).
Y = [X|_G3008] ;
Y = [_G3007, X|_G3011] ;
Y = [_G3007, _G3010, X|_G3014] ;
Y = [_G3007, _G3010, _G3013, X|_G3017] ;
Y = [_G3007, _G3010, _G3013, _G3016, X|_G3020] 

?- true.

?- types([], x, alpha).
false.

?- types(X, x, alpha).
X = [[x, alpha]|_G3001] ;
X = [_G3000, [x, alpha]|_G3004] ;\
X = [_G3000, _G3003, [x, alpha]|_G3007] ;
X = [_G3000, _G3003, _G3006, [x, alpha]|_G3010] ;
X = [_G3000, _G3003, _G3006, _G3009, [x, alpha]|_G3013] 

?- types(Gamma, x, alpha).
Gamma = [[x, alpha]|_G3001] ;
Gamma = [_G3000, [x, alpha]|_G3004] ;
Gamma = [_G3000, _G3003, [x, alpha]|_G3007] ;
Gamma = [_G3000, _G3003, _G3006, [x, alpha]|_G3010] 

?- types([[x,alpha],[y,beta]], x, Tau).
Tau = alpha ;
false.

?- true.

?- types(Gamma, app(x, y), alpha).
Gamma = [[app(x, y), alpha]|_G3007] Gamma = [_G3006, [app(x, y), alpha]|_G3010] ;
Gamma = [_G3006, _G3009, [app(x, y), alpha]|_G3013] 

?- types(Gamma, app(x, y), alpha).
Gamma = [[app(x, y), alpha]|_G3007] 

?- true.

?- types(Gamma, app(x, y), alpha).
Gamma = [[x, arrow(_G3000, alpha)], [y, _G3000]|_G3019] ;
Gamma = [[x, arrow(_G3000, alpha)], _G3018, [y, _G3000]|_G3022] ;
Gamma = [[x, arrow(_G3000, alpha)], _G3018, _G3021, [y, _G3000]|_G3025] ;
Gamma = [[x, arrow(_G3000, alpha)], _G3018, _G3021, _G3024, [y, _G3000]|_G3028] ;
Gamma = [[x, arrow(_G3000, alpha)], _G3018, _G3021, _G3024, _G3027, [y, _G3000]|_G3031] ;
Gamma = [[x, arrow(_G3000, alpha)], _G3018, _G3021, _G3024, _G3027, _G3030, [y, _G3000]|_G3034] ;
Gamma = [[x, arrow(_G3000, alpha)], _G3018, _G3021, _G3024, _G3027, _G3030, _G3033, [y|...]|_G3037] 

?- true.

?- i(I), types(Gamma, I, Tau).
I = lam(x, x),
Tau = arrow(_G3069, _G3069) ;
I = lam(x, x),
Gamma = [[x, _G3070]|_G3088],
Tau = arrow(_G3069, _G3070) ;
I = lam(x, x),
Gamma = [_G3087, [x, _G3070]|_G3091],
Tau = arrow(_G3069, _G3070) ;
I = lam(x, x),
Gamma = [_G3087, _G3090, [x, _G3070]|_G3094],
Tau = arrow(_G3069, _G3070) 

?- true.

?- i(I), types(I, Tau).
I = lam(x, x),
Tau = arrow(_G3052, _G3052) ;
false.

?- k(K), types(K, Tau).
K = lam(x, lam(y, x)),
Tau = arrow(_G3055, arrow(_G3067, _G3055)) ;
false.

?- s(S), types(S, Tau).
S = lam(x, lam(y, lam(z, app(app(x, z), app(y, z))))),
Tau = arrow(arrow(_G3091, arrow(_G3103, _G3092)), arrow(arrow(_G3091, _G3103), arrow(_G3091, _G3092))) ;
false.

?- omega(O), types(O, Tau).
O = app(lam(x, app(x, x)), lam(x, app(x, x))) ;
false.

?- w(W), types(W, Tau).
W = lam(x, app(x, x)),
Tau = arrow(_S1, _G3056), % where
    _S1 = arrow(_S1, _G3056) false.

?- true.

?- w(W), types(W, Tau).
false.

?-