Toggle navigation
?
users online
Logout
Open hangout
Open chat for current file
%% PROLOG % x :- y,z has the same meaning as % y z % ----- % x % Variables always start with capitals. %% TERMS % "z" is to be understood as 0, "pair" is, well, for pairing term(z). term(s(N)) :- term(N). term(pair(X,Y)) :- term(X), term(Y). term(sum(X)) :- term(X). % "::" is taken instead of a single colon since that is already used. :- op(800, xfx, ::). %% TYPING z :: nat. s(N) :: nat :- N :: nat. pair(X,Y) :: natpair :- X :: nat, Y :: nat. sum(X) :: nat :- X :: natpair. %% SINGLE-STEP REDUCTION % required for Prolog reasons, no transitivity red(z,z). red(pair(X,Y),pair(X1,Y1)) :- red(X,X1), red(Y,Y1). red(s(X),s(Y)) :- red(X,Y). %red(X,Z) :- red(X,Y), red(Y,Z). red(sum(pair(z,X)), X). red(sum(pair(s(Y),X)),s(sum(pair(Y,X)))). %% REAL REDUCTION % the transitive closure of red reds(X,Y) :- red(X,Y). reds(X,Z) :- red(X,Y), reds(Y,Z).