%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%	Prolog Codes for the Three Versions of 
%		Variants Lambek Calculus.
%	By	Shen-Tzay Huang
%		Computer Science Dept. UCLA.
%		June, 1992.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Version 1 : 
%    Undirectional + FA + FC.
:- op(400, xfy, ':').

%  Main program.
lambek(Lexicon, Final) :-
        lca(Lexicon, Clist),
        calculus(Clist,Final).

calculus([X],[X]).
calculus([X,Y|Xs],Z) :-
        lc(X,Y,XY),!,
        calculus([XY|Xs],Z).
calculus([X,Y|Xs],[Z]) :-
        calculus([Y|Xs],[YXs]), 
        lc(X,YXs,Z), !.
calculus([X,Y|Xs],Z) :-
        geachable(X,Y,XY),!,
        calculus([XY|Xs],Z).
calculus([X,Y|Xs],Z) :-
        mable(X,Y,XY),!,
        calculus([XY|Xs],Z).

%  Function Application
lc(F:X, Y, F)   :- eq(X,Y).
lc(X, F:Y, F)   :- eq(X,Y).

%  Functional Composition
lc(F:X, Y : Z, F:Z) :-	eq(X,Y).
lc(Y:Z, F : X, F:Z) :-	eq(X,Y).

%  Type Raising
%  a. Geach Rule
%     a:b  -> (a:c):(b:c)
%     Lower middle case.
%      W:R	->	((W:Z):(R:Z)).
geachable(X:(Y:Z), W:R, X:(R:Z)) :- 
        eq(W,Y).
geachable(W:R, X:(Y:Z), X:(R:Z)) :- 
        eq(W,Y).
%  Upper middle case.
geachable((Y:Z):X, R:W, (R:Z):X) :- 
        eq(W,Y).
geachable(R:W, (Y:Z):X, (R:Z):X) :- 
        eq(W,Y).

%  b. M rule.
%     a	-> b/(b/a).
%     lower case :	X/Y ; Y/(Y/W).
mable(X:Y,W,X:(Y:W)) :- \+ eq(W,Y).
mable(W,X:Y,X:(Y:W)) :- \+ eq(W,Y).
%     upper case :	(X/W)/Y ; X/(X/W).
mable((X:U):Y,W,X:Y) :- 
        \+ eq(W,Y),eq(U,W).
mable(W,(X:U):Y,X:Y) :- 
        \+ eq(W,Y),eq(U,W).

%  Lexical Category Assignment.
lca([],[]).
lca([X|Xs], [Y|Ys]) :-	
        dict(X,Y), lca(Xs,Ys).

%  dictionary :
%  for phrase : 
%  a cake which i believe that she ate.
dict(a, np:n).
dict(cake, n:r).
dict(which, r:(s:np)).
dict(i,s:fvp).
dict(believe, fvp:s1).
dict(that, s1:s).
dict(she,s:fvp).
dict(ate, fvp:np).

%  for phrase : 
%  i believe that she ate those cakes.
dict(those, np:n).
dict(cakes,n).

% for phrase : john walks.
dict(john, n).
dict(walks, t:n).

% for phrase : everyone loves someone.
dict(everyone,s:fvp).
dict(loves,fvp:np).
dict(someone,s:(s:np)).

%  Underlying equational theory for 
%  defining matching. Currently, it's 
%  just first order unification.
eq(X,X).


%  Version 2 : 
%    Undirectional + FA + FC + M + G, 
%    together with Semantic Data Structure 
%    along with the parsing processing.
%
:-  op(400, xfy, ':').
:-  op(500, xfy, 'of').

%  Main program.
lambek(Lexicon, Final) :-
        lca(Lexicon, Clist),
        calculus(Clist,Final).

calculus([X],[X]).
calculus([X,Y|Xs],Z) :-
        lc(X,Y,XY),!,
        calculus([XY|Xs],Z).
calculus([X,Y|Xs],[Z]) :-
        calculus([Y|Xs],[YXs]), 
        lc(X,YXs,Z), !.
calculus([X,Y|Xs],Z) :-
        geachable(X,Y,XY),!,
        calculus([XY|Xs],Z).
calculus([X,Y|Xs],Z) :-
        mable(X,Y,XY),!,
        calculus([XY|Xs],Z).

%  Function Application
lc(V1 of F:X,V2 of Y, V3 of F) :- 
        eq(X,Y), apply(V1,V2,V3).
lc(V1 of X, V2 of F:Y, V3 of F)	:- 
        eq(X,Y), apply(V2,V1,V3).

%  Functional Composition
lc(V1 of F:X, V2 of Y : Z, V3 of F:Z) :-
        eq(X,Y),compose(V1,V2,V3).
lc(V1 of Y:Z, V2 of F : X, V3 of F:Z) :-
        eq(X,Y),compose(V2,V1,V3).

%  Type Raising
%  a. Geach Rule
%     a:b -> (a:c):(b:c)
%     Lower middle case.
geachable(V1 of X:(Y:Z), V2 of W:R,
          V3 of X:(R:Z)) 
      :- eq(W,Y), simple_graise(V2,V1,V3).
geachable(V1 of W:R, V2 of X:(Y:Z), 
          V3 of X:(R:Z))
      :- eq(W,Y),simple_graise(V1,V2,V3).
%  Upper middle case.
geachable(V1 of (Y:Z):X, V2 of R:W, 
          V3 of (R:Z):X)
      :- eq(W,Y), graise(V2,V1,V3).
geachable(V1 of R:W, V2 of (Y:Z):X, 
          V3 of (R:Z):X) 
      :- eq(W,Y), graise(V1,V2,V3).

%  b. M rule.
%     a -> b/(b/a).
%     Lower case :   X/Y ; Y/(Y/W).
mable(V1 of X:Y, V2 of W, V3 of X:(Y:W)) :-
      \+ eq(W,Y),mraise(V2,V1,V3).
mable(V1 of W, V2 of X:Y, V3 of X:(Y:W)) :- 
      \+ eq(W,Y),mraise(V1,V2,V3).
%  Upper case :	(X/W)/Y ; (X/(X/W)).
mable(V1 of (X:U):Y, V2 of W, V3 of X : Y)
      :- \+ eq(W,Y), eq(U,W),
         mraise2(V2,V1,V3).
mable(V1 of W, V2 of (X:U):Y, V3 of X : Y)
      :- \+ eq(W,Y), eq(U,W),
         mraise2(V1,V2,V3).

%  Lexical Category Assignment.
lca([],[]).
lca([X|Xs], [Y|Ys]) :-
      dict(X,Y), lca(Xs,Ys).

%  dictionary :
%  for phrase : john walks.
dict(john, john of n).
dict(walks, fun(X, walks(X)) of t:n).

% for phrase : everyone loves someone.
dict(everyone,fun(X, all(X)) of s:fvp).
dict(loves,fun(X, love(X)) of fvp:np).
dict(someone,fun(F,F:somebody) of s:(s:np)).

%  Underlying equational theory for 
%  defining matching. Currently, it's just 
%  first order unification.
eq(X,X).

%  Supporting Lambda Calculus routines.
apply(fun(X,F),D,F)  :- eq(X,D).

compose(fun(X,F), fun(Y,G), fun(Y,F)) :- 
       eq(X,G).

%  M rules : first raise W to fun(Z,Z:W),
%  and then compose with fun(Y,XY) using 
%  the above rule compose/3.
mraise(W,fun(Y,X), fun(Z,X)) :- 
       eq(Y,Z:W).
mraise2(W, fun(Y, fun(U,X)), fun(Y, X)) :-
       eq(U,W).

%  G rules :    This is tricky in terms of 
%   parameter passing by lambda variables. 
%   Improper substitution by the use of 
%   logical variables is carefully coded to 
%   deal with type varibles and renamed 
%   substitution.
graise(fun(Y,X), fun(W,fun(Z,F)), 
      fun(W,fun(Z,XF))) :- eq(Y,F),XF = X.

simple_graise(fun(R,W), fun(YZ,X), 
      fun(R,fun(Z,XW))) :- eq(W,YZ), XW = X.
 

%  Version 3 : 
%    Undirectional + FA + FC + M + G, 
%    together with only parse structure 
%    along with the parsing processing.
:-  op(400, xfy, ':').
:-  op(500, xfy, 'of').

%  Main program.
lambek(Lexicon, Final) :-
        lca(Lexicon, Clist),
        calculus(Clist,Final).

calculus([X],[X]).
calculus([X,Y|Xs],Z) :-
        lc(X,Y,XY),!,
        calculus([XY|Xs],Z).
calculus([X,Y|Xs],[Z]) :-
        calculus([Y|Xs],[YXs]), 
        lc(X,YXs,Z), !.
calculus([X,Y|Xs],Z) :-
        geachable(X,Y,XY),!,
        calculus([XY|Xs],Z).
calculus([X,Y|Xs],Z) :-
        mable(X,Y,XY),!,
        calculus([XY|Xs],Z).

%  Function Application
lc(V1 of F:X,V2 of Y, V3 of F) :- 
        eq(X,Y), apply(V1,V2,V3).
lc(V1 of X, V2 of F:Y, V3 of F)	:- 
        eq(X,Y), apply(V2,V1,V3).

%  Functional Composition
lc(V1 of F:X, V2 of Y : Z, V3 of F:Z) :-
        eq(X,Y),compose(V1,V2,V3).
lc(V1 of Y:Z, V2 of F : X, V3 of F:Z) :-
        eq(X,Y),compose(V2,V1,V3).

%  Type Raising
%  a. Geach Rule
%     a/b ->  (a/c)/(b/c).
%     Lower middle case.
geachable(V1 of X:(Y:Z), V2 of W:R,
          V3 of X:(R:Z)) 
       :- eq(W,Y), simple_graise(V2,V1,V3).
geachable(V1 of W:R, V2 of X:(Y:Z), 
          V3 of X:(R:Z)) 
       :- eq(W,Y),simple_graise(V1,V2,V3).
%  Upper middle case.
geachable(V1 of (Y:Z):X, V2 of R:W, 
          V3 of (R:Z):X)
       :- eq(W,Y), graise(V2,V1,V3).
geachable(V1 of R:W, V2 of (Y:Z):X, 
         V3 of (R:Z):X) 
       :- eq(W,Y), graise(V1,V2,V3).

%  b. M rule.
%     a ->  b/(b/a).
mable(V1 of X:Y, V2 of W, V3 of X:(Y:W)) :-
      \+ eq(W,Y),mraise(V2,V1,V3).
mable(V1 of W, V2 of X:Y, V3 of X:(Y:W)) :- 
      \+ eq(W,Y),mraise(V1,V2,V3).
mable(V1 of (X:U):Y, V2 of W, V3 of X : Y) 
           :- \+ eq(W,Y), eq(U,W), 
              mraise2(V2,V1,V3).
mable(V1 of W, V2 of (X:U):Y, V3 of X:Y) 
           :- \+ eq(W,Y), eq(U,W), 
              mraise2(V1,V2,V3).

%  Lexical Category Assignment.
lca([],[]).
lca([X|Xs], [Y|Ys]) :-	
       dict(X,Y), lca(Xs,Ys).

%  dictionary :
%  for phrase : john walks.
dict(john, john of n).
dict(walks, walks of t:n).

% for phrase : everyone loves someone.
dict(everyone,everyone of s:fvp).
dict(loves,loves of fvp:np).
dict(someone,someone of s:(s:np)).

%  Underlying equational theory for 
%  defining matching. Currently, it's just 
%  first order unification.
eq(X,X).

%  Parse Tree Construction Routines.
apply(F,D,beta(F,D)).

compose(F,G, comp(F,G)).

%  M rules :  Two Cases. 
mraise(W,X, msubcomp(W,X)).

mraise2(W,X, msubcomp(W,X)).

%  G rules :  Two Cases. 
graise(YX, WZF, g1subcomp(YX,WZF)).

simple_graise(RW, ZYX, g2subcomp(ZYX,RW)).