%  This module implements the unification problems that
%  Huet showed in 
%
%	G. Huet, ``The Undecidability of Unification in Third Order
%	Logic,'' Information and Control 22(3), 1973, 257 -- 267.
%
%  to be equivalent to solutions of the Post correspondence problem.
%  A conclusion of this encoding is that third order unification (notice the
%  type of the argument for two_corresp) is recursively undecidable.
%  This is also a good example of a rather simple problem for which the
%  depth-first implementation of unification in lambda Prolog will
%  often get into a loop.

module post.

kind	i	type.

%  Letters are encoded as functions.  Thus, appending of lists is
%  function composition.  By properties of lambda conversion, this
%  operation is associative.
%  u and v are one element lists.  (X\ (u (v X))) is a two element
%  list.  (X\X) is the empty list.

type	u	i -> i.
type	v	i -> i.

type	two_corresp	((i -> i) -> (i -> i) -> i) -> o.
type	three_corresp	((i -> i) -> (i -> i) -> (i -> i) -> i) -> o.

%  This is the Post problem {(uv,u), (u,vu)}.
two_corresp F :- 
   (F (X\ (u (v X))) u) =
   (F u (X\ (v (u X)))),
   (F u u) = (u (G u )).

%  This is the Post problem {(uv,vu), (v,vu), (u,e)}.
three_corresp F :-
   (F (X\ (u (v X)))  v             u) =
   (F (X\ (v (u X))) (X\ (v (u X))) (X\X)),
   (F u u u) = (u (G u)).


% Terzo> #load "post.mod".
% [reading file ./post.mod]
% module post
% [closed file ./post.mod]
% Terzo> #query post two_corresp F.
% 
% F = x\ x1\ u (F1 x x1) 
% (( F1,
%    G,
%    F1 u u = G u,
%    F1 (X\ u (v u)) u = F1 u (X1\ v (u X1)) ))
% 
% Terzo> #query post three_corresp F.
% 
% F = x\ x1\ x2\ u (F1 x x1 x2) 
% (( F1,
%    G,
%    F1 u u u = G u,
%    F1 (X\ u (v v)) v u
%     = F1 (X1\ v (u X2\ v (u X3\ X1))) (X4\ v (u X5\ X4)) (X6\ X6) ))
% 
% Terzo>