%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                                                                %%
%% (Program 3.12 with still inadequate but saner semantics Mk.II.)%%
%%                                                                %%
%%                                                                %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- op(500, xfy, &).     % A dummy logical conjunction operator
:- op(510, xfy, =>).    % Dummy implication, in case we want to do "every"

%% A predicate is a function NP->S; S is instantiated by `partial
%% execution'.   But the subject is now a function over predicates:
s(S1) --> np(VP^S1), vp(VP).

%% In fact, ALL NPs, even proper names, are functions over properties
%% (so betrand becomes np((bertrand^S)^S), while walks as always yields
%% vp(X^walks(X)).   MAKE SURE YOU UNDERSTAND HOW THIS MAKES THE ABOVE
%% S RULE YIELD S1 = walks(bertrand) BEFORE YOU READ BEYOND THE NEXT LINE):
np((E^S)^S) --> pn(E).

%% The real point of this is to make full NPs do the reight thing with
%% quantifiers (look at the definition of determiners etc
%% below.  They turn it via partial execution into the equivalent of
%% the following: 
%% np((X^S2)^S3) -->
%%      det((X^S1)^(X^S2)^S3), n(X^S0),optrel((X^S0)^(X^S1)).
np(NP) -->
      det(N2^NP), n(N1),optrel(N1^N2).

vp(X^S1) -->                    % NB Here we depart from P&S
      tv(Y^X^S),                    % There is more to this than meets
      np((Y^S)^S1).             % the eye !

vp(VP) -->
      iv(VP).

%% The following bind S0, S1, S2, and S3 in the NP definition:
optrel(N^N) --> [].

optrel((X^S1)^(X^(S1&S2))) -->
      relpron(X), vp(X^S2).

det(LF) --> [Det], {det(Det,LF)}.
det(a,(X^S1)^(X^S2)^exists(X,S1&S2)).
det(the,(X^S1)^(X^S2)^def(X,S1&S2)).
det(some,(X^S1)^(X^S2)^exists(X,S1&S2)).
det(every,(X^S1)^(X^S2)^all(X,S1=>S2)).

n(LF) --> [N], {n(N,LF)}.
n(author,X^author(X)).
n(book,X^book(X)).
n(program,X^program(X)).
n(programmer,X^programmer(X)).
n(professor,X^professor(X)).
n(student,X^student(X)).

pn(E) --> [PN], {pn(PN,E)}.
pn(begriffsschrift,begriffsschrift).
pn(principia,principia).
pn(lunar,lunar).
pn(shrdlu,shrdlu).
pn(bertrand,bertrand).
pn(gottlob,gottlob).
pn(gilbert,gilbert).
pn(george,george).
pn(terry,terry).
pn(bill,bill).

tv(LF) --> [TV], {tv(TV,LF)}.         % NB Here we depart from P&S
tv(concerns,Y^X^concerns(X,Y)).       % Note that this is a more
tv(met,Y^X^met(X,Y)).                 % traditional semantics for TV
tv(ran,Y^X^ran(X,Y)).                 % See the transitive vp defn above
tv(wrote,Y^X^wrote(X,Y)).

iv(LF) --> [IV], {iv(IV,LF)}.
iv(halted,X^halted(X)).
iv(walks,X^walks(X)).

relpron(LF) --> [RelPron], {relpron(RelPron,LF)}.
relpron(that,LF).
relpron(who,LF).
relpron(whom,LF).

\end{verbatim}}

This version behaves better.   For example, given an appropriate database,
including facts like the following --
\begin{verbatim}
halted(shrdlu).
program(shrdlu).
\end{verbatim}
-- we can not only build queries:
\begin{verbatim}
%| ?- [-'hw3c.p'].
%hw3c.p reconsulted 140 bytes 0.0833346 sec.
%
%yes
%| ?- s(T,[some,program,halted],[]).
%
%T = exists(_25,program(_25)&halted(_25)) ;
%
%no
%| ?- s(T,[gilbert, wrote, some,program],[]).
%
%T = exists(_25,program(_25)&wrote(gilbert,_25)) ;
%
%no
\end{verbatim}
--- We can also (given appropriate prolog definitions of 
{\tt exists, \&} etc.) {\em run} them to yield truth values:
{\small
\begin{verbatim}
%| ?- s(T,[some,program,halted],[]), call(T).
%
%T = exists(_25,program(_25)&halted(_25)) 
%
% yes
%| ?- s(T,[some,programmer,halted],[]), call(T)
%
% no
%| ?- s(T,[every,student,that, wrote, some,program,halted],[]).
%
%T = all(_29,student(_29)&exists(_58,program(_58)&wrote(_29,_58))=>halted(_29)
% ;
%
%no
%Note that the program still does not capture the semantics of
%quantifiers completely.  Consider the following example:
%| ?- s(T,[every,student, wrote, some,program],[]).
%
%T = all(_27,student(_27)=>exists(_48,program(_48)&wrote(_27,_48))) ;
%
%no
%The program only yields {\em one} interpretation, whereas there should
%be two.  
%Read Pereira \& Shieber, and Hobbs \& Shieber in the bulk
%pack on this problem and the nature
%of the solution.

exists(X,TerminX) :- \+\+TerminX.