# Introducing a Calculus of Effects and Handlers for Natural Language Semantics

Jirka Maršík, Maxime Amblard

► To cite this version:

Jirka Maršík, Maxime Amblard. Introducing a Calculus of Effects and Handlers for Natural Language Semantics. Formal Grammar 2016, Aug 2016, Bozen-Bolzano, Italy. pp.257–272, 10.1007/978-3-662-53042-9_15 . hal-01332762v2

HAL Id: hal-01332762

https://inria.hal.science/hal-01332762v2

Submitted on 7 Jul 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Introducing a Calculus of Effects and Handlers for Natural Language Semantics

Jirka Maršík and Maxime Amblard

LORIA, UMR 7503, Université de Lorraine, CNRS, Inria, Campus Scientifique, F-54506 Vandœuvre-lès-Nancy, France
{jirka.marsik, maxime.amblard}@loria.fr

**Abstract.** In compositional model-theoretic semantics, researchers assemble truth-conditions or other kinds of denotations using the lambda calculus. It was previously observed [26] that the lambda terms and/or the denotations studied tend to follow the same pattern: they are instances of a monad. In this paper, we present an extension of the simply-typed lambda calculus that exploits this uniformity using the recently discovered technique of effect handlers [22]. We prove that our calculus exhibits some of the key formal properties of the lambda calculus and we use it to construct a modular semantics for a small fragment that involves multiple distinct semantic phenomena.

**Keywords:** compositionality, side effects, monads, handlers, deixis, conventional implicature

## 1 Introduction

The prevailing methodology of formal semantics is compositionality in the sense of Frege: denotations of complex phrases are functions of the denotations of their immediate constituents. However, several phenomena have been identified that challenge this notion of compositionality. Examples include anaphora, presupposition, quantification, deixis and conventional implicature. In all of these examples, simple models of denotation (i.e. noun phrases are individuals, sentences are truth-values) run into complications as the denotations can depend on external values (anaphora, deixis) or on something which is not an immediate constituent (presupposition, quantification, conventional implicature).

Among the solutions to these challenges, we find (at least) two types of solutions. First, we have those that relax the condition of compositionality. Notably, the denotation of a complex phrase is no longer a *function per se* of the denotations of its immediate subconstituents. Rather, it is some other formally defined process.<fnref n="1" /> Examples of this approach include:

<footnote n="1">¹ This kind of distinction is the same distinction as the one between a mathematical function and a function in a programming language, which might have all kinds of side effects and therefore not be an actual function.</footnote>
- the incremental algorithm used to build discourse representation structures in DRT, as presented in [12]

- the λμ calculus, used in [6] to analyze quantification, since, due to the lack of confluence, function terms do not denote functions over simple denotations

- the use of exceptions and exception handlers in [18] to model presuppositions in an otherwise compositional framework

- the parsetree interpretation step in the logic of conventional implicatures of [23] that builds the denotation of a sentence by extracting implicatures from the denotations of its subparts (including the non-immediate ones)

The other approach is to enrich the denotations so that they are parame-
terized by the external information they need to obtain and contain whatever
internal information they need to provide to their superconstituents. Here are
some examples of this style:

- any kind of semantic indices (e.g. the speaker and addressee for deixis, the current world for modality), since they amount to saying that a phrase denotes an indexed set of simpler meanings

- the continuized semantics for quantification [1] in which denotations are functions of their own continuations

• and more generally, any semantics using type raising or generalized quan-
tifiers for noun phrase denotations

- the dynamic denotations of [7] that are functions of the common ground and their continuation

- compositional event semantics, such as the one in [25], that shift the denotations of sentences from truth-values to predicates on events

We want to find a common language in which we could express the above tech-
niques. Our inspiration comes from computer science. There, a concept known
as *monad* has been used:

- in denotational semantics to give the domain of interpretation for programming languages that involve side effects [21].

- in functional programming to emulate programming with side effects via term-level encodings of effectful programs [29].

These two principal applications of monads align with the two approaches we have seen above. The one where we change our calculus so it no longer defines pure functions (e.g. is non-deterministic, stateful or throws exceptions) and the one where we use a pure calculus to manipulate terms (denotations) that encode some interaction (e.g. dynamicity, continuations or event predication).

Monad is a term from category-theory. Its meaning is relative to a category. For us, this will always be the category whose objects are types and whose arrows are functions between different types. A monad is formed by a functor and a pair of natural transformations that satisfy certain laws. In our case, this means that a monad is some type constructor (the functor part) and some combinators (the natural transformations) that follow some basic laws. To give an example of this,
we can think of the functor $T(\alpha) = (\alpha \to o) \to o$ together with combinators such as the type raising $\eta(x) = \lambda P. P x$ as a monad of quantification.

The relationship between side effects in functional programming and computational semantics has been developed in several works [27,28],<fnref n="2" /> stretching as far back as 1977 [10]. The usefulness of monads in particular has been discovered by Shan in 2002 [26]. Since then, the problem that remained was how to compose several different monads in a single solution. Charlow used the popular method of monad morphisms<fnref n="3" /> to combine several monads in his dissertation [4]. Giorgolo and Asudeh have used distributive laws to combine monads [8], while Kiselyov has eschewed monads altogether in favor of applicative functors which enjoy easy composability [13].

Our approach follows the recent trend in adopting effects and handlers to combine side effects [2,11] and to encode effectful programs in pure functional programming languages [14,3].

The idea is that we can represent each of the relevant monads using an algebra. We can then combine the signatures of the algebras by taking a disjoint union. The free algebra of the resulting signature will serve as a universal representation format for the set of all terms built from any of the source algebras and closed under substitution. Then, we will build modular interpreters that will give meanings to the operators of the algebras in terms of individuals, truth-values and functions.

In Sect. 2, we will introduce a formal calculus for working with the algebraic terms that we will use in our linguistic denotations. In Sect. 3, we will incrementally build up a fragment involving several of the linguistic phenomena and see the calculus in action. Before we conclude in Sect. 5, we will also discuss some of the formal properties of the calculus in Sect. 4.

## 2 Definition of the Calculus

Our calculus is an extension of the simply-typed lambda calculus (STLC). We add terms of a free algebra into our language and a notation for writing handlers, composable interpreters of these terms. An operator of the free algebra corresponds to a particular interaction that a piece of natural language can have with its context (e.g. a deictic expression might request the speaker's identity using some operator **speaker** in order to find its denotation). A handler gives an interpretation to every occurrence of an operator within a term (e.g. direct speech introduces a handler for the operator **speaker** that essentially rebinds the current speaker to some other entity).

<footnote n="2">² Side effects are to programming languages what pragmatics are to natural languages: they both study how expressions interact with the worlds of their users. It might then come as no surprise that phenomena such as anaphora, presupposition, deixis and conventional implicature yield a monadic description.</footnote>

<footnote n="3">³ Also known as monad transformers in functional programming.</footnote>
## 2.2 Types

We now give a syntax for the types of our calculus along with a typing relation. In the grammar below, $\alpha, \beta, \gamma...$ range over types, $\nu$ ranges over atomic types from some set $\mathcal{T}$ and $E, E'...$ range over effect signatures (introduced below).

The types of our language consist of:

$$ \begin{array}{lcl} \alpha, \beta, \gamma ::= & \alpha \to \beta & [\text{function}] \\ | & \nu & [\text{atom}] \\ | & \mathcal{F}_E(\alpha) & [\text{computation}] \end{array} $$

The only novelty here is the $\mathcal{F}_E(\alpha)$ computation type. This is the type of algebraic expressions whose atoms are terms of type $\alpha$ and whose operation symbols come from the effect signature $E$. We call them computation types and we call terms of these types computations because our algebraic expressions will always represent some kind of program with effects.

Effect signatures are similar to typing contexts. They are partial mappings from the set of operation symbols $\mathcal{E}$ to pairs of types. We will write the elements of effect signatures the following way — $op: \alpha \to \beta \in E$ means that $E$ maps $op$ to the pair of types $\alpha$ and $\beta$.<fnref n="5" /> When dealing with effect signatures, we will often make use of the disjoint union operator $\uplus$. The term $E_1 \uplus E_2$ serves as a constraint demanding that the domains of $E_1$ and $E_2$ be disjoint and at the same time it denotes the effect signature that is the union of $E_1$ and $E_2$.

The typing rules are presented in Figure 1.

The typing rules mirror the syntax of terms. Again, the first four rules come from STLC. The $[\eta]$ and $[\delta]$ rules are self-explanatory and so we will focus on the $[op]$, $[\emptyset]$ and $[C]$ rules.

**[op]** To use an operation $op: \alpha \to \beta$, we provide the input parameter $M_p: \alpha$ and a continuation $\lambda x. M_c: \beta \to \mathcal{F}_E(\gamma)$, which expects the output of type $\beta$. The resulting term has the same type as the body of the continuation, $\mathcal{F}_E(\gamma)$.

Before, we have spoken of terms of type $\mathcal{F}_E(\gamma)$ as of algebraic expressions generated by the terms of type $\gamma$ and the operators in the effect signature $E$. However, having seen the typing rule for operation terms, it might not be obvious how such a term represents an algebraic expression. Traditionally, algebraic signatures map operation symbols to arities, which are natural numbers. Our effect signatures map each operation symbol to a pair of types $\alpha \to \beta$.

- We can explain $\alpha$ by analogy to the single-sorted algebra of vector spaces. In a single-sorted vector space algebra, scalar multiplication is viewed as a unary operation parameterized by some scalar. So technically, there is a different unary operation for each scalar. All of our operations are similarly parameterized and $\alpha$ is the type of that parameter.

<footnote n="5">⁵ The two types $\alpha$ and $\beta$ are to be seen as the operation's *input* and *output* types, respectively.</footnote>
$$ \frac{\Gamma, x : \alpha \vdash M : \beta}{\Gamma \vdash \lambda x. M : \alpha \rightarrow \beta} \text{ [abs]} $$

$$ \frac{x : \alpha \in \Gamma}{\Gamma \vdash x : \alpha} \text{ [var]} $$

$$ \frac{\Gamma \vdash M : \alpha}{\Gamma \vdash \eta M : \mathcal{F}_E(\alpha)} \text{ [\eta]} $$

$$ \frac{\Gamma \vdash M : \mathcal{F}_\emptyset(\alpha)}{\Gamma \vdash \mathcal{I} M : \alpha} \text{ [\delta]} $$

$$ \frac{\Gamma \vdash M : \alpha \rightarrow \beta \quad \Gamma \vdash N : \alpha}{\Gamma \vdash MN : \beta} \text{ [app]} $$

$$ \frac{c : \alpha \in \Sigma}{\Gamma \vdash c : \alpha} \text{ [const]} $$

$$ \frac{\Gamma \vdash M_p : \alpha}{\Gamma \vdash \mathbf{op} M : \alpha \rightarrow \beta \in E} \quad \frac{\Gamma \vdash \mathbf{op} M_p : (\lambda x. M_c) : \mathcal{F}_E(\gamma)}{\Gamma \vdash \mathbf{op} M_p : \alpha \rightarrow \beta \in E} \text{ [op]} $$

$$ \begin{gathered} E = \{ \mathbf{op}_i : \alpha_i \mapsto \beta_i \}_{i \in I} \uplus E_f \\ E' = E'' \uplus E_f \\ [\Gamma \vdash M_i : \alpha_i \rightarrow (\beta_i \rightarrow \mathcal{F}_{E'}(\delta)) \rightarrow \mathcal{F}_{E'}(\delta)]_{i \in I} \\ \Gamma \vdash M_\eta : \gamma \rightarrow \mathcal{F}_{E'}(\delta) \\ \Gamma \vdash N : \mathcal{F}_E(\gamma) \\ \frac{\Gamma \vdash (\mathbf{op}_i : M_i)_{i \in I}, \eta : M_\eta}{\Gamma \vdash (\mathbf{op}_i : M_i)_{i \in I} N : \mathcal{F}_{E'}(\delta)} \text{ [\{\}]} \end{gathered} $$

$$ \frac{\Gamma \vdash M : \alpha \rightarrow \mathcal{F}_E(\beta)}{\Gamma \vdash \mathcal{C} M : \mathcal{F}_E(\alpha \rightarrow \beta)} \text{ [C]} $$

<caption>Fig. 1: The typing rules for our calculus.</caption>

- The type $\beta$ expresses the arity of the operator. When we say that an operator has arity $\beta$, where $\beta$ is a type, we mean that it takes one operand for every value of $\beta$ [24]. We can also think of the operator as taking one operand containing $x : \beta$ as a free variable.

We can look at the algebraic expression $\mathbf{op} M_p (\lambda x. M_c)$ as a description of a program that:

- interacts with its context by some operator called $\mathbf{op}$

- to which it provides the input $M_p$

- and from which it expects to receive an output of type $\beta$

- which it will then bind as the variable $x$ and continue as the program described by $M_c$.

The banana brackets describe iterators/catamorphisms.<fnref n="6" /> In the typing rule, $E$ is the input's signature, $E'$ is the output's signature, $\gamma$ is the input's atom type and $\delta$ is the output's atom type. $E$ is decomposed into the operations that our iterator will actually interpret, the other operations form a residual signature $E_f$. The output signature will then still contain the uninterpreted operations $E_f$ combined with any operations $E''$ that our interpretation might introduce.

<footnote n="6">⁶ These are similar to recursors/paramorphisms. See [20] for the difference. Catamorphisms are also known as folds and the common higher-order function *fold* found in functional programming languages is actually the iterator/catamorphism for lists.</footnote>
[C] We said before that the C function will let us commute $\lambda$ and operations. Here we see that, on the type level, this corresponds to commuting the $F_E(-)$ and the $\alpha \to$ - type constructors.

## 2.3 Reduction Rules

We will now finally give a semantics to our calculus. The semantics will be given in the form of a reduction relation on terms. Even though the point of the calculus is to talk about effects, the reduction semantics will not be based on any fixed evaluation order; any subterm that is a redex can be reduced in any context. The reduction rules are given in Fig. 2.

<figure><img src="image_2.png" /><figcaption>Fig. 2: The reduction rules of our calculus.</figcaption></figure>

We have the $\beta$ and $\eta$ rules, which, by no coincidence, are the same rules as the ones found in STLC. The rest are function definitions for $\langle \rangle$, $\circled$ and $C$.

By looking at the definition of $\langle \rangle$, we see that it is an iterator. It replaces every occurrence of the constructors $op_j$ and $\eta$ with $M_j$ and $M_\eta$, respectively.

The C function recursively swaps $C(\lambda x. \cdot)$ with $op M_p(\lambda y. \cdot)$ using the $C_{op}$ rule. When C finally meets the $\eta$ constructor, it swaps $(\lambda x. \cdot)$ with $\eta \cdot$ and terminates. Note that the constraint $x \notin FV(M_p)$ in rule $C_{op}$ cannot be dismissed by
renaming of bound variables. If the parameter $M_p$ contains a free occurrence of $x$, the evaluation of $C$ will get stuck. $C$ is thus a partial function: it is only applicable when none of the operations being commuted with the $\lambda$-binder actually depend on the bound variable.

## 2.4 Common Combinators

When demonstrating the calculus in the next section, the following combinators will be helpful. First, we define a sequencing operator. The operator $\gg=$, called bind, replaces all the $\alpha$-typed atoms of a $\mathcal{F}_E(\alpha)$-typed expression with $\mathcal{F}_E(\beta)$-typed expressions. More intuitively, $M \gg= N$ is the program that first runs $M$ to get its result $x$ and then continues as the program $N x$.

$$ \begin{array}{l} \text{\_}\gg\text{\_} : \mathcal{F}_E(\alpha) \rightarrow (\alpha \rightarrow \mathcal{F}_E(\beta)) \rightarrow \mathcal{F}_E(\beta) \\ M \gg= N = (|\eta: N|) M \end{array} $$

The type constructor $\mathcal{F}_E$ along with the operators $\eta$ and $\gg=$ form a free monad. Using this monadic structure, we can define the following combinators (variations on application) which we will make heavy use of in Section 3.

$$ \begin{array}{l} \text{\_}\ll\text{\_} : \mathcal{F}_E(\alpha \rightarrow \beta) \rightarrow \alpha \rightarrow \mathcal{F}_E(\beta) \\ F \ll\cdot x = F \gg= (\lambda f. \eta (f x)) \\ \text{\_}\gg\text{\_} : (\alpha \rightarrow \beta) \rightarrow \mathcal{F}_E(\alpha) \rightarrow \mathcal{F}_E(\beta) \\ f \gg X = X \gg= (\lambda x. \eta (f x)) \\ \text{\_}\ll\gg\text{\_} : \mathcal{F}_E(\alpha \rightarrow \beta) \rightarrow \mathcal{F}_E(\alpha) \rightarrow \mathcal{F}_E(\beta) \\ F \ll\gg\gg X = F \gg= (\lambda f. X \gg= (\lambda x. \eta (f x))) \end{array} $$

All of these operators associate to the left, so $f \gg X \ll\gg Y$ should be read as $(f \gg X) \ll\gg Y$.

Let $\circ : o \rightarrow o \rightarrow o$ be a binary operator on propositions. We define the following syntax for the same operator lifted to computations of propositions.

$$ \begin{array}{l} \text{\_\bar{o}\_} : \mathcal{F}_E(o) \rightarrow \mathcal{F}_E(o) \rightarrow \mathcal{F}_E(o) \\ M \bar{o} N = (\lambda mn. m \circ n) \gg M \ll\gg N \end{array} $$

# 3 Linguistic Phenomena as Effects

## 3.1 Deixis

We will now try to use this calculus to do some semantics. Here is our tectogrammar in an abstract categorial grammar presentation [5].

JOHN, MARY, ME : NP

LOVES : NP $\to$ NP $\to$ S
And here is our semantics.

$$ 
\begin{align*}
\llbracket \text{JOHN} \rrbracket &:= \eta \mathbf{j} \\
\llbracket \text{MARY} \rrbracket &:= \eta \mathbf{m} \\
\llbracket \text{ME} \rrbracket &:= \text{speaker} \star (\lambda x. \eta x) \\
\llbracket \text{LOVES} \rrbracket &:= \lambda \mathcal{O} \mathcal{S}. \text{love} \cdot \gg S \ll \gg O
\end{align*}
$$

In the semantics for $\llbracket ME \rrbracket$, we use the speaker operation to retrieve the current speaker and make it available as the value of the variable $x$. The star $(\star)$ passed to speaker is a dummy value of the unit type 1.

This, and all the semantics we will see in this paper, satisfies a homomorphism condition that whenever $M : \tau$, then $\llbracket M \rrbracket : \llbracket \tau \rrbracket$. In our case, $\llbracket NP \rrbracket = \mathcal{F}_E(\iota)$ and $\llbracket S \rrbracket = \mathcal{F}_E(o)$, where $\iota$ and $o$ are the types of individuals and propositions, respectively. Of $E$, we assume that speaker : $1 \to \iota \in E$, since that is the type of speaker used in our semantics.<fnref n="7" />

With this fragment, we can give meanings to trivial sentences like:

(1) John loves Mary.

(2) Mary loves me.

whose meanings we can calculate as:

$$ \llbracket \text{LOVES MARY JOHN} \rrbracket \to \eta (\mathbf{love} \mathbf{j} \mathbf{m}) \quad (1) $$

$$ \llbracket \text{LOVES ME MARY} \rrbracket \to \text{speaker} \star (\lambda x. \eta (\mathbf{love} \mathbf{m} x)) \quad (2) $$

The meaning of (1) is a proposition of type $o$ wrapped in $\eta$, i.e. something that we can interpret in a model. As for the meaning of (2), the speaker operator has propagated from the ME lexical entry up to the meaning of the whole sentence. We now have an algebraic expression having as operands the propositions $\mathbf{love} \mathbf{m} x$ for all possible $x : \iota$. In order to get a single proposition which is to be seen as the truth-conditional meaning of the sentence and which can be evaluated in a model, we will need to fix the speaker. We will do so by defining an interpreting handler.

$$ \begin{align*} \text{withSpeaker} : \iota \to \mathcal{F}_{\{\text{speaker}:1 \to \iota\} \psi_E}(\alpha) &\to \mathcal{F}_E(\alpha) \\ \text{withSpeaker} = \lambda s M. (\llbracket \text{speaker}: (\lambda x. k. s) \rrbracket) &\to M \end{align*} $$

Note that we omitted the $\eta$ clause in the banana brackets above. In such cases, we say there is a default clause $\eta: (\lambda x. \eta x)$.

$$ \text{withSpeaker } s \llbracket \text{LOVES ME MARY} \rrbracket \to \eta (\mathbf{love} \mathbf{m} s) $$

So far, we could have done the same by introducing a constant named **me** to stand in for the speaker. However, since handlers are part of our object language,

<footnote n="7">⁷ 1 is the unit type whose only element is written as $\star$.</footnote>
we can include them in lexical entries. With this, we can handle phenomena such as direct (quoted) speech, that rebinds the current speaker in a certain scope.

$$ \text{SAID}_{\text{IS}} : S \to \text{NP} \to S $$

$$ \text{SAID}_{\text{DS}} : S \to \text{NP} \to S $$

Those are our new syntactic constructors: one for the indirect speech use of *said* and the other for the direct speech use (their surface realizations would differ typographically or phonologically). Let us give them some semantics.

$$ [[\text{SAID}_{\text{IS}}]] = \lambda C S . \text{say} \cdot \gg S \ll \gg C $$

$$ = \lambda C S . S \gg = (\lambda s . \text{say} s \cdot \gg C) $$

$$ [[\text{SAID}_{\text{DS}}]] = \lambda C S . S \gg = (\lambda s . \text{say} s \cdot \gg (\text{withSpeaker } s C)) $$

Here we elaborated the entry for indirect speech so it is easier to compare with the one for direct speech, which just adds a use of the withSpeaker operator.

(3) John said Mary loves me.

(4) John said, “Mary loves me”.

$$ [[\text{SAID}_{\text{IS}} (\text{LOVES ME MARY}) \text{JOHN}}] \to \text{speaker} \star (\lambda x . \eta (\text{say j (love m x)})) \quad (3) $$

$$ [[\text{SAID}_{\text{DS}} (\text{LOVES ME MARY}) \text{JOHN}}] \to \eta (\text{say j (love m j)}) \quad (4) $$

The meaning of sentence (3) depends on the speaker (as testified by the use of the speaker operator) whereas in (4), this dependence has been eliminated due to the use of direct speech.

## 3.2 Quantification

Now we turn our attention to quantificational noun phrases.

$$ \text{EVERY, A} : N \to \text{NP} $$

$$ \text{MAN, WOMAN} : N $$

$$ [[\text{EVERY}}] := \lambda N . \text{scope} (\lambda c . \forall \cdot \gg (C (\lambda x . (N \ll \cdot x) \Rightarrow (c x)))) (\lambda x . \eta x) $$

$$ [[\text{A}}] := \lambda N . \text{scope} (\lambda c . \exists \cdot \gg (C (\lambda x . (N \ll \cdot x) \bar{\wedge} (c x)))) (\lambda x . \eta x) $$

$$ [[\text{MAN}}] := \eta \text{man} $$

$$ [[\text{WOMAN}}] := \eta \text{woman} $$

The entries for EVERY and A might seem intimidating. However, if we ignore the $\gg$, the C, the $\ll$ and the overline on the logical operator, we get the familiar generalized quantifiers. These decorations are the plumbing that takes care of the proper sequencing of effects.

Note that we make use of the C operator here. In the denotation of $[[A]]$, the term $(\lambda x . (N \ll \cdot x) \bar{\wedge} (c x))$ describes the property to which we want to apply the quantifier $\exists$. However, this term is of type $\iota \to \mathcal{F}_E(o)$. In order to apply
∃, we need something of type $ι \to o$. Intuitively, the effects of E correspond to the process of interpretation, the process of arriving at some logical form of the sentence. They should thus be independent of the particular individual that we use as a witness for $x$ when we try to model-check the resulting logical form. This independence allows us use the $C$ operator without fear of getting stuck. Once we arrive at the type $\mathcal{F}_E(ι \to o)$, it is a simple case of using $∃ \cdot \gg _-$ to apply the quantifier within the computation type.⁸⁹

While the terms that use the **scope** operator might be complex, the handler that interprets them is as simple as can be.

$$ SI = \lambda M. (\llbracket \mathbf{scope} : (\lambda ck. ck) \rrbracket M) $$

Same as with withSpeaker, SI will also be used in lexical items. By interpreting the **scope** operation in a particular place, we effectively determine the scope of the quantifier. Hence the name of SI, short for Scope Island. If we want to model clause boundaries as scope islands, we can do so by inserting SI in the lexical entries of clause constructors (in our case, the verbs).

$$ \llbracket \mathbf{LOVES} \rrbracket := \lambda OS. SI (\llbracket \mathbf{LOVES} \rrbracket OS) $$

$$ \llbracket \mathbf{SAID}_{\mathbf{IS}} \rrbracket := \lambda CS. SI (\llbracket \mathbf{SAID}_{\mathbf{IS}} \rrbracket CS) $$

$$ \llbracket \mathbf{SAID}_{\mathbf{DS}} \rrbracket := \lambda CS. SI (\llbracket \mathbf{SAID}_{\mathbf{DS}} \rrbracket CS) $$

Whenever we use the semantic brackets on the right-hand side of these revised definitions, they stand for the denotations we have assigned previously.

(5) Every man loves a woman.

(6) John said every woman loves me.

(7) John said, “Every woman loves me”.

$$ \llbracket \mathbf{LOVES} \text{ (A WOMAN) (EVERY MAN)} \rrbracket \\ \rightarrow \eta (\forall x. \mathbf{man} x \rightarrow (\exists y. \mathbf{woman} y \wedge \mathbf{love} x y)) \qquad (5) $$

$$ \text{withSpeaker } s \llbracket \mathbf{SAID}_{\mathbf{IS}} \text{ (LOVES ME (EVERY WOMAN)) JOHN} \rrbracket \\ \rightarrow \eta (\mathbf{say} \mathbf{j} (\forall x. \mathbf{woman} x \rightarrow \mathbf{love} x s)) \qquad (6) $$

$$ \llbracket \mathbf{SAID}_{\mathbf{DS}} \text{ (LOVES ME (EVERY WOMAN)) JOHN} \rrbracket \\ \rightarrow \eta (\mathbf{say} \mathbf{j} (\forall x. \mathbf{woman} x \rightarrow \mathbf{love} x \mathbf{j})) \qquad (7) $$

The calculus offers us flexibility when modelling the semantics. We might choose to relax the constraint that clauses are scope islands by keeping the old

<footnote n="8">⁸ Other solutions to this problem include separating the language of logical forms and the metalanguage used in the semantic lexical entries to manipulate logical forms as objects [13].</footnote>

<footnote n="9">⁹ Our $C$ has been inspired by an operator of the same name proposed in [9]: de Groote introduces a structure that specializes applicative functors in a similar direction as monads by introducing the $C$ operator and equipping it with certain laws; our $C$ operator makes the $\mathcal{F}_E$ type constructor an instance of this structure.</footnote>
entries for verbs that do not use the SI handler. We might then want to add the SI handler to the lexical entry of SAID<sub>DS</sub>, next to the withSpeaker handler, so that quantifiers cannot escape quoted expressions. We might also allow for inverse scope readings by, e.g., providing entries for transitive verbs that evaluate their arguments right-to-left (though then we would have to watch out for crossover effects if we were to add anaphora).

## 3.3 Conventional Implicature

Our goal is to show the modularity of this approach and so we will continue and plug in one more phenomenon into our growing fragment: conventional implicatures, as analyzed by Potts [23]. Specifically, we will focus on nominal appositives.

$$ \text{APPOS} : NP \to NP \to NP $$

$$ \text{BEST-FRIEND} : NP \to NP $$

$$ [[\text{APPOS}] := \lambda X Y . X \gg (\lambda x . \text{SI}(\eta x \equiv Y) \gg (\lambda i . \text{implicate}_i(\lambda z . \eta x))) $$

$$ [[\text{BEST-FRIEND}] := \lambda X . \text{best-friend} \gg X $$

In the denotation of the nominal appositive construction, APPOS, we first evaluate the head noun phrase X : [[NP]] to find its referent x : t. We then want to implicate that x is equal to the referent of Y. The term ηx ≡ Y (note the line over =) is the term that computes that referent and gives us the proposition we want. We also want to state that no quantifier from within the appositive Y should escape into the matrix clause and so we wrap this computation in the SI handler to establish a scope island. Finally, we pass this proposition as an argument to implicate and we return x as the referent of the noun phrase.

The point of the implicate operation is to smuggle non-at-issue content outside the scope of logical operators. The contribution of an appositive should survive, e.g., logical negation.<fnref n="10" /> The place where we will accommodate the implicated truth-conditions will be determined by the use of the following handler:

$$ \text{accommodate} : \mathcal{F}_{\{\text{implicate}:o \to 1\} \lor E}(o) \to \mathcal{F}_E(o) $$

$$ \text{accommodate} = \lambda M. (\lfloor \text{implicate} : (\lambda ik. \eta i \wedge k \star) \rfloor M) $$

We want conventional implicatures to project out of the common logical operators. However, when we consider direct quotes, we would not like to attribute the implicature made by the quotee to the quoter. We can implement this by inserting the accommodate handler into the lexical entry for direct speech.

$$ [[\text{SAID}_{\text{DS}}]] := \lambda CS . \text{SI}(S \gg (\lambda s. \text{say } s \gg (\text{withSpeaker } s \text{ (accommodate } C \text{)}))) $$

Consider the following three examples.

<footnote n="10">¹⁰ In our limited fragment, we will only see it sneak out of a quantifier.</footnote>
(8) John, my best friend, loves every woman.

(9) Mary, everyone's best friend, loves John.

(10) A man said, “My best friend, Mary, loves me”.

In (8), the conventional implicature that John is the speaker's best friend projects from the scope of the quantifier. On the other hand, in (10), the implicature does not project from the quoted clause and so it is not misattributed.

with Speaker s (accommodate [[LOVES (EVERY WOMAN) (APPOS JOHN (BEST-FRIEND ME))]])

$$ \rightarrow \eta ((\mathbf{j} = \mathbf{best-friend} s) \wedge (\forall x. \mathbf{woman} x \rightarrow \mathbf{love} \mathbf{j} x)) \qquad (8) $$

accommodate [[LOVES JOHN (APPOS MARY (BEST-FRIEND EVERYONE))]]

$$ \rightarrow \eta ((\forall x. \mathbf{m} = \mathbf{best-friend} x) \wedge (\mathbf{love} \mathbf{m} \mathbf{j})) \qquad (9) $$

[[SAID<sub>DS</sub> (LOVES ME (APPOS (BEST-FRIEND ME) MARY)) (A MAN)]]

$$ \rightarrow \eta (\exists x. \mathbf{man} x \wedge \mathbf{say} x ((\mathbf{best-friend} x = \mathbf{m}) \wedge (\mathbf{love} (\mathbf{best-friend} x) x))) \qquad (10) $$

## 3.4 Summary

Let us look back at the modularity of our approach and count how often during the incremental development of our fragment we either had to modify existing denotations or explicitly mention previous effects in new denotations.

When adding quantification:

- in the old denotations of verbs, we added the new SI handler so that clauses form scope islands

When adding appositives and their conventional implicatures:

- in the old denotations [[SAID<sub>DS</sub>]], we added the new accommodate handler to state that conventional implicatures should not project out of quoted speech

- in the new denotation [[APPOS]], we used the old SI handler to state that appositives should form scope islands

Otherwise, none of the denotations prescribed in our semantic lexicon had to be changed. We did not have to type-raise non-quantificational NP constructors like [[JOHN]], [[ME]] or [[BEST-FRIEND]]. With the exception of direct speech, we did not have to modify any existing denotations to enable us to collect conventional implicatures from different subconstituents.

Furthermore, all of the modifications we have performed to existing denotations are additions of handlers for new effects. This gives us a strong guarantee that all of the old results are conserved, since applying a handler to a computation which does not use the operations being handled changes nothing.

The goal of our calculus is to enable the creation of semantic lexicons with a high degree of separation of concerns. In this section, we have seen how it can be done for one particular fragment.
# 4 Properties of the Calculus

The calculus defined in Sect. 2 and to which we will refer as $\langle\lambda\rangle$, has some
satisfying properties.

First of all, the reduction rules preserve types of terms (subject reduction).
The reduction relation itself is confluent and, for well-typed terms, it is also
terminating. This means that typed $\langle\lambda\rangle$ is strongly normalizing.

The proof of subject reduction is a mechanical proof by induction. For conflu-
ence and termination, we employ very similar strategies: we make use of general
results and show how they apply to our calculus. Due to space limitations, we
will pursue in detail only the proof of confluence.

Our reduction relation is given as a set of rules which map redexes matching
some pattern into contracta built up out of the redexes' free variables. However,
our language also features binding, and so some of the rules are conditioned on
whether or not certain variables occur freely in parts of the redex. Fortunately,
such rewriting systems have been thoroughly studied. Klop's Combinatory Re-
duction Systems (CRSs) [16] is one class of such rewriting systems.

We will make use of the result that orthogonal CRSs are confluent [16]. A CRS
is orthogonal if it is left-linear and non-ambiguous. We will need to adapt our
formulation of the reduction rules so that they form a CRS and we will need
to check whether we satisfy left-linearity and non-ambiguity (we will see what
these two properties mean when we get to them).

We refer the reader to [16] for the definition of CRSs. The key point is that
in a CRS, the free variables which appear in the left-hand side of a rewrite rule,
called metavariables, are explicitly annotated with the set of all free variables
that are allowed to occur within a term which would instantiate them. This
allows us to encode all of our $x \notin FV(M)$ constraints.

One detail which must be taken care of is the set notation $(\mathbf{op}_i : M_i)_{i \in I}$ and
the indices $I$ used in the $\langle\rangle$ rules. We do away with this notation by adding a
separate rule for every possible instantiation of the schema. This means that for
each sequence of distinct operation symbols $\mathbf{op}_1, \dots, \mathbf{op}_n$, we end up with:

- a special rewriting rule $\langle \mathbf{op}_1 : M_1, \dots, \mathbf{op}_n : M_n, \eta : M_\eta \rangle (\eta N) \rightarrow M_\eta N$

- for every $1 \le i \le n$, a special rewriting rule

$$ 
\begin{align*}
& \langle \mathbf{op}_1 : M_1, \dots, \mathbf{op}_n : M_n, \eta : M_\eta \rangle (\mathbf{op}_i N_p (\lambda x. N_c(x))) \\
& \rightarrow M_i N_p (\lambda x. (\langle \mathbf{op}_1 : M_1, \dots, \mathbf{op}_n : M_n, \eta : M_\eta \rangle N_c(x)))
\end{align*}
$$

- for every $\mathbf{op}' \in \mathcal{E} \setminus \{\mathbf{op}_i | 1 \le i \le n\}$, a special rewriting rule

$$ 
\begin{align*}
& \langle \mathbf{op}_1 : M_1, \dots, \mathbf{op}_n : M_n, \eta : M_\eta \rangle (\mathbf{op}'_i N_p (\lambda x. N_c(x))) \\
& \rightarrow \mathbf{op}'_i N_p (\lambda x. (\langle \mathbf{op}_1 : M_1, \dots, \mathbf{op}_n : M_n, \eta : M_\eta \rangle N_c(x)))
\end{align*}
$$

So now we have a CRS which defines the same reduction relation as the rules
we have shown in 2.3. Next, we verify the two conditions. Left-linearity states
that no left-hand side of any rule contains multiple occurrences of the same
metavariable. By examining our rules, we find that this is indeed the case.<fnref n="11" />

<footnote n="11">¹¹ Multiple occurrences of the same $\mathbf{op}_i$ are alright, since those are not metavariables.</footnote>
Non-ambiguity demands that there is no non-trivial overlap between any of the left-hand sides.<fnref n="12" /> In our CRS, we have overlaps between the $\beta$ and the $\eta$ rules. We split our CRS into one with just the $\eta$ rule ($\rightarrow_{\eta}$) and one with all the other rules ($\rightarrow_{\{\lambda\}}$). Now, there is no overlap in either of these CRSs, so they are both orthogonal and therefore confluent.

We then use the Lemma of Hindley-Rosen [17, p. 7] to show that the union of $\rightarrow_{\{\lambda\}}$ and $\rightarrow_{\eta}$ is confluent when $\rightarrow_{\{\lambda\}}$ and $\rightarrow_{\eta}$ are both confluent and commute together. For that, all that is left to prove is that $\rightarrow_{\{\lambda\}}$ and $\rightarrow_{\eta}$ commute. Thanks to another result due to Hindley [17, p. 8], it is enough to prove that for all $a$, $b$ and $c$ such that $a \rightarrow_{\{\lambda\}} b$ and $a \rightarrow_{\eta} c$, we have a $d$ such that $b \rightarrow_{\eta} d$ and $c \rightarrow_{\{\lambda\}} d$. The proof of this is a straightforward induction on the structure of $a$.

# 5 Conclusion

In our contribution, we have introduced a new calculus motivated by modelling detailed semantics and inspired by current work in programming language theory. Our calculus is an extension of the simply-typed lambda calculus which is the de facto lingua franca of semanticists. Its purpose is to facilitate the communication of semantic ideas without depending on complex programming languages [19,15] and to do so with a well-defined formal semantics.

We have demonstrated the features of our calculus on several examples exhibiting phenomena such as deixis, quantification and conventional implicature. While our calculus still requires us to do some uninteresting plumbing to be able to correctly connect all the denotations together, we have seen that the resulting denotations are very generic. We were able to add new phenomena without having to change much of what we have done before and the changes we have made arguably corresponded to places where the different phenomena interact.

Finally, we have also shown that the calculus shares some of the useful properties of the simply-typed lambda calculus, namely strong normalization.

In future work, it would be useful to automate some of the routine plumbing that we have to do in our terms. It will also be important to test the methodology on larger and more diverse fragments (besides this fragment, we have also created one combining anaphora, quantification and presupposition [19]). Last but not least, it would be interesting to delve deeper into the foundational differences between the approach used here, the monad transformers used by Charlow [4] and the applicative functors used by Kiselyov [13].

# References

1. Barker, C.: Continuations and the nature of quantification. Natural language semantics 10(3), 211–242 (2002)

2. Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program. 84(1), 108–123 (2015)

<footnote n="12">¹² The definition of (non-trivial) overlap is the same one as the one used when defining critical pairs. See [16] for the precise definition.</footnote>
3. Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: ACM SIGPLAN Notices (2013)

4. Charlow, S.: On the semantics of exceptional scope. Ph.D. thesis, New York University (2014)

5. de Groote, P.: Towards abstract categorial grammars. In: Proceedings of the 39th Annual Meeting on Association for Computational Linguistics (2001)

6. de Groote, P.: Type raising, continuations, and classical logic. In: Proceedings of the thirteenth Amsterdam Colloquium (2001)

7. de Groote, P.: Towards a montagovian account of dynamics. In: Proceedings of SALT. vol. 16 (2006)

8. Giorgolo, G., Asudeh, A.: Natural language semantics with enriched meanings (2015)

9. de Groote, P.: On Logical Relations and Conservativity. In: NLCS'15. Third Workshop on Natural Language and Computer Science (2015)

10. Hobbs, J., Rosenschein, S.: Making computational sense of montague's intensional logic. Artificial Intelligence 9(3), 287-306 (1977)

11. Kammar, O., Lindley, S., Oury, N.: Handlers in action. In: ACM SIGPLAN Notices (2013)

12. Kamp, H., Reyle, U.: From discourse to logic. Kluwer Academic Pub (1993)

13. Kiselyov, O.: Applicative abstract categorial grammars. In: Proceedings of the Third Workshop on Natural Language and Computer Science (2015)

14. Kiselyov, O., Sabry, A., Swords, C.: Extensible effects: an alternative to monad transformers. In: ACM SIGPLAN Notices (2013)

15. Kiselyov, O., Shan, C.c.: Lambda: the ultimate syntax-semantics interface (2010)

16. Klop, J.W., Van Oostrom, V., Van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical computer science (1993)

17. Klop, J.W., et al.: Term rewriting systems. Handbook of logic in computer science 2, 1-116 (1992)

18. Lebedeva, E.: Expression de la dynamique du discours à l'aide de continuations. Ph.D. thesis, Université de Lorraine (2012)

19. Maršík, J., Amblard, M.: Algebraic Effects and Handlers in Natural Language Interpretation. In: Natural Language and Computer Science (Jul 2014)

20. Meijer, E., Fokkinga, M., Paterson, R.: Functional programming with bananas, lenses, envelopes and barbed wire. In: Functional Programming Languages and Computer Architecture (1991)

21. Moggi, E.: Notions of computation and monads. Information and computation 93(1), 55-92 (1991)

22. Plotkin, G., Pretnar, M.: Handlers of algebraic effects. In: Programming Languages and Systems, pp. 80-94. Springer (2009)

23. Potts, C.: The logic of conventional implicatures. Oxford University Press (2005)

24. Pretnar, M.: Logic and handling of algebraic effects. Ph.D. thesis, The University of Edinburgh (2010)

25. Qian, S., Amblard, M.: Event in compositional dynamic semantics. In: Logical Aspects of Computational Linguistics. Springer (2011)

26. Shan, C.: Monads for natural language semantics. arXiv cs/0205026 (2002)

27. Shan, C.: Linguistic side effects. Ph.D. thesis, Harvard University (2005)

28. Van Eijck, J., Unger, C.: Computational semantics with functional programming. Cambridge University Press (2010)

29. Wadler, P.: The essence of functional programming. In: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (1992)