// Unification Algorithm // Chang and Lee, Symbolic Logic and Mechanical Theorem Proving \d .unify mgu:{[a;b](mgu_ .)/(a;b;())} mgu_:{[a;b;u]:[a~b;(a;b;u);unify[a;b;u]occurs . disagree[a]b]} unify:{[a;b;u;v](apply[a]v;apply[b]v;compose[u]v)} disagree:{[a;b]:[(*a)~*b;_f[atom 1_ a;atom 1_ b];expression'(a;b)]} expression:{[e]:[4:e;e;*e]} occurs:{[a;b] if[~|/c:variable'(a;b);'`fail] if[c 1;t:a;a:b;b:t] if[{:[@y;x=y;|/x _f/:y]}[a]b;'`fail] ,(b;a)} atom:{:[1=#x;*x;x]} variable:{x _in"xyzuvw"} apply:{:[#x;{{:[x~z;y;@x;x;_f[;y;z]'x]}[x]. y}/[x;y];y]} compose:{:[~#x;y;~#y;x;.[x;(;0);apply[;y]],y@&~y[;1]_lin x[;1]]} \ \l parse w:.parse.p'("P[a,x,f[g[y]]]";"P[z,f[z],f[u]]") mgu . w