Toggle navigation
?
users online
Logout
Open hangout
Open chat for current file
% for stackoverflow.com/questions/75174062 % by stackoverflow.com/users/849891/will-ness :- op(450,xfy,-). % for '-' to assoc on the right; '*' on the left type( c, (A-B-C)-B-A-C). % s*(b*b*s)*(k*k) Cfxy=fyx type( b, (A-B)-(C-A)-C-B). % s*(k*s)*k Bfgx=f(gx) type( i, A-A). % s*k*k Ix=x type( k, A-_-A). % Wfx=CSIfx=SfIx=fxx type( s, (A-B-C) - (A-B)-A-C). % c*s*i : (A-A-B)-A-B type( F*X, B) :- type( F, A-B), type( X, A). run(X,Z) :- U = s*i*i, % U combinator, Ux = xx, U : t ~ (t->a) Y = b*U*(c*b*U), % Y combinator, Yf = f(Yf), Y : (a->a)->a type( Y, X), % Y = BU(CBU) type( Y*i, Z), numbervars( [X,Z], 0, _). %%% run(Y,YI), type(s*i*i, T), numbervars(T,2,_), %%% arg(1,T,T1), arg(1,T1,T). %%% => %%% T = T1, T1 = T1-C, Y = (A-A)-A, YI = B %%% i.e. %%% T = T-C, Y = (A-A)-A, YI = B