%----*- coding: utf-8 -*-

\section{An introduction to continuation semantics}


Most versions of dynamic semantics (DS) in linguistics make heavy use of assignment functions as semantic objects.  While this may not be apparent to the casual reader of early work like \cite{kamp81}, a compositional semantics for DRT, DPL~\citep{groenendijk91} or more recent developments~\citep{brasoeavnu10}  leads almost inevitably to the introduction of ``odd'' types whose inhabitants are variables, assignments or other ``representational'' elements.  Dynamic Intensional Logic (DIL)\cite{groenendijk-stokhof96,dekker99}, following \cite{janssen}'s work on programming languages, has the virtue of making central the semantic status of assignment functions, as they are the points of evaluation in that model theory.  But almost all of extant versions of DS include assignment functions as parts of semantic values.  The exploitation of assignment functions as semantic objects plays a crucial role in many dynamic semantics approaches to modal subordination and intensionality~\cite{frank97,asher07}.  This engenders subtle differences in the underlying logic, clouding the logical status of discourse referents in a ``top'' DRS by making them appear ambiguous between existentially bound variables and free ones (cf.~\cite{fernando94}).  It also leads to problems of destructive assignment in DPL and with variable clash in DRT or versions of DPL that use partial assignment functions.  It is difficult to avoid these problems in a purely compositional environment, leading to cumbersome systems.  


Continuation style semantics (CS) developed by computer scientists in the 70s and introduced into linguistics by \cite{barker04,barker-shan,degroote06,bernardi07} avoid these problems.   CS provides a more abstract setting for dynamic logics, abstracting away from assignments that are essential to the formulations of DIL, DPL and DRT.  CS, like DS, models the dynamic meaning of a natural language expression as a transition between a left context and a right one.  But in CS right contexts are explicitly introduced and are defined in terms of left contexts and sentence denotations.  CS exploits the structure of a monad in category theory~\cite{moggi91}, which specifies the parameters needed to provide a CS: the first is \emph{to specify what a left context is}; the second is to provide a ``binder'' rule, which tells us \emph{how to combine the semantics of a text with that of subsequent sentence}; the third is \emph{to specify the lexical entries for expressions}.  CS thus refocuses semanticists' attention on specifying appropriate lexical entries and discourse contexts. CS permits a wide variety of choices as to what left contexts, binder rules and lexical entries are, a liberalism we exploit below. 


As an example, consider \posscitet{degroote06}~CS.
de~Groote exploits Montague's
homomorphic interpretation of syntactic types and structures into
semantic types and terms. But \cite{degroote06} changes Montague's interpretation of the sentence type $\SC$, $\inter{\SC}$ from  $\Prop$ to:
$\Omega \defin \gamma \imp (\gamma \imp \Prop) \imp \Prop$, where $\gamma$ is the type of
the left context or discourse context already given and $\gamma \imp \Prop$ is
the type of the right context or discourse ``to come''---its
\emph{continuation}. If this sentence introduces a new discourse entity $x$,
 given an environment $i$ (as  \textit{input}) and a continuation $k$ as
parameter, it can provide $(x::i)$ (with $\cdot :: \cdot$ a
  list constructor of type $\ent \imp \gamma \imp \gamma$) as parameter to $k$, making the value of
$x$ available for $k$.

Other types have standard interpretations.  Where $\inter{X}$ stands for the $\lambda$-term or meaning of $X$,
 $\inter{\NP}=(\ent \imp
\inter{\SC}) \imp \inter{\SC}$ and $\inter{\N}=\ent \imp \inter{\SC}$. Pronouns have the following interpretation:
$\inter{\textit{it}} = \lambda P.\lambda i k. P\,(\sel\,i)\,i\,k$, where $i \colon \gamma, k \colon \gamma \rightarrow \Prop$, and where
$\sel\,i$ is a function that selects a \emph{suitable} discourse
antecedent inside $i$.
% (note that here the antecedents
%are explicitly given in $i$ and ordinary bound objectual variables rather than discourse referents and computed over the
%representation as in DRT).


A CS like~\posscitet{degroote06}'s must say how a text $T$ combines with a sentence to its right.  This is the CS binder issue, which  is also an essential part of all dynamical systems---it is the DRS update operation of DRT or relational composition of sentence contents in DPL.  Here is the basic binder equation for de~Groote's system and ours:%
\begin{equation}
\label{degroote}
\inter{T.S} = \lambda i. \lambda k. \inter{T}\ i\ (\lambda i'. \inter{S}\ i'\ k)
\end{equation}
That is, the text to date $T$ takes the meaning of $S$ as its right context, or rather the meaning of $S$ suitably applied and abstracted so that it can be of $\Prop$ type.   A quick type check on $\lambda i'.\inter{S}\ i'\ k$ confirms that this is indeed the right output: $\inter{S} : \gamma \imp (\gamma \imp \Prop) \imp \Prop$ so $\lambda i'. \inter{S}\ i'\ k : \gamma \imp \Prop$.

Let's look at a sample discourse to see how the theory works.%
\example{\label{snore}A man is sleeping.  He is snoring.}%
Suitable lexical entries provide a completely classical interpretation of these two sentences except that they have both a left and right context and that the second sentence fills in the right context of the first.  The entries also make the existential determiner introduce an individual into the right context---a witness that will be ``selected'' by the pronoun.   With this in mind, the interpretation of the first sentence is:
\begin{equation}
\lambda i. \lambda k. \exists x. \ (\semof{man}\ x) \wedge (\semof{sleeping}\ x) \wedge (k \ (x::i))
\end{equation}
The second sentence provides the $\lambda$ term:
\begin{equation}
\lambda i. \lambda k. (\semof{snoring}\ (\sel\ i)) \wedge (k\ i)
\end{equation}
Using the binder rule in (\ref{degroote}), these last two $\lambda$ terms yield a meaning for (\ref{snore}) :
\begin{align*}
  \lefteqn{\lambda i\ k.[\lambda i\ k.\exists x.(\semof{man}\ x) \wedge (\semof{sleeping}\ x) \wedge k\ (x::i)]\ i\ (\lambda i'. (\lambda i\ k.(\semof{snoring}\ (\sel\ i)) \wedge (k\ i))\ i'\ k)}\\
 &\betareduce \lambda i\ k.[\lambda k. \exists x. (\semof{man}\ x) \wedge (\semof{sleeping}\ x) \wedge (k\ (x::i))]\ (\lambda i'.(\semof{snoring}\ (\sel\ i')) \wedge (k\ i'))\\
& \betareduce \lambda i\ k.[\exists x. (\semof{man}\ x) \wedge (\semof{sleeping}\ x) \wedge ((\lambda i'.(\semof{snoring}\ (\sel\ i')) \wedge (k\ i'))\ (x::i))]\\
& \betareduce \lambda i\ k.[\exists x. (\semof{man}\ x) \wedge (\semof{sleeping}\ x) \wedge ((\semof{snoring}\ (\sel\ (x::i)) \wedge (k\ (x::i))))]\\
\end{align*}

 \noindent
 In selecting the bound variable $x$, the semantic value of the anaphoric pronoun falls within the scope of the original existential quantifier, reducing anaphoric binding to quantificational binding.
 
 
 
We briefly compare de~Groote's CS to DIL.\footnote{DIL's Montagovian nature facilitates the comparison, but we could have illustrated our points with other versions of DS.}  The points of evaluation in models for DIL are not worlds but assignments of values to variables.  Sentences have the type: $(s \imp t) \imp t$, where $s$ is the type of states (assignments).  Crucial to DIL's account of intersentential anaphora are the modalities,  $\langle x/d\rangle$,  where $d$ identifies an assignment.  
%$\inter{^{\wedge}Ud}(s) = 1$ iff the value of $d \in \inter{U}^{s}$
%$d$ is an "identifier assignment"
$\langle x/d\rangle \phi$ evaluates $\phi$ relative to an assignment in which the value of d = 
the value of $x$ in the current state.  In DIL, quantification over $x$ in $\langle x/d\rangle \phi$ provides dynamic binding, and as \cite{dekker99} emphasizes:
%\example{
%\label{dekker} $\lambda p. \langle x/d\rangle ^{\vee} p[ ^{\wedge}Ud] \betareduce Ux$}
%and in particular that:
\example{
\label{dekker1} $\lambda p. \exists x. \langle x/d\rangle ^{\vee} p[ ^{\wedge}Ud] \betareduce \exists x. Ux$}
%Crucially, $d$ is not free in $Ud$ above.

Like CS, DIL uses a binder rule to build text meanings:
\begin{equation}
  \label{DILrule}
  \inter{T}.\inter{S} = \lambda p ( \inter{T} (^{\wedge}\inter{S}(p))
\end{equation}
Returning to (\ref{snore}), DIL provides the following logical forms for the two sentences.%
%\examples[l@{}XMl]{%
%  \ex \label{man}   \lambda p. \exists x \langle x/d\rangle. (\semof{man}\ x) \wedge (\semof{sleeping}\ x) \wedge ^{\vee} p)\\
%  \ex \label{smoke}  \lambda p. \semof{snoring}\ (d)\wedge ^{\vee}  p)%
%}
\examples{%
 \ex \label{man}   $\lambda p. \exists x \langle x/d\rangle. (\semof{man}\ x) \wedge (\semof{sleeping}\ x) \wedge ^{\vee} p)$\\
  \ex \label{smoke}  $\lambda p. \semof{snoring}\ (d)\wedge ^{\vee}  p)$%
}
 Exploiting (\ref{dekker1}), the translations (\ref{man}) and (\ref{smoke}), together with (\ref{DILrule}), now yield for (\ref{snore}): 
\example{%
$\lambda p.\exists x. (\semof{man}\ x) \wedge (\semof{sleeping}\ x) \wedge \semof{snoring}\ (d)\wedge ^{\vee}  p)$
}
%\begin{align*}
%  \lefteqn{\lambda p_0.(\lambda p. \exists x. (Mx \wedge Wx \wedge ^{\vee} p))[^{\wedge}\lambda p. Sd \wedge ^{\vee} p)(p_0)]}\\
% & \betareduce \lambda p_0. (\lambda p. \exists x. (Mx \wedge Wx \wedge ^{\vee} p))[^{\wedge}Sd \wedge ^{\vee}p_0]\\
%& \betareduce \lambda p_0.\exists x. (Mx \wedge Wx \wedge ^{\vee\wedge}Sd \wedge  ^{\vee}p_0)\\
%& \betareduce \lambda p_0.\exists x. (Mx \wedge Wx \wedge Sx \wedge  ^{\vee} p_0)
%\end{align*}
The DIL derivation capitalizes on the reduction properties of state switcher $\langle x/d\rangle$  and crucially depends on DIL's unorthodox "worlds", which are assignments.  This is
quite different from~de Groote's CS, whose model theory and logic are completely classical.  The left context list structure builds in effect assignment functions {\em internally}, via the interpretation of update operator $: :$ and captures the structure of an assignment function without postulating any as basic objects in the model theory.\footnote{The semantics would work just as well, if instead of lists, we had used sets of objects as left contexts.}    Notice that this simplification comes about simply by a ``distribution of labor'': the binder rule in \citeauthor{degroote06} is more complex than that of DIL as are the lexical entries.  But the payoff is a logical framework that is \emph{just} that of standard logic.

