%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Chapter for the Wiley-Blackwell Handbook of Contemporary Semantics
% (Second Edition).
% 
% Chapter:  Implementing Semantic Theories
% Version:  Final
% Author:   Jan van Eijck
% Email:    jve@cwi.nl
% Date:     April 2014
% Comments: Revised 
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\documentclass[pdfextras]{handbook}           % For US-Letter paper
\documentclass[a4paper,pdfextras]{handbook}   % For SO-A4 paper

%% Alternatively, use one of the following if you start to get PDF and
%% hyperref related errors:
%\documentclass{handbook}           % For US-Letter paper
%\documentclass[a4paper]{handbook}  % For ISO-A4 paper

%% You might wish to uncomment the following line if you want to
%% create PDF output using ghostscript or adobe tools on dvips
%% generated Postscript output.
%\PassOptionToPackage{dvips}{hyperref}

%% The following command invokes single-spaced formatting.  You may
%% wish to uncomment it in order to save paper when printing personal
%% working copies.
\setstretch{1.0}

%% Uncomment the next command if you want lingmacros.  Note the
%% "sequential" environment can be used for sequential example
%% numbering (see below).
% \usepackage{lingmacros}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% The following packages are included in this class by default.  
%% Their presence is merely noted here.
%%
%\usepackage{hyperref}           % Useful for adding links and 
%                                % bookmarks to the PDF output.  
%\usepackage[round,sort]{natbib} % advanced bibliography style
%\usepackage{makeidx}            % allows index generation
%\usepackage{graphicx}           % standard LaTeX graphics tool
%                                % for including figure files
%\usepackage{doublespace}        % required by Blackwell
%\usepackage{multicol}           % used for the two-column index
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% Please avoid using unnecessary additional packages as this can
% complicate the final intergration of your chapter into the handbook.

\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{proof}
\usepackage[pdf]{qtree}

\usepackage{fancybox}
\usepackage{calc}

\newcommand{\commentout}[1]{}


\newcommand{\ldb}{\lbrack\!\lbrack}
\newcommand{\rdb}{\rbrack\!\rbrack}

\newcommand{\pow}{{\cal P}}

\newcommand{\NI}{\noindent}

\newcommand{\mi}[1]{\mbox{\it #1}}
\newcommand{\mb}[1]{\mbox{\bf #1}}

\newcommand{\impl}{\rightarrow}

\newcommand{\Var}{{\rm Var\:}}
\newcommand{\Dom}{{\rm Dom\:}}
\newcommand{\Rng}{{\rm Rng\:}}


\usepackage{color}
\definecolor{lightgrey}{gray}{0.55}
\definecolor{darkgrey}{gray}{0.30}


\newcommand{\bc}{\vspace{1em}\noindent\begin{minipage}{\textwidth}\color{darkgrey}%
\rule{\textwidth}{.07ex}\vspace{-0.5em}}
\newcommand{\ec}{\vspace{-1em}\rule{\textwidth}{.07ex}\color{black}\end{minipage}\vspace{1em}}

\newcommand{\bp}{\vspace{1em}\noindent\begin{minipage}{\textwidth}\color{lightgrey}%
\rule{\textwidth}{.07ex}\vspace{-0.5em}}
\newcommand{\ep}{\vspace{-1em}\rule{\textwidth}{.07ex}\color{black}\end{minipage}\vspace{1em}}

\usepackage{tikz}
\usetikzlibrary{trees}
\usepgflibrary{arrows}
\usetikzlibrary{positioning,shapes}
\usetikzlibrary{patterns}

\newsavebox{\fminibox}
\newlength{\fminilength}
\newenvironment{fminipage}[1][\linewidth]
 {\setlength{\fminilength}{#1-2\fboxsep-2\fboxrule-1em}%
 \bigskip\begin{lrbox}{\fminibox}\quad\begin{minipage}{\fminilength}\bigskip}
 {\smallskip\end{minipage}\end{lrbox}\noindent\fbox{\usebox{\fminibox}}\bigskip}

\newenvironment{fminipage2}[1][\linewidth]
 {\setlength{\fminilength}{#1-2\fboxsep-2\fboxrule-1em}%
 \bigskip\begin{lrbox}{\fminibox}\quad\begin{minipage}{\fminilength}\bigskip}
 {\smallskip\end{minipage}\end{lrbox}\noindent\doublebox{\usebox{\fminibox}}\bigskip}

\newcommand{\balg}{\begin{fminipage2}\color{darkgrey}}
\newcommand{\ealg}{\color{black}\end{fminipage2}}

\newcommand{\balgt}[1]{\begin{fminipage2}\color{darkgrey}
\begin{center}{\bf #1}\end{center}}

\newcommand{\ex}[1]{\mbox{}&&\mbox{\em{}#1}}
\newcommand{\sref}[1]{(\ref{#1})}



\makeindex                      % used for the subject index


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
% The following turns on line numbering, which is useful for
% reviewers, proof readers and copy editors. Comment out this line if
% the line numbering causes problems.
\linenumbers

\title*{Implementing Semantic Theories}

% Use \titlerunning{Short Title} for an abbreviated version of
% your contribution title if the original one is too long

\author{Jan van Eijck
\inst{1}
}

% Use \authorrunning{Short Title} for an abbreviated version of
% your contribution title if the original one is too long

\institute{%
   Centrum Wiskunde \&\ Informatica, Science Park 123, 1098 XG Amsterdam, The Netherlands
    \texttt{jve@cwi.nl} \\[2ex]
   ILLC, Science Park 904, 1098 XH Amsterdam, The Netherlands
 }


\maketitle


%\keywords{You can put keywords here if you like, and uncomment this line.}


%Your text goes here. Separate text sections with the standard \LaTeX\
%sectioning commands (\verb+\section{<title>}+ and
%\verb+\subsection{<title>}+.


\section{Introduction}

\paragraph{What is a semantic theory, and why is it useful 
to implement semantic theories?}

In this chapter, a semantic theory is taken to be a 
collection of rules for specifying the interpretation of 
a class of natural language expressions. An example would 
be a theory of how to handle quantification, expressed as 
a set of rules for how to interpret 
determiner expressions like {\em all}, {\em all except one}, 
{\em at least three but no more than ten}. 

It will be demonstrated that implementing such a theory as a program
that can be executed on a computer involves much less effort than is
commonly thought, and has greater benefits than most linguists
assume. Ideally, this Handbook should have example implementations in
all chapters, to illustrate how the theories work, and to demonstrate
that the accounts are fully explicit.

\paragraph{What makes a semantic theory easy or hard to implement?}

What makes a semantic theory easy to implement is formal explicitness
of the framework in which it is stated. Hard to implement are theories
stated in vague frameworks, or stated in frameworks that elude
explicit formulation because they change too often or too quickly. It
helps if the semantic theory itself is stated in more or less formal
terms.

\paragraph{Choosing an implementation language: imperative versus 
declarative} 

Well-designed implementation languages are a key to good software design, 
but while many well designed languages are available, not all kinds of 
language are equally suited for implementing semantic theories. 

Programming languages can be divided very roughly into imperative and
declarative. Imperative programming consists in specifying a sequence
of assignment actions, and reading off computation results from registers. 
Declarative programming consists in defining functions or predicates
and executing these definitions to obtain a result. 
\index{imperative programming}
\index{declarative programming}

Recall the old joke of the computer programmer who died in the shower?
He was just following the instructions on the shampoo bottle:
``Lather, rinse, repeat.'' Following a sequence of instructions to the
letter is the essence of imperative programming.  The joke also has a
version for functional programmers.  The definition on the shampoo
bottle of the functional programmer runs:
\begin{verbatim} 
  wash = lather : rinse : wash 
\end{verbatim}
This is effectively a definition by co-recursion (like definition 
by recursion, but without a base case) of an infinite stream of 
lathering followed by rinsing followed by lathering followed by \ldots. 
\index{co-recursion}  

To be suitable for the representation of semantic theories, an
implementation language has to have good facilities for specifying
{\em abstract data types}. The key feature in specifying abstract data
types is to present a precise description of that data type without
referring to any concrete representation of the objects of that
datatype and to specify operations on the data type 
without referring to any implementation details. 

This abstract point of view is provided by many-sorted algebras.  Many
sorted algebras are specifications of abstract datatypes.  Most
state-of-the art functional programming languages excel here. See
below. An example of an abstract data type would be the specification
of a grammar as a list of context free rewrite rules, say in Backus
Naur form (BNF). \index{Backus Naur Form} \index{BNF}

\paragraph{Logic programming or functional programming: trade-offs}

First order predicate logic can be turned into a computation engine by
adding SLD resolution, unification and fixpoint computation.  The
result is called {\em datalog}.
\index{SLD resolution}
\index{unification}
\index{fixpoint computation}
\index{datalog}
SLD resolution is {\em L}\/inear resolution with a 
{\em S}\/election function for {\em D}\/efinite sentences.
Definite sentences, also called Horn clauses, \index{Horn clauses} 
are clauses with exactly one positive literal. 
An example: 
\[
 \text{father}(x) \lor \neg \text{parent} (x) \lor 
   \neg \text{male} (x). 
\]
This can be viewed as a definition of the predicate {\em father} in 
terms of the predicates {\em parent} and {\em male}, and it 
is usually written as a reverse implication, and using a comma:
\[
  \text{father}(x) \leftarrow \text{parent}(x), \text{male}(x). 
\]
To extend this into a full fledged programming paradigm, backtracking
and cut (an operator for pruning search trees) were added (by Alain
Colmerauer and Robert Kowalski, around 1972). The result is {\em
  Prolog}, short for {\em programmation logique}.  An excellent source
of information on logic programming can be found at
\url{http://vl.fmnet.info/logic-prog/}
\index{Prolog}
\index{Colmerauer, Alain} 
\index{Kowalski, Robert}

Pure lambda calculus was developed in the 1930s and 40s by the logician
Alonzo Church, as a foundational project intended to put mathematics
on a firm basis of `effective procedures'. In the system of pure
lambda calculus, {\em everything}\/ is a function. Functions can be
applied to other functions to obtain values by a process of
application, and new functions can be constructed from existing
functions by a process of lambda abstraction.
\index{Church, Alonzo} 
\index{Pure lambda calculus}

 Unfortunately, the system of pure lambda calculus admits the
 formulation of Russell's paradox.  \index{Russell's paradox}
 Representing sets by their characteristic functions (essentially
 procedures for separating the members of a set from the non-members),
 we can define
\[ 
   r = \lambda x \cdot \neg (x \ x). 
\]
Now apply $r$ to itself: 
\begin{eqnarray*} 
  r \ r & = &  (\lambda x \cdot \neg (x \ x))  
               (\lambda x \cdot \neg (x \ x)) \\
        & = &  \neg ((\lambda x \cdot \neg (x \ x)) 
                     (\lambda x \cdot \neg (x \ x))) \\
        & = &  \neg (r \ r). 
\end{eqnarray*}
So if $(r \ r)$ is true then it is false and vice versa.
This means that pure lambda calculus is not a suitable foundation 
for mathematics. However, as Church and Turing realized, it is 
a suitable foundation for computation. Elements of lambda calculus 
have found their way into a number of programming languages
such as Lisp, Scheme,  ML, Caml, Ocaml, and Haskell.
\index{Lisp}
\index{Scheme}
\index{ML}
\index{Caml}
\index{Ocaml}
\index{Haskell}
 

In the mid-1980s, there was no ``standard'' non-strict,
purely-functional programming language. A language-design committee
was set up in 1987, and the Haskell language is the result.  Haskell
is named after Haskell B. Curry, a logician who has the distinction of
having {\em two}\/ programming languages named after him, {\em
  Haskell} and {\em Curry}.  For general info on functional
programming the reader is referred to
\url{http://www.cs.nott.ac.uk/~gmh/faq.html}.  \index{Curry, Haskell
  B.} A functional language has {\em non-strict evaluation} or {\em
  lazy evaluation} if evaluation of expressions stops `as soon as
possible'.  In particular, only arguments that are necessary for the
outcome are computed, and only as far as necessary. This makes it
possible to handle infinite data structures such as infinite lists. We
will use this below to represent the infinite domain of natural numbers.
\index{lazy evaluation} \index{non-strict evaluation}

A declarative programming language is better than an imperative
programming language for implementing a description of a set of
semantic rules. The two main declarative programming styles that are
considered suitable for implementating computational semantics are
logic programming and functional programming. Indeed, computational
paradigms that emerged in computer science, such as unification and
proof search, found their way into semantic theory, as basic feature
value computation mechanisms and as resolution algorithms for pronoun
reference resolution.

If unification and first order inference play an important role in a
semantic theory, then a logic programming language like Prolog may
seem a natural choice as an implementation language. 
However, while unification and proof search for definite
clauses constitute the core of logic programming (there is hardly more
to Prolog than these two ingredients), functional programming
encompasses the whole world of abstract datatype definition and
polymorphic typing.  As we will demonstrate below, the key ingredients
of logic programming are easily expressed in Haskell, while Prolog is
not very suitable for expressing data abstraction. Therefore, in this
chapter we will use Haskell rather than Prolog as our implementation
language. For a textbook on computational semantics that uses Prolog,
we refer to \cite{BlaBos05:raifnl}. A recent computational semantics
textbook that uses Haskell is \cite{EijckUng10:cswfp}.

Modern functional programming languages such as Haskell are in fact 
implementations of typed lambda calculus with a flexible type 
system. Such languages have polymorphic types, which means that 
functions and operations can apply generically to data. E.g., 
the operation that joins two lists has as its only requirement
that the lists are of the same type $a$ --- where $a$ can 
be the type of integers, the type of characters, the type of lists of 
characters, or any other type ---  and it yields
a result that is again a list of type $a$. 

This chapter will demonstrate, among other things, that implementing a
Montague style fragment in a functional programming language with
flexible types is a breeze: Montague's underlying representation
language is typed lambda calculus, be it without type flexibility, 
so Montague's specifications of natural language fragments
in PTQ \cite{Montague:tptoqi} and UG  \cite{Montague:ug} are 
in fact already specifications of functional programs. Well, almost. 

%\paragraph{Role of first order inference in implementations} 
%
%A Prolog engine is easy to develop in Haskell. A Prolog implementation
% in Haskell written by Mark P.~Jones was once distributed as part of
% the demo programs that came with the Haskell interpreter {\em Hugs}.
% See
% \url{http://darcs.haskell.org/nofib/real/prolog/Examples}.\index{Prolog}
% In a similar way, implementing a basic resolution style or tableau
% style theorem proving engine for first order logic as a functional
% program is not hard. Alternatively, one can hook up an external
% theorem prover.

\paragraph{The role of type theory in implementations} 

If your toolkit has just a hammer in it, then everything looks like a
nail. If your implementation language has built-in unification, it is
tempting to use unification for the composition of expressions that
represent meaning. The Core Language Engine
\cite{Alshawi:tcle,AlsEij:lfitcl} uses unification to construct
logical forms.

For instance, instead of combining noun phrase interpretations with
verb phrase interpretations by means of functional composition, in a
Prolog implementation a verb phrase interpretation typically has a
Prolog variable \verb^X^ occupying a \verb^subjVal^ slot, and the noun
phrase interpretation typically unifies with the \verb^X^. But this
approach will not work if the verb phrase contains more than one
occurrence of \verb^X^. Take the translation of {\em No one was
  allowed to pack and leave}. This does not mean the same as {\em No
  one was allowed to pack and no one was allowed to leave}.  But the
confusion of the two is hard to avoid under a feature unification
approach.

Theoretically, function abstraction and application in a universe of
higher order types are a much more natural choice for logical form
construction. Using an implementation language that is based on type
theory and function abstraction makes it particularly easy to
implement the elements of semantic processing of natural language, as
we will demonstrate below.

\paragraph{Literate Programming} 

This Chapter is written in so-called literate programming style.
Literate programming, as advocated by Donald Knuth in \cite{Knuth:lp},
is a way of writing computer programs where the first and foremost aim
of the presentation of a program is to make it easily accessible
to humans. Program and documentation are in a single file. In fact,
the program source text is extracted from the \LaTeX\ source text of
the chapter. Pieces of program source text are displayed as in the
following Haskell module declaration for this Chapter:

\bc\begin{verbatim}
module IST where 

import Data.List
import Data.Char
import System.IO
\end{verbatim}\ec

This declares a module called {\em IST}, for ``Implementing a Semantic
Theory'', and imports the Haskell library with list processing
routines called {\em Data.List}. 

We will explain most programming constructs that we use, while
avoiding a full blown tutorial. For tutorials and further
background on programming in Haskell we refer the reader to
\url{www.haskell.org}. You are strongly encouraged to 
install the Haskell Platform on your computer, download 
the software that goes with this chapter from 
internet address \url{https://github.com/janvaneijck/ist}, 
and try out the code for yourself. The advantage of developing 
such fragments with the help of a computer is that interacting 
with the code gives us feedback on the clarity and quality 
of our formal notions. 


\section{Logical Form or Direct Interpretation?}  \label{LFdirectSection}

In Montague style semantics, there are two flavours: use of a logical
 form language, as in PTQ \cite{Montague:tptoqi} and UG
 \cite{Montague:ug}, and direct semantic interpretation, as in EAAFL
 \cite{Montague:eaafl}.

To illustrate the distinction, consider the following BNF grammar 
for generalized quantifiers: 
\[
   \text{Det} ::= \text{Every} 
              \mid  \text{All} 
              \mid  \text{Some} 
              \mid  \text{No} 
              \mid  \text{Most}.
\]
The data type definition in the implementation follows this 
to the letter: 

\bc\begin{verbatim}
data Det = Every | All | Some | No | Most
  deriving Show
\end{verbatim}\ec

Let $D$ be some finite domain. Then the
 interpretation of a determiner on this domain can be viewed as a
 function of type $\pow D \to \pow D \to \{ 0, 1 \}$.  Given two
 subsets $P,Q$ of $D$, the determiner relation does or does not hold
 for these subsets. E.g., the quantifier relation \text{All} holds
 between two sets $P$ and $Q$ iff $P \subseteq Q$.  Similarly the
 quantifier relation \text{Most} holds between two finite sets $P$ and
 $Q$ iff $P \cap Q$ has more elements than $P - Q$. 
Let's implement this. First fix a domain: 

\bc\begin{verbatim}
domain = [1..100]
\end{verbatim}\ec

A direct interpretation instruction for ``All'' for this 
domain is given by: 

\bc\begin{verbatim}
intDET :: Det -> (Int -> Bool) -> (Int -> Bool) -> Bool
intDET All =  \ p q -> 
  filter (\x -> p x && not (q x)) domain == []
\end{verbatim}\ec

This says that {\em All} is interpreted as the relation between 
properties $p$ and $q$ that evaluates to {\em True} iff the set of 
objects in the domain that satisfy $p$ but not $q$ is empty. 

A direct interpretation instruction for ``Most'' for this 
domain is given by: 

\bc\begin{verbatim}
intDET Most = \ p q -> 
 let 
   xs = filter (\x -> p x && not (q x)) domain
   ys = filter (\x -> p x && q x) domain
 in length ys > length xs 
\end{verbatim}\ec

This says that {\em Most} is interpreted as the relation between 
properties $p$ and $q$ that evaluates to {\em True} iff the set of 
objects in the domain that satisfy both $p$ and $q$ is larger than 
the set of objects in the domain that satisfy $p$ but not $q$. 
Note that this implementation will only work for finite domains. 

To contrast this with translation into logical form, we define a
datatype for formulas with generalized quantifiers.

Building blocks that we need for that are {\em names} and {\em
  identifiers}\/ (type {\tt Id}\/), which are pairs consisting of a
name (a string of characters) and an integer index.

\bc\begin{verbatim} 
type Name = String
data Id  = Id Name Int deriving (Eq,Ord) 
\end{verbatim}\ec

What this says is that we will use {\em Name} is a synonym for {\em
  String}, and that an object of type {\em Id} will consist of the
identifier {\em Id} followed by a {\em Name} followed by an {\em Int}. 
In Haskell, {\em Int} is the type for fixed-length
integers.  Here are some examples of identifiers:

\bc\begin{verbatim} 
ix = Id "x" 0
iy = Id "y" 0
iz = Id "z" 0
\end{verbatim}\ec 

From now on we can use {\em ix} for \verb^Id "x" 0^, and so on. 
Next, we define terms. Terms are either variables or functions with
 names and term arguments.  First in BNF notation:
\[
  t ::= v_i \mid f_i (t, \ldots, t).
\]
The indices on variables $v_i$ and function symbols $f_i$ 
can be viewed as names. Here is the corresponding data type: 

\bc\begin{verbatim}
data Term = Var Id | Struct Name [Term] deriving (Eq,Ord)
\end{verbatim}\ec 

Some examples of variable terms: 

\bc\begin{verbatim}
x    = Var ix 
y    = Var iy 
z    = Var iz 
\end{verbatim}\ec 

An example of a constant term (a function without arguments): 

\bc\begin{verbatim}
zero :: Term 
zero  = Struct "zero" []
\end{verbatim}\ec

Here, \verb+[]+ is the empty list. 
\index{empty list}

Some examples of function symbols: 

\bc\begin{verbatim}
s     = Struct "s" 
t     = Struct "t"
u     = Struct "u"
\end{verbatim}\ec 

Function symbols can be combined with constants to define so-called
{\em ground terms} (terms without occurrences of variables). 
In the following, we use $s[\ ]$ for the successor function. 

\bc\begin{verbatim}
one   = s[zero]
two   = s[one]
three = s[two]
four  = s[three]
five  = s[four]
\end{verbatim}\ec

The function {\em isVar} checks whether a term is a variable; 
it uses the type {\em Bool} for Boolean (true or false).  
The type specification \verb+Term -> Bool+ says that  {\em isVar}
is a classifier of terms. It classifies the the terms that start
with \verb+Var+ as variables, and all other terms as non-variables. 

\bc\begin{verbatim}
isVar :: Term -> Bool
isVar (Var _) = True
isVar _       = False
\end{verbatim}\ec

The function {\em isGround} checks whether a term is a ground term
(a term without occurrences of variables); it uses the Haskell primitives
{\em and}\/ and {\em map}, which you should look up in a Haskell tutorial
if you are not familiar with them. 

\bc\begin{verbatim}
isGround :: Term -> Bool
isGround (Var _) = False
isGround (Struct _ ts) = and (map isGround ts)
\end{verbatim}\ec

This gives (you should check this for yourself): 

\begin{verbatim} 
*IST> isGround zero
True
*IST> isGround five
True
*IST> isGround (s[x])
False
\end{verbatim}

The functions {\em varsInTerm} and {\em varsInTerms} give the
variables that occur in a term or a term list. Variable lists should
not contain duplicates; the function {\em nub} cleans up the variable
lists. If you are not familiar with {\em nub}, {\em concat} and
function composition by means of $\cdot$, you should look up these
functions in a Haskell tutorial.

\bc\begin{verbatim}
varsInTerm :: Term -> [Id]
varsInTerm (Var i)       = [i]
varsInTerm (Struct _ ts) = varsInTerms ts

varsInTerms :: [Term] -> [Id]
varsInTerms = nub . concat . map varsInTerm
\end{verbatim}\ec 

We are now ready to define formulas from atoms that contain 
lists of terms. First in BNF: 
\[
 \phi ::= A(t,\ldots, t) 
  \mid t = t 
  \mid \neg \phi
  \mid \phi \land \phi
  \mid \phi \lor \phi
  \mid Q_v \phi \phi. 
\]
Here $A(t,\ldots, t)$ is an atom with a list of term arguments. 
In the implementation, the data-type for formulas can look like this: 

\bc\begin{verbatim}
data Formula = Atom Name [Term]
             | Eq Term Term
             | Not Formula 
             | Cnj [Formula]
             | Dsj [Formula]
             | Q Det Id Formula Formula
             deriving Show
\end{verbatim}\ec 

Equality statements \verb+Eq Term Term+ express identities $t_1 =
t_2$.  The \verb+Formula+ data type defines conjunction and
disjunction as lists, with the intended meaning that \verb^Cnj fs^ is
true iff all formulas in \verb^fs^ are true, and that \verb^Dsj fs^ is
true iff at least one formula in \verb^fs^ is true. This will be taken
care of by the truth definition below.

Before we can use this, we have to address a syntactic issue. The
determiner expression is translated into a logical form construction
recipe, and this recipe has to make sure that variables bound by a
newly introduced generalized quantifier are bound properly. The
definition of the \verb^fresh^ function that takes care of this can be
found in the appendix. It is used in the translation into logical form
for the quantifiers:

\bc\begin{verbatim}
lfDET :: Det -> 
         (Term -> Formula) -> (Term -> Formula) -> Formula
lfDET All p q  = Q All i (p (Var i)) (q (Var i)) where 
   i = Id "x" (fresh [p zero, q zero])
lfDET Most p q = Q Most i (p (Var i)) (q (Var i)) where 
   i = Id "x" (fresh [p zero, q zero])
lfDET Some p q = Q Some i (p (Var i)) (q (Var i)) where 
   i = Id "x" (fresh [p zero, q zero])
lfDET No p q = Q No i (p (Var i)) (q (Var i)) where 
   i = Id "x" (fresh [p zero, q zero])
\end{verbatim}\ec

Note that the use of a fresh index is essential. If an index \verb^i^
 is not fresh, this means that it is used by a quantifier somewhere
 inside \verb^p^ or \verb^q^, which gives a risk that if these
 expressions of type \verb^Term -> Formula^ are applied to
 \verb^Var i^, occurrences of this variable may get bound by the wrong
 quantifier expression.

Of course, the task of providing formulas of the form {\em All} $v\ 
\phi_1 \phi_2$ or the form {\em Most} $v \ \phi_1 \phi_2$ with the
correct interpretation is now shifted to the truth definition for the
logical form language. We will turn to this in the next Section. 

\section{Model Checking Logical Forms} \label{MCLogicalFormsSection}

The example formula language from Section \ref{LFdirectSection} is
first order logic with equality and the generalized quantifier {\em
  Most}. This is a genuine extension of first order logic with
equality, for it is proved in \cite{BarCoo:gqanl} that {\em Most} is
not expressible in first order logic.

Once we have a logical form language like this, we can dispense with
extending this to a higher order typed version, and instead use the
implementation language to construct the higher order types.

Think of it like this. For any type $a$, the implementation language
 gives us properties (expressions of type $a \to \text{Bool}$),
 relations (expressions of type $a \to a \to \text{Bool}$), higher
 order relations (expressions of type $(a \to \text{Bool}) \to (a \to
 \text{Bool}) \to \text{Bool}$), and so on. Now replace the type of
 Booleans with that of logical forms or formulas (call it $F$), and
 the type $a$ with that of terms (call it $T$).  Then the type $T \to
 F$ expresses an LF property, the type $T \to T \to F$ an LF relation,
 the type $(T \to F) \to (T \to F) \to F$ a higher order relation,
 suitable for translating generalized quantifiers, and so on.

For example, the LF translation of the generalized quantifier {\em
   Most} in Section \ref{LFdirectSection}, produces an expression of
 type $(T \to F) \to (T \to F) \to F$.

Tarski's famous truth definition for first order logic
\cite{Tarski:tcotit} has as key ingredients variable 
assignments, interpretations for predicate symbols, and 
interpretations for function symbols, and proceeds by recursion on 
the structure of formulas. 
\index{Tarski, Alfred}
\index{truth definition of Tarski} 

A domain of discourse $D$ together with an interpretation function $I$ 
that interprets predicate symbols as properties or relations on $D$, 
and function symbols as functions on $D$, is called a {\em first order
model}. 
\index{first order model}

In our implementation, we have to distinguish between the interpretation 
for the predicate letters and that for the function symbols, for they 
have different types: 

\bc\begin{verbatim}
type Interp a  = Name -> [a] -> Bool
type FInterp a = Name -> [a] -> a
\end{verbatim}\ec

These are polymorphic declarations: the type \verb^a^ can be anything.
  Suppose our domain of entities consists of integers. Let us say we
 want to interpret on the domain of the natural numbers. Then the
 domain of discourse is infinite. Since our implementation language 
has non-strict evaluation, we can handle infinite lists. The domain 
of discourse is given by: 

\bc\begin{verbatim}
naturals :: [Integer]
naturals = [0..]
\end{verbatim}\ec

The type \verb+Integer+ is for integers of arbitrary size. 
Other domain definitions are also possible. Here is an example of 
a finite number domain, using the fixed size data type \verb+Int+: 

\bc\begin{verbatim}
numbers :: [Int]
numbers = [minBound..maxBound]
\end{verbatim}\ec

Before we can turn to evaluation of formulas, we have to 
construct valuation functions of type \verb^Term -> a^, 
given appropriate interpretations for function symbols, 
and given an assignment to the variables that occur in terms. 

A variable assignment is a function of type \verb^Id -> a^, where 
\verb^a^ is the type of the domain of interpretation. The term lookup 
function takes a variable assigment and a function symbol interpretation 
as inputs, and constructs a term assignment, as follows. 

\bc\begin{verbatim}
tVal :: FInterp a -> (Id -> a) -> Term -> a
tVal fint g (Var v)         = g v
tVal fint g (Struct str ts) = 
           fint str (map (tVal fint g) ts)
\end{verbatim}\ec 

{\em tVal} computes a value (an entity in the domain of discourse) for
 any term, on the basis of an interpretation for the function symbols
 and an assigment of entities to the variables. Understanding how this
 works is one of the keys to understanding the truth definition for first
 order predicate logic, as it is explained in textbooks of logic. Here
 is the explanation:
\begin{itemize} 
\item If the term is a variable, {\em tVal} borrows its value 
from the assignment {\em g} for variables. 
\item If the term is a function symbol followed by a list of 
terms, then {\em tVal} is applied recursively to the term list, 
which gives a list of entities, and next the interpretation for the function
symbol is used to map this list to an entity. 
\end{itemize} 
Example use: \verb^fint1^ gives an interpretation to the function
 symbol \verb^s^ while \verb^(\ _ -> 0)^ is the anonymous function
 that maps any variable to $0$. The result of applying this to the
 term {\em five} (see the definition above) gives the expected value:
\begin{verbatim}
*IST> tVal fint1 (\ _ -> 0) five
5
\end{verbatim}

The truth definition of Tarski assumes a relation interpretation, 
a function interpretation and a variable assigment, and defines 
truth for logical form expression by recursion on the structure of 
the expression. 

Given a structure with interpretation function $M\! = \! (D, I)$, 
we can define a valuation for the predicate logical formulas, provided 
we know how to deal with the values of individual variables. Let $V$
be the set of variables of the language. A function $g\colon V \to D$ is 
called a {\em variable assignment} or {\em valuation}. 
\index{variable assignment} \index{valuation}

We use $g[v:=d]$ for the valuation that is like $g$ except for the
fact that $v$ gets value $d$ (where $g$ might have assigned a
different value). For example, let $D = \{ 1, 2, 3 \}$ be the domain
of discourse, and let $V = \{ v_1, v_2, v_3 \}$.  Let $g$ be given by
$g(v_1) = 1, g(v_2) = 2, g(v_3) = 3$.  Then $g[v_1:=2]$ is the
valuation that is like $g$ except for the fact that $v_1$ gets the
value $2$, i.e. the valuation that assigns $2$ to $v_1$, $2$ to $v_2$,
and $3$ to $v_3$.

Here is the implementation of $g[v:= d]$: 

\bc\begin{verbatim}
change :: (Id -> a) -> Id -> a -> Id -> a 
change g v d = \ x -> if x == v then d else g x
\end{verbatim}\ec

Let $M = (D,I)$ be a model for language $L$, i.e., $D$ is the domain
of discourse, $I$ is an interpretation function for predicate letters
and function symbols. Let $g$ be a variable assignment for $L$ in
$M$. Let $F$ be a formula of our logical form language.

Now we are ready to define the notion $M \models_g F$, for $F$ is true
in $M$ under assignment $g$, or: $g$ satisfies $F$ in model $M$.  We
assume $P$ is a one-place predicate letter, $R$ is a two-place
predicate letter, $S$ is a three-place predicate letter. Also, we 
use $\ldb t \rdb^I_g$ as the term interpretation of $t$ under $I$ 
and $g$. With this notation, Tarski's truth definition can be 
stated as follows: 
\[ 
\begin{array}{lll} 
M \models_g Pt & \mbox{ iff } & \ldb t \rdb^I_g \in I(P) \\
M \models_g R(t_1,t_2) & \mbox{ iff } & 
   (\ldb t_1 \rdb^I_g, \ldb t_2 \rdb^I_g) \in I(R) \\
M \models_g S(t_1,t_2,t_3) & \mbox{ iff } & 
   (\ldb t_1 \rdb^I_g, \ldb t_2 \rdb^I_g, \ldb t_3 \rdb^I_g) \in I(S) \\
M \models_g (t_1 = t_2) & \mbox{ iff } & 
  \ldb t_1 \rdb^I_g = \ldb t_2 \rdb^I_g   \\
M \models_g \neg F & \mbox{ iff } & 
\text{ it is not the case that } M \models_g F. \\
M \models_g (F_1 \land F_2) & \mbox{ iff } & 
  M \models_g F_1 \text{ and } M \models_g F_2 \\
M \models_g (F_1 \lor F_2) & \mbox{ iff } & 
  M \models_g F_1 \mbox{ or } M \models_g F_2 \\
M \models_g Q v F_1  F_2 & \mbox{ iff } & 
  \{ d \mid  M \models_{g[v:=d]} F_1  \} \text{ and } 
   \{ d \mid  M \models_{g[v:=d]} F_2 \} \\
 & & \text{are in the relation specified by } Q 
\end{array} 
\] 
What we have presented just now is a recursive definition of truth 
for our logical form language. The `relation specified by $Q$' in the
last clause refers to the generalized quantifier interpretations for 
{\em all}, {\em some}, {\em no} and {\em most}. Here is an implementation
of quantifiers are relations: 

\bc\begin{verbatim}
qRel :: Eq a => Det -> [a] -> [a] -> Bool
qRel All xs ys = all (\x -> elem x ys) xs 
qRel Some xs ys = any (\x -> elem x ys) xs 
qRel No xs ys = not (qRel Some xs ys) 
qRel Most xs ys = 
  length (intersect xs ys) > length (xs \\ ys)
\end{verbatim}\ec

If we evaluate closed formulas --- formulas without free variables ---
 the assignment $g$ is irrelevant, in the sense that any $g$ gives the
 same result. So for closed formulas $F$ we can simply define $M
 \models F$ as: $M \models_g F$ for some variable assignment $g$.  But
 note that the variable assignment is still crucial for the truth
 definition, for the property of being closed is not inherited by the
 components of a closed formula.

Let us look at how to implement an evaluation function.
\index{evaluation function} It takes as its first argument a domain,
as its second argument a predicate interpretation function, as its
third argument a function interpretation function, as its fourth
argument a variable assignment, as its fifth argument a formula, and
it yields a truth value. It is defined by recursion on the structure
of the formula.  The type of the evaluation function \verb^eval^
reflects the above assumptions.  \index{evaluation
  function!eval@\verb^eval^|(}

\bc\begin{verbatim}
eval :: Eq a   => 
    [a]        -> 
    Interp a   -> 
    FInterp a  -> 
    (Id -> a)  -> 
    Formula    -> Bool
\end{verbatim}\ec

The evaluation function is defined for all types \verb^a^ that belong
 to the class \verb^Eq^. The assumption that the type \verb^a^ of the
 domain of evaluation is in \verb^Eq^ is needed in the evaluation
 clause for equalities.  The evaluation function takes a universe
 (represented as a list, \verb^[a]^) as its first argument, an
 interpretation function for relation symbols (\verb^Interp a^) as its
 second argument, an interpretation function for function symbols as
 its third argument, a variable assignment (\verb^Id -> a^) as its
 fourth argument, and a formula as its fifth argument. The definition
 is by structural recursion on the formula:

\bc\begin{verbatim}
eval domain i fint = eval' where 
  eval' g (Atom str ts)  = i str (map (tVal fint g) ts)
  eval' g (Eq   t1 t2)   = tVal fint g t1 == tVal fint g t2
  eval' g (Not  f)       = not (eval' g f)
  eval' g (Cnj fs)       = and (map (eval' g) fs)
  eval' g (Dsj fs)        = or  (map (eval' g) fs)
  eval' g (Q det v f1 f2)  = let 
     restr = [ d | d <- domain, eval' (change g v d) f1 ]
     body  = [ d | d <- domain, eval' (change g v d) f2 ]
   in qRel det restr body
\end{verbatim}\ec
\index{evaluation function!eval@\verb^eval^|)}

This evaluation function can be used to check the
truth of formulas in appropriate domains. The domain 
does not have to be finite. Suppose we want to check 
the truth of ``There are even natural numbers''. 
Here is the formula: 

\bc\begin{verbatim}
form0 = Q Some ix (Atom "Number" [x]) (Atom "Even" [x])
\end{verbatim}\ec

We need an interpretation for the predicates ``Number'' and ``Even''. 
We also throw in an interpretation for ``Less than'': 

\bc\begin{verbatim}
int0 :: Interp Integer
int0 "Number" = \[x] -> True
int0 "Even"   = \[x] -> even x
int0 "Less_than" = \[x,y] -> x < y 
\end{verbatim}\ec

We don't need to interpret function symbols, so any function
interpretation will do, for this example.  But for other examples we
want to give names to certain numbers, using the constants ``zero'',
``s'', ``plus'', ``times''. Here is a suitable term interpretation
function for that:

\bc\begin{verbatim}
fint0 :: FInterp Integer
fint0 "zero"  []    = 0
fint0 "s"     [i]   = succ i
fint0 "plus"  [i,j] = i + j 
fint0 "times" [i,j] = i * j 
\end{verbatim}\ec

Note the distinction between syntax (expressions like ``plus'' and 
``times'') and semantics (operations like \verb^+^ and \verb^*^). 

\begin{verbatim}
*IST> eval naturals int0 fint0 (\ _ -> 0) form0
True
\end{verbatim}

This used a variable assigment that maps any variable to $0$. 

Now suppose we want to evaluate the following formula: 

\bc\begin{verbatim}
form1 = Q All ix (Atom "Number" [x]) 
          (Q Some iy (Atom "Number" [y]) 
                     (Atom "Less_than" [x,y]))
\end{verbatim}\ec

This says that for every number there is a larger number, which
as we all know is true on the natural numbers. But this fact cannot 
be established by model checking. The following computation does 
not halt: 

\begin{verbatim}
*IST> eval naturals int0 fint0 (\ _ -> 0) form1
...
\end{verbatim}

This illustrates that model checking on the natural numbers is 
undecidable. Still, many useful facts can be checked, and new 
relations can be defined in terms of a few primitive ones. 

Suppose we want to define the relation ``divides''. A natural 
number $x$ divides a natural number $y$ if there is a number 
$z$ with the property that $x*z = y$. This is easily defined, 
as follows: 

\bc\begin{verbatim}
divides :: Term -> Term -> Formula
divides m n = Q Some iz (Atom "Number" [z]) 
              (Eq n (Struct "times" [m,z]))
\end{verbatim}\ec

This gives: 

\begin{verbatim}
*IST> eval naturals int0 fint0 (\ _ -> 0) (divides two four)
True
\end{verbatim}

The process of defining truth for expressions of natural language is
similar to that of evaluating formulas in mathematical models.
Differences are that the models may have more internal structure than
mathematical domains, and that substantial vocabularies need to be
interpreted.

\paragraph{Interpretation of Natural Language Fragments} 

Where in mathematics it is enough to specify the meanings of `less
than', `plus' and `times', and next define notions like `even', `odd',
`divides', `prime', `composite', in terms of these primitives, in
natural language understanding there is no such privileged core
lexicon. This means we need interpretations for all non-logical items
in the lexicon of a fragment.

To give an example, assume that the domain of discourse is a finite 
set of entities. Let the following data type be given. 

\bc\begin{verbatim}
data Entity = A | B | C | D | E | F | G
            | H | I | J | K | L | M 
     deriving (Eq,Show,Bounded,Enum)
\end{verbatim}\ec

Now we can define entities as follows: 

\bc\begin{verbatim}
entities :: [Entity]
entities =  [minBound..maxBound] 
\end{verbatim}\ec

Now, proper names will simply be interpreted as entities.

\bc\begin{verbatim}
alice, bob, carol :: Entity
alice      = A
bob        = B
carol      = C 
\end{verbatim}\ec

Common nouns such as \emph{girl} and \emph{boy} as well as
intransitive verbs like \emph{laugh} and \emph{weep} are interpreted as
properties of entities.  Transitive verbs like \emph{love} and \emph{hate} 
are interpreted as relations between entities.

Let's define a type for predications:

\bc\begin{verbatim}
type Pred a = [a] -> Bool
\end{verbatim}\ec

Some example properties: 

\bc\begin{verbatim}
girl, boy :: Pred Entity
girl = \ [x] -> elem x [A,C,D,G]
boy  = \ [x] -> elem x [B,E,F]
\end{verbatim}\ec

Some example binary relations: 

\bc\begin{verbatim}
love, hate :: Pred Entity
love = \ [x,y] -> elem (x,y) [(A,A),(A,B),(B,A),(C,B)]
hate = \ [x,y] -> elem (x,y) [(B,C),(C,D)]
\end{verbatim}\ec

And here is an example of a ternary relation:

\bc\begin{verbatim}
give, introduce :: Pred Entity
give = \ [x,y,z] -> elem (x,y,z) [(A,H,B),(A,M,E)]
introduce = \ [x,y,z] -> elem (x,y,z) [(A,A,B),(A,B,C)]
\end{verbatim}\ec

The intention is that the first element in the list specifies the giver, 
the second element the receiver, and the third element what is given. 

Once we have this we can specify operations on predications. 
A simple example is passivization, which is a process of 
argument reduction: the agent of an action is dropped. 
Here is a possible implementation: 

\bc\begin{verbatim}
passivize :: [a] -> Pred a -> Pred a 
passivize domain r = \ [x] -> any (\ y -> r [y,x]) domain
\end{verbatim}\ec

Let's check this out: 

\begin{verbatim}
*IST> :t (passivize entities love)
(passivize entities love) :: Pred Entity
*IST> filter (\ x -> passivize entities love [x]) entities
[A,B]
\end{verbatim}

This version does not work for ternary predicates, but the 
following more general version does: 

\bc\begin{verbatim}
passivize' :: [a] -> Pred a -> Pred a 
passivize' domain r = \ xs -> any (\ y -> r (y:xs)) domain
\end{verbatim}\ec

Here is the illustration: 

\begin{verbatim}
*IST> :t (passivize' entities give)
(passivize' entities give) :: Pred Entity
*IST> filter (passivize' entities give) 
         [[x,y] | x <- entities, y <- entities]
[[H,B],[M,E]]
\end{verbatim}

Another example of argument reduction in natural languages is
 reflexivization. The view that reflexive pronouns are relation
 reducers is folklore among logicians, but can also be found in
 linguistics textbooks, such as Daniel B\"uring's book on Binding
 Theory \cite[pp.\,43--45]{Buering2005}.

Under this view, reflexive pronouns like \emph{himself} and
\emph{herself} differ semantically from non-reflexive pronouns like
\emph{him} and \emph{her} in that they are not interpreted as
individual variables. Instead, they denote argument reducing
functions.  Consider, for example, the following sentence:
\begin{eqnarray} 
\ex{Alice loved herself.}
\end{eqnarray}
The reflexive \emph{herself} is interpreted as a function that takes
the two-place predicate \emph{loved} as an argument and turns it into
a one-place predicate, which takes the subject as an argument and
expressing that this entity loves itself.  This can be achieved by
the following function \verb^self^.

\bc\begin{verbatim}
self ::  Pred a -> Pred a 
self r = \ (x:xs) -> r (x:x:xs)
\end{verbatim}\ec
\index{self@\verb^self^}

Here is an example application: 

\begin{verbatim}
*IST> :t (self love)
(self love) :: Pred Entity
*IST> :t  \ x -> self love [x]
\ x -> self love [x] :: Entity -> Bool
*IST> filter (\ x -> self love [x]) entities
[A]
\end{verbatim}

This approach to reflexives has two desirable consequences.  The first
one is that the locality of reflexives immediately falls out. Since
\verb^self^ is applied to a predicate and unifies arguments of this
predicate, it is not possible that an argument is unified with a
non-clause mate.  So in a sentence like \sref{nonclausemate}, {\em
  herself} can only refer to {\em Alice} but not to {\em Carol}.
\begin{eqnarray}
\ex{Carol believed that Alice loved herself.} \label{nonclausemate}
\end{eqnarray}
 The second one is that it also immediately follows that
 reflexives in subject position are out.
\begin{eqnarray}
\ex{$^\ast$ Herself loved Alice.}
\end{eqnarray}
Given a compositional interpretation, we first apply the predicate
\emph{loved} to \emph{Alice}, which gives us the one-place predicate
$\lambda [x] \mapsto \text{love } [x,a]$. Then trying to apply the function
\verb^self^ to this will fail, because it expects at least two
arguments, and there is only one argument position left. 

Reflexive pronouns can also be used to reduce ditransitive verbs
to transitive verbs, in two possible ways: the reflexive can be 
the direct object or the indirect object: 
\begin{eqnarray}
\ex{Alice introduced herself to Bob.} \\
\ex{Bob gave the book to himself.} 
\end{eqnarray}
The first of these is already taken care of by the reduction operation
above. For the second one, here is an appropriate reduction function:

\bc\begin{verbatim}
self' ::  Pred a -> Pred a 
self' r = \ (x:y:xs) -> r (x:y:x:xs)
\end{verbatim}\ec

Quantifier scope ambiguities can be dealt with in several ways.  From
 the point of view of type theory it is attractive to view sequences
 of quantifiers as functions from relations to truth values. E.g., the
 sequence ``every man, some woman'' takes a binary relation $\lambda x y
 \cdot R[x,y]$ as input and yields {\em True} if and only if it is the
 case that for every man $x$ there is some woman $y$ for which
 $R[x,y]$ holds. To get the reversed scope reading, just swap the
 quantifier sequence, and transform the relation by swapping the first 
two argument places, as follows: 

\bc\begin{verbatim}
swap12 :: Pred a -> Pred a
swap12 r = \ (x:y:xs) -> r (y:x:xs)
\end{verbatim}\ec

So scope inversion can be viewed as a joint operation on quantifier
sequences and relations. See \cite[Chapter 10]{EijckUng10:cswfp} for a
full-fledged implementation and for further discussion.

\section{Example: Implementing Syllogistic Inference}  \label{SylSection}

As an example of the process of implementing inference for
 natural language, let us view the language of the Aristotelian
 syllogism as a tiny fragment of natural language. Compare 
the chapter by Larry Moss on Natural Logic in this Handbook. 
\index{natural logic}
\index{Moss, Larry} The treatment in this Section is an improved 
version of the implementation in \cite[Chapter 5]{EijckUng10:cswfp}. 

The Aristotelian quantifiers are given in the following well-known
 square of opposition:

\begin{center}
\setlength{\unitlength}{1 mm}
\begin{picture}(45,50)
\thicklines
 \put(0,42){\makebox(0,0)[b]{All A are B}}
 \put(40,42){\makebox(0,0)[b]{No A are B}}
 \put(0,2){\makebox(0,0)[b]{Some A are B}}
 \put(40,2){\makebox(0,0)[b]{Not all A are B}}
 \put(0,38){\line(3,-2){40}}
 \put(40,38){\line(-3,-2){40}}
\end{picture}
\end{center}

Aristotle interprets his quantifiers with existential import: 
{\em All A are B}\/ and {\em No A are B}
are taken to imply that there are {\em A}.

What can we ask or state with the Aristotelian quantifiers? The following 
grammar gives the structure of queries and statements (with PN for plural nouns): 

\begin{eqnarray*}
Q & ::= & \text{ Are all} \ \text{PN} \ \text{PN} ? \\
     & | & \text{ Are no} \ \text{PN} \ \text{PN} ? \\
     & | & \text{ Are any} \ \text{PN} \ \text{PN} ? \\
     & | & \text{ Are any} \ \text{PN} \ \text{not} \ \text{PN} ? \\
     & | & \text{ What about } \ \text{PN} ?
\end{eqnarray*}
\begin{eqnarray*}
S & ::= & \text{ All} \ \text{PN} \ \text{are} \ \text{PN} . \\
     & | & \text{ No} \ \text{PN} \ \text{are} \ \text{PN} . \\
     & | & \text{ Some} \ \text{PN} \ \text{are} \ \text{PN} . \\
     & | & \text{ Some} \ \text{PN} \ \text{are not} \
     \text{PN} . 
\end{eqnarray*}

The meanings of the Aristotelean quantifiers can be given in terms of 
set inclusion and set intersection, as follows: 
\begin{itemize}
\item {\bf ALL}: Set inclusion 
\item {\bf SOME}: Non-empty set intersection 
\item {\bf NOT ALL}: Non-inclusion 
\item {\bf NO}: Empty intersection 
\end{itemize}

Set inclusion: $A \subseteq B$ holds if and only if every element of
 $A$ is an element of $B$.  Non-empty set intersection: $A \cap B \neq
 \emptyset$ if and only if there is some $x \in A$ with $x \in B$.
  Non-empty set intersection can can expressed in terms of inclusion,
 negation and complementation, as follows: $A \cap B \neq \emptyset$
 if and only if $A \not\subseteq \overline{B}$.

 To get a sound and complete inference system for this, we use the
 following {\bf Key Fact:} A finite set of syllogistic forms $\Sigma$
 is unsatisfiable if and only if there exists an existential form
 $\psi$ such that $\psi$ taken together with the universal forms from
 $\Sigma$ is unsatisfiable.

 This restricted form of satisfiability can easily be tested with
 propositional logic.  Suppose we talk about the properties of a
 single object $x$.  Let proposition letter $a$ express that object
 $x$ has property $A$.  Then a universal statement ``All $A$ are $B$''
 gets translated as $a \rightarrow b$.  An existential statement
 ``Some $A$ is $B$'' gets translated as $a \land b$.

For each property $A$ we use a single proposition letter $a$. 
We have to check for {\em each} existential statement whether it 
is satisfiable when taken together with all universal statements. 
To test the satisfiability of a set of syllogistic statements with 
$n$ existential statements we need $n$ checks. 

\paragraph{Literals, Clauses, Clause Sets}

A {\em literal} is a propositional letter or its negation.
A {\em clause} is a set of literals. 
A {\em clause set}  is a set of clauses. 

Read a clause as a {\em disjunction} of its literals, and a clause set
as a {\em conjunction} of its clauses. 

Represent the propositional formula 
\[
(p \rightarrow q) \land (q \rightarrow r)
\]
as the following clause set: 
\[
  \{ \{ \neg p, q \}, \{ \neg q, r \} \}. 
\]
Here is an inference rule for clause sets: {\em unit propagation}

\balgt{Unit Propagation}
If one member of a clause set is a singleton $\{ l \}$, then: 

\begin{itemize}
\item remove every other clause containing $l$ from the clause set; 

\item remove $\overline{l}$ from every clause in which it occurs. 
\end{itemize}
\ealg

The result of applying this rule is a simplified equivalent clause set. 
For example, unit propagation for $\{ p \}$ to 
\[
  \{ \{ p \} , \{ \neg p, q \}, \{ \neg q, r \}, \{ p ,  s \} \}
\]
yields 
\[ 
   \{ \{ p \}, \{ q \}, \{ \neg q, r \} \}. 
\]
Applying unit propagation for $\{ q \}$ to this result yields: 
\[
   \{ \{ p \}, \{ q \}, \{ r \} \}. 
\]
The {\em Horn fragment} of propositional logic consists of all 
clause sets where every clause has {\em at most one positive literal}. 
Satisfiability for syllogistic forms containing exactly one
existental statement translates to the Horn fragment of propositional logic.
HORNSAT is the problem of testing Horn clause sets for satisfiability. 
Here is an algorithm for HORNSAT: 

\balgt{HORNSAT Algorithm}
\begin{itemize} 
\item 
If unit propagation yields a clause set in which units 
$\{ l \}, \{ \overline{l} \}$ occur, the original clause set is unsatisfiable.

\item 
Otherwise the units in the result determine a satisfying valuation. \\
%
Recipe: for all units $\{ l \}$ occurring in the final clause set, 
map their proposition letter to the truth value that makes $l$ true. 
Map all other proposition letters to false. 
\end{itemize} 
\ealg

Here is an implementation. The definition of literals: 

\bc\begin{verbatim}
data Lit = Pos Name | Neg Name deriving Eq

instance Show Lit where 
  show (Pos x) = x
  show (Neg x) = '-':x

neg :: Lit -> Lit 
neg (Pos x) = Neg x
neg (Neg x) = Pos x

\end{verbatim}\ec

We can represent a clause as a list of literals: 

\bc\begin{verbatim}
type Clause = [Lit]
\end{verbatim}\ec

The names occurring in a list of clauses: 

\bc\begin{verbatim} 
names :: [Clause] -> [Name]
names = sort . nub . map nm . concat
  where nm (Pos x) = x
        nm (Neg x) = x
\end{verbatim}\ec

The implementation of the unit propagation algorithm: 
propagation of a single unit literal: 

\bc\begin{verbatim}
unitProp :: Lit -> [Clause] -> [Clause]
unitProp x cs = concat (map (unitP x) cs)

unitP :: Lit -> Clause -> [Clause]
unitP x ys = if elem x ys then []
              else 
               if elem (neg x) ys 
                then [delete (neg x) ys]
                else [ys]
\end{verbatim}\ec

The property of being a unit clause: 

\bc\begin{verbatim}
unit :: Clause -> Bool
unit [x] = True 
unit  _  = False
\end{verbatim}\ec

Propagation has the following type, where the Maybe expresses that 
the attempt to find a satisfying valuation may fail. 

\bc\begin{verbatim}
propagate :: [Clause] -> Maybe ([Lit],[Clause])
\end{verbatim}\ec

The implementation uses an auxiliary function \verb^prop^ with 
three arguments. The first argument gives the literals 
that are currently mapped to True, the second argument gives 
the literals that occur in unit clauses, the third argument 
gives the non-unit clauses. 

\bc\begin{verbatim}
propagate cls = 
  prop [] (concat (filter unit cls)) (filter (not.unit) cls) 
  where
    prop :: [Lit] -> [Lit] -> [Clause] 
            -> Maybe ([Lit],[Clause])
    prop xs [] clauses = Just (xs,clauses)
    prop xs (y:ys) clauses = 
      if elem (neg y) xs
       then Nothing
       else prop (y:xs)(ys++newlits) clauses' where 
        newclauses = unitProp y clauses
        zs         = filter unit newclauses
        clauses'   = newclauses \\ zs
        newlits    = concat zs
\end{verbatim}\ec

\paragraph{Knowledge bases}

A knowledge base is a pair, with as first element the clauses
that represent the universal statements, and as second element 
a lists of clause lists, consisting of one clause list per 
existential statement. 

\bc\begin{verbatim}
type KB = ([Clause],[[Clause]])
\end{verbatim}\ec

The intention is that the first element represents the 
universal statements, while the second element has 
one clause list per existential statement. 

The universe of a knowledge base is the list of all classes that are
 mentioned in it. We assume that classes are literals:

\bc\begin{verbatim}
type Class = Lit

universe :: KB -> [Class]
universe (xs,yss) = 
  map (\ x -> Pos x) zs ++ map (\ x -> Neg x) zs
    where zs = names (xs ++ concat yss)
\end{verbatim}\ec

Statements and queries according to the grammar given above: 

\bc\begin{verbatim}
data Statement = 
     All1  Class   Class | No1     Class Class 
   | Some1 Class   Class | SomeNot Class Class 
   | AreAll Class Class  | AreNo   Class Class 
   | AreAny Class Class  | AnyNot  Class Class
   | What   Class 
  deriving Eq
\end{verbatim}\ec

Statement Display: 

\bc\begin{verbatim}
instance Show Statement where 
  show (All1 as bs)     = 
    "All "  ++ show as ++ " are " ++ show bs ++ "."
  show (No1 as bs)      = 
    "No "   ++ show as ++ " are " ++ show bs ++ "."
  show (Some1 as bs)    = 
    "Some " ++ show as ++ " are " ++ show bs ++ "."
  show (SomeNot as bs) = 
    "Some " ++ show as ++ " are not " ++ show bs ++ "."
  show (AreAll as bs)  = 
    "Are all " ++ show as ++ show bs ++ "?"
  show (AreNo as bs)   = 
    "Are no "  ++ show as ++ show bs ++ "?"
  show (AreAny as bs)  = 
    "Are any " ++ show as ++ show bs ++ "?"
  show (AnyNot as bs)  = 
    "Are any " ++ show as ++ " not " ++ show bs ++ "?"
  show (What as)       = "What about " ++ show as ++ "?"
\end{verbatim}\ec

Statement classification: 

\bc\begin{verbatim}
isQuery :: Statement -> Bool
isQuery (AreAll _ _)  = True
isQuery (AreNo _ _)   = True
isQuery (AreAny _ _)  = True
isQuery (AnyNot _ _)  = True
isQuery (What _)      = True
isQuery  _            = False
\end{verbatim}\ec

Query negation: 

\bc\begin{verbatim}
negat :: Statement -> Statement
negat (AreAll as bs) = AnyNot as bs
negat (AreNo  as bs) = AreAny as bs
negat (AreAny as bs) = AreNo  as bs
negat (AnyNot as bs) = AreAll as bs
\end{verbatim}\ec

The $\subset$ Relation: 

\bc\begin{verbatim}
subsetRel :: KB -> [(Class,Class)]
subsetRel kb = 
  [(x,y) | x <- classes, y <- classes, 
     propagate ([x]:[neg y]: fst kb) == Nothing ]
    where classes = universe kb
\end{verbatim}\ec

If $R \subseteq A^2$ and $x\in A$, then $xR := \{ y \mid (x,y) \in R\}$.
This is called a {\em right section of a relation}. 

\bc\begin{verbatim}
rSection :: Eq a => a -> [(a,a)] -> [a] 
rSection x r = [ y | (z,y) <- r, x == z ]
\end{verbatim}\ec

The supersets of a class are given by a right section of the subset
relation, that is, the supersets of a class are all classes of which
it is a subset.

\bc\begin{verbatim}
supersets :: Class -> KB -> [Class]
supersets cl kb = rSection cl (subsetRel kb)
\end{verbatim}\ec

The non-empty intersection relation: 

\bc\begin{verbatim}
intersectRel :: KB -> [(Class,Class)]
intersectRel kb@(xs,yys) = 
 nub [(x,y) | x <- classes, y <- classes, lits <- litsList, 
    elem x lits && elem y lits   ]
     where 
       classes = universe kb
       litsList = 
         [ maybe [] fst (propagate (ys++xs)) | ys <- yys ]   
\end{verbatim}\ec

The intersection sets of a class $C$ are the classes that have 
a non-empty intersection with $C$: 

\bc\begin{verbatim}
intersectionsets :: Class -> KB -> [Class]
intersectionsets cl kb = rSection cl (intersectRel kb)
\end{verbatim}\ec

In general, in KB query, there are three possibilities: 

\begin{itemize}
\item \verb^derive kb stmt^ is true. This means that the statement is 
derivable, hence true. 
\item \verb^derive kb (neg stmt)^ is true. This means that the negation 
of \verb^stmt^ is derivable, hence true. So \verb^stmt^ is false. 
\item neither  \verb^derive kb stmt^ nor \verb^derive kb (neg stmt)^ is true. 
This means that the knowledge base has no information about \verb^stmt^. 
\end{itemize}

The derivability relation is given by: 

\bc\begin{verbatim}
derive :: KB -> Statement -> Bool
derive kb (AreAll as bs) = bs `elem` (supersets as kb)
derive kb (AreNo as bs)  = (neg bs) `elem` (supersets as kb)
derive kb (AreAny as bs) = bs `elem` (intersectionsets as kb) 
derive kb (AnyNot as bs) = (neg bs) `elem` 
                               (intersectionsets as kb) 
\end{verbatim}\ec

To build a knowledge base we need a function for updating an
existing knowledge base with a statement. 
If the update is successful, we want an updated knowledge base. 
If the update is not successful, we want to get an indication of failure.  
This explains the following type. The boolean in the output is a flag indicating 
change in the knowledge base. 

\bc\begin{verbatim}
update  :: Statement -> KB -> Maybe (KB,Bool)
\end{verbatim}\ec

Update with an `All' statement.  The update function checks for
possible inconsistencies. E.g., a request to add an $A \subseteq B$
fact to the knowledge base leads to an inconsistency if $A
\not\subseteq B$ is already derivable.

\bc\begin{verbatim}
update (All1 as bs) kb@(xs,yss) 
  | bs' `elem` (intersectionsets as kb) = Nothing
  | bs `elem` (supersets  as kb) = Just (kb,False) 
  | otherwise = Just (([as',bs]:xs,yss),True)
 where 
   as' = neg as
   bs' = neg bs
\end{verbatim}\ec

Update with other kinds of statements: 

\bc\begin{verbatim}
update (No1 as bs) kb@(xs,yss)
  | bs `elem` (intersectionsets as kb) = Nothing
  | bs' `elem` (supersets  as kb) = Just (kb,False)
  | otherwise = Just (([as',bs']:xs,yss),True)
 where    
   as' = neg as 
   bs' = neg bs
\end{verbatim}\ec

\bc\begin{verbatim}
update (Some1 as bs) kb@(xs,yss)  
  | bs' `elem` (supersets  as kb) = Nothing
  | bs `elem` (intersectionsets as kb) = Just (kb,False)
  | otherwise = Just ((xs,[[as],[bs]]:yss),True)
 where    
   bs' = neg bs
\end{verbatim}\ec

\bc\begin{verbatim}
update (SomeNot as bs) kb@(xs,yss) 
  | bs `elem` (supersets  as kb) = Nothing
  | bs' `elem` (intersectionsets as kb) = Just (kb,False)
  | otherwise = Just ((xs,[[as],[bs']]:yss),True)
 where 
   bs' = neg bs
\end{verbatim}\ec

The above implementation of an inference engine for syllogistic reasoning 
is a mini-case of computational semantics. What is the use of this? 
Cognitive research focusses on this kind of quantifier reasoning, so it 
is a pertinent question whether the engine can be used to meet cognitive realities?
A possible link with cognition would refine this calculus and the check whether 
the predictions for differences in processing speed for various tasks are realistic. 

There is also a link to the ``natural logic for natural language'' enterprise: the 
logical forms for syllogistic reasoning are very close to the 

All in all, reasoning engines like this one are relevant for rational reconstructions 
of cognitive processing. 

Constructing a knowledge base from a list of statements: 

\bc\begin{verbatim}
makeKB :: [Statement] -> Maybe KB
makeKB = makeKB' ([],[]) 
     where 
         makeKB' kb []     = Just kb
         makeKB' kb (s:ss) = case update s kb of 
              Just (kb',_) -> makeKB' kb' ss
              Nothing      -> Nothing
\end{verbatim}\ec

A preprocess function to prepare for parsing: 

\bc\begin{verbatim}
preprocess :: String -> [String]
preprocess = words . (map toLower) .
             (takeWhile (\ x -> isAlpha x || isSpace x))
\end{verbatim}\ec

The parsing may fail, hence the type: 

\bc\begin{verbatim}
parse :: String -> Maybe Statement
parse = parse' . preprocess
  where
    parse' ["all",as,"are",bs] = 
      Just (All1 (Pos as) (Pos bs))
    parse' ["no",as,"are",bs] = 
      Just (No1 (Pos as) (Pos bs)) 
    parse' ["some",as,"are",bs] = 
      Just (Some1 (Pos as) (Pos bs)) 
    parse' ["some",as,"are","not",bs] = 
      Just (SomeNot (Pos as) (Pos bs))
    parse' ["are","all",as,bs] = 
      Just (AreAll (Pos as) (Pos bs))
    parse' ["are","no",as,bs] = 
      Just (AreNo (Pos as) (Pos bs)) 
    parse' ["are","any",as,bs] = 
      Just (AreAny (Pos as) (Pos bs)) 
    parse' ["are","any",as,"not",bs] = 
      Just (AnyNot (Pos as) (Pos bs))
    parse' ["what", "about", as] = Just (What (Pos as))
    parse' ["how", "about", as]  = Just (What (Pos as))
    parse' _ = Nothing
\end{verbatim}\ec

\bc\begin{verbatim}
process :: String -> KB
process txt = maybe ([],[]) id (mapM parse (lines txt) >>= makeKB)
\end{verbatim}\ec

An example text: 

\bc\begin{verbatim}
mytxt = "all bears are mammals\n"
     ++ "no owls are mammals\n"
     ++ "some bears are stupids\n"
     ++ "all men are humans\n"
     ++ "no men are women\n"
     ++ "all women are humans\n"
     ++ "all humans are mammals\n"
     ++ "some men are stupids\n"
     ++ "some men are not stupids"
\end{verbatim}\ec

Reading a knowledge base from disk: 

\bc\begin{verbatim}
getKB :: FilePath -> IO KB
getKB p = do 
           txt <- readFile p 
           return (process txt)
\end{verbatim}\ec

Universal fact to statement: 

\bc\begin{verbatim}
u2s :: Clause -> Statement
u2s [Neg x, Pos y] = All1 (Pos x) (Pos y)
u2s [Neg x, Neg y] = No1 (Pos x) (Pos y)
\end{verbatim}\ec

Existential fact to statement:

\bc\begin{verbatim}
e2s :: [Clause] -> Statement
e2s [[Pos x],[Pos y]] = Some1 (Pos x) (Pos y)
e2s [[Pos x],[Neg y]] = SomeNot (Pos x) (Pos y)
\end{verbatim}\ec

Writing a knowledge base to disk, in the form of a list 
of statements. 

\bc\begin{verbatim}
writeKB :: FilePath -> KB -> IO ()
writeKB p (xs,yss) = writeFile p (unlines (univ ++ exist))
  where 
    univ  = map (show.u2s) xs
    exist = map (show.e2s) yss
\end{verbatim}\ec

Telling about a class, based on the info in a knowledge base. 

\bc\begin{verbatim}
tellAbout :: KB -> Class -> [Statement]
tellAbout kb as = 
  [All1 as (Pos bs) | (Pos bs) <- supersets as kb, 
                        as /= (Pos bs) ] 
  ++ 
  [No1  as (Pos bs) | (Neg bs) <- supersets as kb, 
                        as /= (Neg bs) ] 
  ++
  [Some1 as (Pos bs) | (Pos bs) <- intersectionsets as kb, 
                      as /= (Pos bs), 
                      notElem (as,Pos bs) (subsetRel kb) ]
  ++
  [SomeNot as (Pos bs) | (Neg bs) <- intersectionsets as kb,  
                   notElem (as, Neg bs) (subsetRel kb) ]
\end{verbatim}\ec

A chat function that starts an interaction from a given knowledge base and writes
the result of the interaction to a file: 

\bc\begin{verbatim}
chat :: IO ()
chat = do
 kb <- getKB "kb.txt"
 writeKB "kb.bak" kb
 putStrLn "Update or query the KB:"
 str <- getLine
 if str == "" then return ()
  else do
   handleCases kb str
   chat
\end{verbatim}\ec

Depending on the input, the various cases are handled by the following
function:

\bc\begin{verbatim}
handleCases :: KB -> String -> IO ()
handleCases kb str = 
   case parse str of 
     Nothing        -> putStrLn "Wrong input.\n"
     Just (What as) -> let 
         info = (tellAbout kb as, tellAbout kb (neg as)) in 
       case info of 
        ([],[])      -> putStrLn "No info.\n"
        ([],negi)    -> putStrLn (unlines (map show negi))
        (posi,negi)  -> putStrLn (unlines (map show posi))
     Just stmt      -> 
      if isQuery stmt then 
        if derive kb stmt then putStrLn "Yes.\n"
          else if derive kb (negat stmt) 
                 then putStrLn "No.\n" 
                 else putStrLn "I don't know.\n"
        else case update stmt kb of 
          Just (kb',True) -> do 
                              writeKB "kb.txt" kb'
                              putStrLn "OK.\n" 
          Just (_,False)  -> putStrLn 
                              "I knew that already.\n"
          Nothing         -> putStrLn 
                              "Inconsistent with my info.\n"
\end{verbatim}\ec

Try this out by loading the software for this chapter and running \verb^chat^.


\section{Implementing Fragments of Natural Language} 

Now what about the meanings of the sentences in a simple fragment of
 English? Using what we know now about a logical form language and its
 interpretation in appropriate models, and assuming we have constants
 available for proper names, and predicate letters for the nouns and
 verbs of the fragment, we can easily translate the sentences
 generated by a simple example grammar into logical forms. Assume the
 following translation key:
\begin{center}
\begin{tabular}{lll}  
\hline 
 lexical item & translation & type of logical constant \\ 
\hline 
 girl         & {\em Girl}        & one-place predicate \\
 boy          & {\em Boy}         & one-place predicate \\
 toy          & {\em Toy}         & one-place predicate \\
 laughed      & {\em Laugh}       & one-place predicate \\
 cheered      & {\em Cheer}       & one-place predicate \\
 loved        & {\em Love}        & two-place predicate \\
 admired      & {\em Admire}      & two-place predicate \\
 helped       & {\em Help}        & two-place predicate \\
 defeated     & {\em Defeat}      & two-place predicate \\
 gave         & {\em Give}        & three-place predicate \\
 introduced   & {\em Introduce}   & three-place predicate \\
 Alice        & $a$           & individual constant \\ 
 Bob          & $b$           & individual constant \\
 Carol        & $c$           & individual constant \\
\hline
\end{tabular}
\end{center}

Then the translation of  {\em Every boy loved a girl}\/ in 
the logical form language above could become: 
\[
  Q_\forall x (\mi{Boy}\;x) (Q_\exists y (\mi{Girl}\;y) (\mi{Love}\;x\;y)). 
\]

To start the construction of meaning representations, we first represent 
a context free grammar for a natural language fragment in Haskell. 
A rule like {\em S ::= NP VP} defines syntax trees consisting of an
{\em S} node immediately dominating an {\em NP} node and a {\em VP} node. 
This is rendered in Haskell as the following datatype definition: 

\bp\begin{verbatim}
data S = S NP VP
\end{verbatim}\ep

The \verb^S^ on the righthand side is a combinator indicating the name of the 
top of the tree. Here is a grammar for a tiny fragment: 

\bc\begin{verbatim}
data S = S NP VP deriving Show
data NP = NP1 NAME | NP2 Det N | NP3 Det RN 
  deriving Show
data ADJ = Beautiful | Happy | Evil 
  deriving Show
data NAME = Alice | Bob | Carol 
  deriving Show
data N = Boy | Girl | Toy | N ADJ N
  deriving Show
data RN = RN1 N That VP | RN2 N That NP TV 
  deriving Show
data That = That deriving Show
data VP = VP1 IV | VP2 TV NP | VP3 DV NP NP deriving Show
data IV = Cheered | Laughed deriving Show
data TV = Admired | Loved | Hated | Helped deriving Show
data DV = Gave | Introduced deriving Show
\end{verbatim}\ec


Look at this is as a definition of syntactic structure trees. 
The structure for {\em The boy that Alice helped admired every girl}
is given in Figure \ref{StructureTreeFig}, with the Haskell version 
of the tree below it. 

\begin{center}
\begin{figure}[htbp] 
\caption{Example structure tree} \label{StructureTreeFig}
\Tree [.S [.NP 
            [.Det {\em the } ]
            [.RN [.N  {\em boy } ]
                 [.{\em that } ]
                 [.NP {\em Alice } ]
                 [.TV {\em helped } ] ] ]
  [.VP [.TV {\em admired } ]
       [.NP [.DET {\em every } ]
            [.CN {\em girl }  ] ]]]

\begin{verbatim}
S 
 (NP (Det the)
     (RN (N boy) That  (NP Alice) (TV helped))
 (VP  (TV admired) (NP (DET every) (N girl)))
\end{verbatim}
\end{figure}
\end{center} 

For the purpose of this chapter we skip the definition of the 
parse function that maps the string {\em The boy that Alice helped admired every girl}
to this structure (but see  \cite[Chapter 9]{EijckUng10:cswfp}). 

Now all we have to do is find appropriate translations for the categories
in the grammar of the fragment.  The first rule, $\mb{S}
\longrightarrow \mb{NP} \ \mb{VP}$, already presents us with a difficulty.
In looking for NP translations and VP translations, should we represent
NP as a function that takes a VP representation as argument, or vice
versa?

In any case, VP representations will have a functional type, for VPs
denote properties. A reasonable type for the function that represents
a VP is \verb^Term -> Formula^. If we feed it with a term, it will yield a
logical form.  Proper names now can get the type of terms. Take the
example {\em Alice laughed}. The verb {\em laughed} gets
represented as the function that maps the term \verb^x^ to the formula
\verb^Atom "laugh" [x]^. Therefore, we get an appropriate logical form
for the sentence if \verb^x^ is a term for {\em Alice}. 

A difficulty with this approach is that phrases like {\em no boy} and
 {\em every girl} do not fit into this pattern. Following Montague, we
 can solve this by assuming that such phrases translate into functions
 that take VP representations as arguments. So the general pattern
 becomes: the NP representation is the function that takes the VP
 representation as its argument. This gives:

\bc\begin{verbatim} 
lfS :: S -> Formula
lfS (S np vp) = (lfNP np) (lfVP vp)
\end{verbatim}\ec 
\index{LF function!lfS@\verb^lfS^}

Next, NP-representations are of type \verb^(Term -> Formula) -> Formula^. 

\index{LF function!lfNP@\verb^lfNP^}
\bc\begin{verbatim} 
lfNP :: NP -> (Term -> Formula) -> Formula
lfNP (NP1 Alice)   = \ p -> p (Struct "Alice" [])
lfNP (NP1 Bob)     = \ p -> p (Struct "Bob"   [])
lfNP (NP1 Carol)   = \ p -> p (Struct "Carol" [])
lfNP (NP2 det cn)  = (lfDET det) (lfN cn) 
lfNP (NP3 det rcn) = (lfDET det) (lfRN rcn) 
\end{verbatim}\ec

Verb phrase representations are of type \verb^Term -> Formula^. 

\index{LF function!lfVP@\verb^lfVP^|(}
\bc\begin{verbatim} 
lfVP :: VP -> Term -> Formula
lfVP (VP1 Laughed)   = \ t -> Atom "laugh"   [t]
lfVP (VP1 Cheered)   = \ t -> Atom "cheer"   [t]
\end{verbatim}\ec 

Representing a function that takes two arguments can be done
either by means of \verb^a -> a -> b^ or by means of \verb^(a,a) -> b^. 
A function of the first type is called {\em curried}, a function 
of the second type {\em uncurried}. 

We assume that representations of transitive verbs are uncurried, so
they have type \verb^(Term,Term) -> Formula^, where the first
term slot is for the subject, and the second term slot for the
object. Accordingly, the representations of ditransitive verbs have
type
\begin{center}
\verb^(Term,Term,Term) -> Formula^
\end{center}
where the first term slot is for the subject, the second one is for
 the indirect object, and the third one is for the direct object.  The
 result should in both cases be a property for VP subjects.  This
 gives us:

\bc\begin{verbatim} 
lfVP (VP2 tv np) =
    \ subj -> lfNP np (\ obj -> lfTV tv (subj,obj))
lfVP (VP3 dv np1 np2) = 
    \ subj -> lfNP np1 (\ iobj -> lfNP np2 (\ dobj -> 
                          lfDV dv (subj,iobj,dobj)))
\end{verbatim}\ec 
\index{LF function!lfVP@\verb^lfVP^|)}

Representations for transitive verbs are: 

\index{LF function!lfTV@\verb^lfTV^}
\bc\begin{verbatim} 
lfTV :: TV -> (Term,Term) -> Formula
lfTV Admired  = \ (t1,t2) -> Atom "admire" [t1,t2]
lfTV Hated    = \ (t1,t2) -> Atom "hate" [t1,t2]
lfTV Helped   = \ (t1,t2) -> Atom "help" [t1,t2]
lfTV Loved    = \ (t1,t2) -> Atom "love" [t1,t2]
\end{verbatim}\ec 

Ditransitive verbs: 

\bc\begin{verbatim} 
lfDV :: DV -> (Term,Term,Term) -> Formula
lfDV Gave = \ (t1,t2,t3) -> Atom "give" [t1,t2,t3]
lfDV Introduced = \ (t1,t2,t3) -> 
                    Atom "introduce" [t1,t2,t3]
\end{verbatim}\ec 

Common nouns have the same type as VPs. 

\index{LF function!lfN@\verb^lfN^}
\bc\begin{verbatim} 
lfN :: N -> Term -> Formula
lfN Girl     = \ t -> Atom "girl"     [t]
lfN Boy      = \ t -> Atom "boy"      [t]
\end{verbatim}\ec 

The determiners we have already treated above, in Section \ref{LFdirectSection}.
Complex common nouns have the same types as simple common nouns: 

\index{LF function!lfRN@\verb^lfRN^}
\bc\begin{verbatim} 
lfRN :: RN -> Term -> Formula
lfRN (RN1 cn _ vp)    = \ t -> Cnj [lfN cn t, lfVP vp t]
lfRN (RN2 cn _ np tv) = \ t -> Cnj [lfN cn t, 
                       lfNP np (\ subj -> lfTV tv (subj,t))]
\end{verbatim}\ec 

We end with some examples: 

\bc\begin{verbatim}
lf1 = lfS (S (NP2 Some Boy) 
                   (VP2 Loved (NP2 Some Girl))) 
lf2 = lfS (S (NP3 No (RN2 Girl That (NP1 Bob) Loved)) 
                   (VP1 Laughed))
lf3 = lfS (S (NP3 Some (RN1 Girl That (VP2 Helped (NP1 Alice)))) 
                   (VP1 Cheered))
\end{verbatim}\ec

This gives: 

\begin{verbatim}
*IST> lf1
Q Some x2 (Atom "boy" [x2]) 
          (Q Some x1 (Atom "girl" [x1]) (Atom "love" [x2,x1]))
*IST> lf2
Q No x1 (Cnj [Atom "girl" [x1],Atom "love" [Bob,x1]]) 
        (Atom "laugh" [x1])
*IST> lf3
Q Some x1 (Cnj [Atom "girl" [x1],Atom "help" [x1,Alice]]) 
         (Atom "cheer" [x1])
\end{verbatim}

What we have presented here is in fact an implementation of 
an extensional fragment of Montague grammar. The next Section 
indicates what has to change in an intensional fragment. 

\section{Extension and Intension} 

One of the trademarks of Montague grammar is the use of possible worlds
to treat intensionality. Instead of giving a predicate a single 
interpretation in a model, possible world semantics gives intensional 
predicates different interpretations in different situations (or: in 
different ``possible worlds''). A prince in one world may be a beggar
in another, and the way in which intensional semantics accounts for 
this is by giving predicates like {\em prince} and {\em beggar} different
interpretations in different worlds. 

So we assume that apart from entities and truth values there is
another basic type, for possible worlds.  We introduce names or
indices for possible worlds, as follows: \label{WorldIndex}

\bc\begin{verbatim}
data W = W Int deriving (Eq,Show) 
\end{verbatim}\ec

Now the type of individual concepts is the type of functions from 
worlds to entities, i.e., \verb+W -> Entity+. An individual concept
is a {\em rigid designator} 
\index{rigid designator} if it picks the same entity in every possible
world: 

\bc\begin{verbatim}
rigid :: Entity -> W -> Entity 
rigid x = \ _ -> x
\end{verbatim}\ec

A function from possible worlds to truth values is a {\em proposition}. 
Propositions have type \verb+W -> Bool+. In 
{\em Mary desires to marry a prince} the rigid designator that 
interprets the proper name ``Mary'' is related to a proposition, 
namely the proposition that is true in a world if and only if 
Mary marries someone who, in that world, is a prince. 
So an intensional verb like {\em desire} may have type 
\verb+(W -> Bool) -> (W -> Entity) -> Bool+, where 
\verb+(W -> Bool)+ is the type of ``marry a prince'', and 
\verb+(W -> Entity)+ is the type for the intensional function 
that interprets ``Mary.''

Models for intensional logic have a domain $D$ of entities plus
functions from predicate symbols to intensions of relations. Here is
an example interpretion for the predicate symbol ``princess:''

\bc\begin{verbatim}
princess :: W -> Pred Entity 
princess = \ w [x] -> case w of 
             W 1 -> elem x [A,C,D,G]
             W 2 -> elem x [A,M]
             _   -> False
\end{verbatim}\ec

What this says is that in $W_1$ $x$ is a princess iff $x$ is among
$A,C,D,G$, in $W_2$ $x$ is a princess iff $x$ is among $A,M$, and in
no other world is $x$ a princess.  This interpretation for
''princess'' will make ``Mary is a princess'' true in $W_2$ but in no
other world.

% \section{Continuation Passing Style Semantics} 

% Recall the Montagovian trick of lifting the type of proper name 
% interpretations from $a$ to $(a \to b) \to b$ by means of 
% argument raising: 

% \bc\begin{verbatim}
% raise :: a -> (a -> b) -> b
% raise x = \ f -> f x
% \end{verbatim}\ec

% If \verb^Alice^ gets translation \verb^Struct "Alice" []^, of 
% type \verb^Term^, then this is lifted to a translation of 
% type \verb^(Term -> Formula) -> Formula^ by means of
% \verb^raise (Struct "Alice" [])^. 

% \begin{verbatim}
% *IST> :t raise (Struct "Alice" [])
% raise (Struct "Alice" []) :: (Term -> b) -> b
% \end{verbatim}

% Applying \verb^raise^ to the result of a function application 
% gives what is called a {\em continuation passing style function}: 

% \bc\begin{verbatim} 
% mkc :: (a -> b) -> a -> (b -> c) -> c 
% mkc f x = raise (f x)
% \end{verbatim}\ec

% Here is an example of its use: 

% \begin{verbatim}
% *IST> mkc (^4) 5 show
% "625"
% \end{verbatim}

% A continuation passing style function is a function with an extra
% argument slot for a function stating `what to do next'.  So: raise to
% the fourth power, next show the result as a string.  Think of the
% second function (\verb^show^ in this case) as the continuation.


\section{Implementing Communicative Action} 

The simplest kind of communicative action probably is question
answering of the kind that was demonstrated in the Syllogistics tool
above, in Section \ref{SylSection}. The interaction is between a
system (the knowledge base) and a user. In the implementation we only
keep track of changes in the system: the knowledge base gets updated
every time the user makes statements that are consistent with the
knowledge base but not derivable from it. 

Generalizing this, we can picture a group of communicating agents,
each with their own knowledge, with acts of communication that change
these knowledge bases. The basic logical tool for this is again
intensional logic, more in particular the epistemic logic proposed by
Hintikka in \cite{Hintikka:kab}, and adapted in cognitive science
(\cite{Gardenfors88:kif}), computer science (\cite{FagHalMosVar:rak}) and
economics (\cite{Aumann1976:atd,BatigalliBonanno1999:rrobk}).  The
general system for tracking how knowledge and belief of communicating
agents evolve under various kinds of communication is called {\em
  dynamic epistemic logic} or {\em DEL}. See \cite{Benthem2011:ldoiai}
for a general perspective, and \cite{DitHoeKoo06:del} for a textbook
account.

To illustrate the basics, we will give an implementation of model checking 
for epistemic update logic with public announcements. 

The basic concept in the logic of knowledge is that of epistemic
uncertainty. If I am uncertain about whether a coin that has just been
tossed is showing head or tail, this can be pictured as two situations
related by my uncertainty.  Such uncertainty relations are
equivalences: If I am uncertain between situations $s$ and $t$, and
between situations $t$ and $r$, this means I am also uncertain between
$s$ and $r$.

Equivalence relations on a set of situations $S$ can be implemented 
as partitions of $S$, where a partition is a family $X_i$ of sets
with the following properties (let $I$ be the index set): 
\begin{itemize} 
\item For each $i \in I$, $X_i \neq \emptyset$ and $X_i \subseteq S$.
\item For $i \neq j$, $X_i \cap X_j = \emptyset$. 
\item $\bigcup_{i \in I} X_i = S$. 
\end{itemize} 
Here is a datatype for equivalence relations, viewed as partitions
(lists of lists of items): 

\bc\begin{verbatim}
type Erel a = [[a]]
\end{verbatim}\ec

The block of an item in a partition: 

\bc\begin{verbatim}
bl :: Eq a => Erel a -> a -> [a]
bl r x = head (filter (elem x) r)
\end{verbatim}\ec

The restriction of a partition to a domain: 

\bc\begin{verbatim} 
restrict :: Eq a => [a] -> Erel a -> Erel a 
restrict domain =  nub . filter (/= []) 
                   . map (filter (flip elem domain)) 
\end{verbatim}\ec

An infinite number of agents, with names for the first
five of them: 

\bc\begin{verbatim}
data Agent = Ag Int deriving (Eq,Ord)

a,b,c,d,e :: Agent
a = Ag 0; b = Ag 1; c = Ag 2; d = Ag 3; e = Ag 4

instance Show Agent where
  show (Ag 0) = "a"; show (Ag 1) = "b"; 
  show (Ag 2) = "c"; show (Ag 3) = "d" ; 
  show (Ag 4) = "e";  
  show (Ag n) = 'a': show n 
\end{verbatim}\ec

A datatype for epistemic models: 

\bc\begin{verbatim}
data EpistM state = Mo
             [state]
             [Agent]
             [(Agent,Erel state)]
             [state]  deriving (Eq,Show)
\end{verbatim}\ec

An example epistemic model: 

\bc\begin{verbatim}
example :: EpistM Int
example = Mo 
 [0..3]
 [a,b,c]
 [(a,[[0],[1],[2],[3]]),(b,[[0],[1],[2],[3]]),(c,[[0..3]])]
 [1]
\end{verbatim}\ec 

In this model there are three agents and four possible worlds.  The
first two agents $a$ and $b$ can distinguish all worlds, and the third
agent $c$ confuses all of them.

Extracting an epistemic relation from a model: 

\bc\begin{verbatim}
rel :: Agent -> EpistM a -> Erel a
rel ag (Mo _ _ rels _) = myLookup ag rels

myLookup :: Eq a => a -> [(a,b)] -> b
myLookup x table = 
   maybe (error "item not found") id (lookup x table)
\end{verbatim}\ec

This gives: 

\begin{verbatim}
*IST> rel a example
[[0],[1],[2],[3]]
*IST> rel c example
[[0,1,2,3]]
*IST> rel d example
*** Exception: item not found
\end{verbatim}


A logical form language for epistemic statements; note that the type
has a parameter for additional information.

\bc\begin{verbatim}
data Form a = Top 
            | Info a
            | Ng (Form a)
            | Conj [Form a]
            | Disj [Form a]
            | Kn Agent (Form a)
          deriving (Eq,Ord,Show)
\end{verbatim}\ec

A useful abbreviation: 

\bc\begin{verbatim}
impl :: Form a -> Form a -> Form a
impl form1 form2 = Disj [Ng form1, form2]
\end{verbatim}\ec

Semantic interpretation for this logical form language: 

\bc\begin{verbatim}
isTrueAt :: Ord state => 
            EpistM state -> state -> Form state -> Bool
isTrueAt m w Top = True 
isTrueAt m w (Info x) = w == x
isTrueAt m w (Ng f) = not (isTrueAt m w f)
isTrueAt m w (Conj fs) = and (map (isTrueAt m w) fs)
isTrueAt m w (Disj fs) = or  (map (isTrueAt m w) fs)
isTrueAt
 m@(Mo worlds agents acc points) w (Kn ag f) = let 
    r = rel ag m 
    b = bl r w 
  in 
    and (map (flip (isTrueAt m) f) b) 
\end{verbatim}\ec

This treats the Boolean connectives as usual, and interprets
knowledge as truth in all worlds in the current accessible 
equivalence block of an agent. 

The effect of a public announcement $\phi$ on an epistemic model
is that the set of worlds of that model gets limited to the 
worlds where $\phi$ is true, and the accessibility relations 
get restricted accordingly. 

\bc\begin{verbatim}
upd_pa :: Ord state => 
          EpistM state -> Form state -> EpistM state
upd_pa m@(Mo states agents rels actual) f = 
  (Mo states' agents rels' actual') 
   where 
   states' = [ s | s <- states, isTrueAt m s f ]
   rels'   = [(ag,restrict states' r) | (ag,r) <- rels ]
   actual' = [ s | s <- actual, s `elem` states' ]
\end{verbatim}\ec

A series of public announcement updates: 

\bc\begin{verbatim}
upds_pa ::  Ord state => 
            EpistM state -> [Form state] -> EpistM state
upds_pa m [] = m 
upds_pa m (f:fs) = upds_pa (upd_pa m f) fs
\end{verbatim}\ec

We illustrate the working of the update mechanism on a famous
epistemic puzzle.  The following Sum and Product riddle was stated by
the Dutch mathematican Hans Freudenthal in a Dutch mathematics journal
in 1969.  \index{Freudenthal, H.}  There is also a version by John
McCarthy (see \url{http://www-formal.stanford.edu/jmc/puzzles.htm}).

\begin{quote} 
A says to S and P: I have chosen two integers $x$, $y$ such that $1 < x < y$
and $x + y  \leq 100$. In a moment, I will inform S only of $s = x + y$, 
and P only of $p = xy$. These announcements remain private. You are required
to determine the pair $(x, y )$. 
He acts as said. The following conversation now takes place:
\begin{enumerate} 
\item P says: ``I do not know the pair.''
\item S says: ``I knew you didn't.''
\item P says: ``I now know it.''
\item S says: ``I now also know it.''
\end{enumerate}
Determine the pair $(x, y )$.
\end{quote} 
This was solved by combinatorial means in a later issue of the
 journal. A model checking solution with DEMO \cite{Eijck07:dadoem}
 (based on a DEMO program written by Ji Ruan) was presented in
 \cite{DitRuaVer05:mcsap}.  \index{Ditmarsch, Hans van} \index{Ruan,
 Ji} \index{Verbrugge, Rineke} The present program is an optimized
 version of that solution.

The list of candidate pairs: 

\bc\begin{verbatim} 
pairs :: [(Int,Int)]
pairs  = [ (x,y) |  x <- [2..100], y <- [2..100], 
                    x < y, x+y <= 100 ]
\end{verbatim}\ec

The initial epistemic model is such that $a$ (representing S) cannot
distinguish number pairs with the same sum, and $b$ (representing P)
cannot distinguish number pairs with the same product.  Instead of
using a valuation, we use number pairs as worlds.

\bc\begin{verbatim} 
msnp :: EpistM (Int,Int)
msnp = (Mo pairs [a,b] acc pairs)
  where 
  acc   = [ (a, [ [ (x1,y1) | (x1,y1) <- pairs,  
                               x1+y1 == x2+y2 ] |
                                 (x2,y2) <- pairs ] ) ]
          ++
          [ (b, [ [ (x1,y1) | (x1,y1) <- pairs,  
                               x1*y1 == x2*y2 ] |
                                 (x2,y2) <- pairs ] ) ]
\end{verbatim}\ec

The statement by $b$ that he does not know the pair: 

\bc\begin{verbatim}
statement_1 = 
  Conj [ Ng (Kn b (Info p)) | p <- pairs ]
\end{verbatim}\ec

To check this statement is expensive. A computationally cheaper
equivalent statement is the following (see \cite{DitRuaVer05:mcsap}).

\bc\begin{verbatim}
statement_1e = 
  Conj [ Info p `impl` Ng (Kn b (Info p)) | p <- pairs ]
\end{verbatim}\ec

In Freudenthal's story, the first public announcement is the statement
where $b$ confesses his ignorance, and the second public announcement
is the statement by $a$ about her knowledge about $b$'s state of
knowledge {\em before}\/ that confession. We can wrap the two together
in a single statement to the effect that initially, $a$
knows that $b$ does not know the pair. This gives:

\bc\begin{verbatim} 
k_a_statement_1e = Kn a statement_1e
\end{verbatim}\ec

The second announcement proclaims the statement by $b$ that now he knows: 

\bc\begin{verbatim}
statement_2 = 
  Disj [ Kn b (Info p) | p <- pairs ]
\end{verbatim}\ec

Equivalently, but computationally more efficient: 

\bc\begin{verbatim}
statement_2e = 
  Conj [ Info p `impl` Kn b (Info p) | p <- pairs ]
\end{verbatim}\ec

The final announcement concerns the statement by $a$ that now she knows as well. 

\bc\begin{verbatim}
statement_3 = 
  Disj [ Kn a (Info p) | p <- pairs ]
\end{verbatim}\ec


In the computationally optimized version: 

\bc\begin{verbatim}
statement_3e =  
  Conj [ Info p `impl` Kn a (Info p) | p <- pairs ]
\end{verbatim}\ec

The solution: 

\bc\begin{verbatim} 
solution = upds_pa msnp 
           [k_a_statement_1e,statement_2e,statement_3e]
\end{verbatim}\ec

This is checked in a matter of minutes: 

\begin{verbatim}
*IST> solution
Mo [(4,13)] [a,b] [(a,[[(4,13)]]),(b,[[(4,13)]])] [(4,13)]
\end{verbatim}

\section{Resources} 

\paragraph{Code for this Chapter} The example code in this Chapter 
can be found at internet address \url{https://github.com/janvaneijck/ist}.
To run this software, you will need the Haskell system, which 
can be downloaded from \url{www.haskell.org}. This site 
also gives many interesting Haskell resources. 

\paragraph{Epistemic model checking} More information on 
epistemic model checking can be found in the documentation 
of the epistemic model checker DEMO. See \cite{Eijck07:dadoem}. 

\paragraph{Link for Computational Semantics With Functional Programming} 
The website for \cite{EijckUng10:cswfp} can be found at 
\url{www.computationalsemantics.eu}. 

\paragraph{Further computational semantics links}
Special Interest Group in Computational Semantics:
\url{http://www.sigsem.org/wiki/}.  International Workshop on
Computational Semantics: \url{http://iwcs.uvt.nl/}. Wikipedia entry on
computational semantics:
\url{http://en.wikipedia.org/wiki/Computational_semantics}.

\section{Appendix} 

A show function for identifiers: 

\bc\begin{verbatim}
instance Show Id where 
  show (Id name 0) = name 
  show (Id name i) = name ++ show i
\end{verbatim}\ec

A show function for terms: 

\bc\begin{verbatim}
instance Show Term where 
  show (Var id)   = show id 
  show (Struct name []) = name 
  show (Struct name ts) = name ++ show ts
\end{verbatim}\ec

For the definition of fresh variables, we collect the list of indices
that are used in the formulas in the scope of a quantifier, and select
a fresh index, i.e., an index that does not occur in the index list:

\bc\begin{verbatim}
fresh :: [Formula] -> Int 
fresh fs = i+1 where i = maximum (0:indices fs)

indices :: [Formula] -> [Int]
indices [] = []
indices (Atom _ _:fs) = indices fs
indices (Eq _ _:fs) = indices fs
indices (Not f:fs)  = indices (f:fs)
indices (Cnj fs1:fs2) = indices (fs1 ++ fs2) 
indices (Dsj fs1:fs2) = indices (fs1 ++ fs2) 
indices (Q _ (Id _ n) f1 f2:fs) = n : indices (f1:f2:fs)
\end{verbatim}\ec 

\bibliographystyle{handbook}
\bibliography{VanEijck}

\printindex
\end{document}





