A Simultaneous Abstraction Calculus and Theories of Semantics

Peter Ruhrberg^{∗} peru@cogsci.ed.ac.uk

May 19, 1998

Abstract

I define a simple calculus of simultaneous abstraction, and show how it can provide the basis for property-theoretic reconstructions of Dynamic Montague Grammar and Discourse Representation Theory. The system can also be used for some forms of Situation Theory, instead of parametric objects and Aczel–Lunnon abstraction.

1 Introduction

There are close similarities between some of the most influential semantic theories of our time, such as Discourse Representation Theory (DRT), see [Kamp 1981] and [Zeevat 1991], Dynamic Montague Grammar (DMG), see [Groenendijk & Stokhof 1990], especially when based on the Dynamic Property Theory (DPT) of [Chierchia 1992], and Situation Theory (ST), as described in [Barwise & Cooper 1991], with its underlying theory of abstraction (AL) developed in [Aczel & Lunnon 1991]. They all can be construed as involving forms of simultaneous abstraction. In DRT we have a set of discourse markers as one ingredient of a DRS, though one usually doesn’t think of them as being abstracted over. We will show a pretty straightforward way of rendering them as abstractions. In DPT the ^{⊓}-operator can be understood as abstracting over the infinite set of discourse markers, which are a subsort of the variables. In AL we take a one-one mapping of roles to parameters as input to abstract over a set of parameters in one go.

Abstraction over an unordered set of variables, or parameters, creates the problem of defining a sensible operation of application which unambiguously determines which of the objects applied to fill which of the positions abstracted over. The solution to this difficulty comes in the form of application to assignments. These abstracts denote, or correspond to, functions from assignments to objects of some kind. They are thus rather like open formulas in standard logics which have their semantics given in terms of functions from assignments to denotations. In the same vein DRSs can be taken to denote, under an assignment, a set of verifying “embeddings,” that is, a function from variable assignments to truth values. In DPT functions from discourse marker assignments to propositions are first class citizens of the semantic domain itself, and in AL the application operation is defined on assignments of entities to role indices.

∗I thank Lawrence Cavedon, Robin Cooper, Rachel Lunnon and Paul Schweizer for criticism and support. This research was funded in part by ESPRIT BR6852 (DYANA-2) and LRE 62-051 (FraCaS).

It seems worthwhile to look for a common core which brings out the similarities as well as the differences between these theories more clearly and with formal precision. This core is our Simultaneous Abstraction Calculus. Semantic theories can be obtained from it by giving axioms of properties, propositions and truth, which again may be shared to some extent across competing theories. One may group the axioms into convenient packages under the banner of “abstract specification,” thus creating a framework that should facilitate the comparison of existing theories as well as the development of alternatives. DMG and DRT for example, which we concentrate on in this paper, share a common theory of identity and propositional logic, but diverge in the kinds of quantification they employ. ST might be obtained by adding a logic of situation types to such unsituated theories of propositions. I can only give a sketchy account of these matters here, and also must leave the topic of relating these semantic objects to natural language utterances largely in the background.

1.1 Variables: “Bound yet Free”

As a consequence of the idea of simultaneous abstraction we will face a certain loss of α-equivalence. This is an inevitable result of the way in which application has to work for such terms. A renaming of variables will normally change the object as it will yield different results when applied to the same assignment. This should come as no surprise: it is of course well known that free variables cannot be renamed, but neither can the “abstracted” discourse markers of a DRS be changed without consequences. The same holds true for DPT discourse markers under ^{⊓}-abstraction. Parameters in AL can be renamed, if abstracted over, but role indices cannot without changing the object.

I will not embark into an argument about whether it is wrong to speak of “abstraction” when there is no α-equivalence. It is more important to see that it is not a virtue in itself to be able to rename variables, as this means that computational work has to be done to establish a trivial identity of objects. Its virtue, as we shall see, lies in obtaining a total substitution operation, which is essential for the full exploitation of β-equivalences.

The idea that variables may be essential to the identity of a semantic object is certainly now fairly accepted, due to DRT and its “dynamic” children. From a more philosophical perspective I would argue that using variables in this way is no more a contamination of semantic objects by non semantic concepts than the common view that the order of arguments to a many place function should matter.

2 The Simultaneous Abstraction Calculus

In this section I introduce the basic formalism for simultaneous abstraction. I then add an operation of partial application to it, and compare the system to a similar one which is closer to Aczel and Lunnon’s approach. Finally I take a look at possibly non well-founded structured objects.

2.1 The Basic Calculus

Instead of abstracting over single variables, as in standard λ-calculus, we allow λabstraction over any set of them. Terms are applied to records assigning terms to variables. For the rest of the paper, differently indexed variables are assumed to be non-identical.

Definition 1 The language Λ consists of terms t, t′ … built up from basic type free constants c, c′ …, and # for “undefined,” and variables x, y … ∈ Var by means of abstraction λM.t, for M ⊆ Var, and application t(x_{1}.t_{1}, …, x_{n}.t_{n}).

We in fact allow infinite sets of variables to be abstracted over and also infinite records (x_{i}.t_{i})_{i∈I} to be applied to. We often write {x_{1}..x_{n}}t instead of λ{x_{1}, .., x_{n}}.t, without meaning to imply that n has to be a finite number. A similar remark holds for application terms. Ways of introducing standard abstraction and application into such a system will be discussed later on.

Semantically, we will be working in the category CPO of complete partial orders and continuous functions. So a domain will always be understood to be a cpo with a least element ⊥, a mapping between cpo’s to be continuous, and the operation → to form the space of continuous functions, ordered pointwise.^{1} g_{f}^{M} is defined by g_{f}^{M}(x) = f(x) if x ∈ M, otherwise g_{f}^{M}(x) = g(x), for all x ∈ Var. Letting dom(f) = {a|f(a) ≠ ⊥} I will use the notation g ≀ f for g_{f}^{dom(f)}. We write ⟨x_{i} ↦ ξ_{i}⟩_{i∈I} for the function f such that f(x_{i}) = ξ_{i} for i ∈ I and f(x) = ⊥ otherwise. A retraction between two domains, written D ⇀ ↽_{Φ}^{Ψ} C, is a pair of mappings Ψ : D → C and Φ : C → D such that Ψ ∘ Φ = id_{C}.

Definition 2 A Λ-model consists of a retraction D ⇀ ↽_{Φ}^{Ψ} (Var → D) → D, and an interpretation ℑ which maps constants into D, with ℑ(#) = ⊥_{D}. The denotation of terms under a variable assignment g is given by:^{2}

• ∥c∥^{g} = ℑ(c);

• ∥x∥^{g} = g(x);

• ∥λM.t∥^{g} = Φ λf∥t∥^{g_{f}^{M}}; • ∥t(x_{i}.t_{i})_{i∈I}∥^{g} = Ψ(∥t∥^{g}) (⟨x_{i} ↦ ∥t_{i}∥^{g}⟩_{i∈I}).

1In some cases they will be required to be strict, preserving the bottom element. For background information notions see [Barendregt 1984]. Notice that every partial assignment function is continuous (if strict), given that Var is a flat domain with an added ⊥.

2The third clause has its predecessor in [Zeevat 1990], where abstraction over the sets of variables of a common type was defined in a reconstruction of DMG. The ‘λ’ on the right is used as an expression of the meta language in this clause, with the expected meaning.

The denotations are only well-defined because the following holds:^{3}

Theorem 1 λf∥t∥^{g_{f}^{M}} is continuous for all terms t.

Definition 3 The free variables of a term are defined by

• F V (x) = {x};

• F V (c) = ∅;

• F V (λM.t) = F V (t) \ M;

• F V (t(x_{i}.t_{i})_{i∈I}) = F V (t) ∪ ⋃_{i∈I} F V (t_{i}).

Lemma 2 If x ∉ F V (t) then ∥t∥^{g} = ∥t∥^{g_{d}^{x}} for all g and d.

In such a case the denotation of t is independent of what we assign to x, but this does not mean one could rename x by some y of which t is independent as well. For example {x}x is independent of x and y, but ∥{x}x∥^{g} ≠ ∥{y}y∥^{g}. The latter becomes clear when we apply these two functions to suitable assignments e.g., ∥{x}x (x.a, y.b)∥^{g} = ∥a∥^{g} ≠ ∥b∥^{g} = ∥{y}y (x.a, y.b)∥^{g}, presuming our model is non trivial.

Definition 4 Simultaneous substitution [s_{j}/y_{j}]_{j∈J} (dropping the index set when no confusion can arise) is a partially defined operation given by:

• [s_{j}/y_{j}]_{j∈J}x = s_{j}, if x = y_{j} for some j ∈ J, otherwise x;

• [s_{j}/y_{j}]c = c;

• [s_{j}/y_{j}]_{j∈J}λM.t = λM.[s_{i}/y_{i}]_{i∈I}t, where I = J \ {j| y_{j} ∈ M}, if M ∩ ⋃_{i∈I} F V (s_{i}) = ∅, otherwise undefined;

• [s_{j}/y_{j}] t(x_{i}.t_{i})_{i∈I} = [s_{j}/y_{j}]t (x_{i}.[s_{j}/y_{j}]t_{i})_{i∈I}.

An example of an undefined substitution would be [y/x]{y}t_{xy}, where replacing x in t_{xy} by y would give undesired results and renaming y is not a possibility. To avoid such trouble we require a fresh variable for a term to occur neither free nor bound in it.

Let us say that Λ ⊧ t = t′ iff for every Λ-model and assignment ∥t∥^{g} = ∥t′∥^{g}.

Theorem 3 1. Λ |̸= {x_{1}..x_{n}}t = {y_{1}..y_{n}}[y_{i}/x_{i}]t,

2. Λ |̸= {x_{1}..x_{n}}{x_{n+1}..x_{n+m}}t = {x_{1}..x_{n+m}}t.

Lemma 4 ∥t∥^{γ} = ∥[t_{i}/x_{i}]_{i∈I} t∥^{g} if [t_{i}/x_{i}]t is defined, where γ = g ≀ ⟨x_{i} ↦ ∥t_{i}∥^{g}⟩_{i∈I}.

3Proofs are generally omitted from this paper. None of them is particularly interesting or involved.

The following equations can now be shown to hold, where the list is not meant to be complete. The fact that substitution is not always defined is responsible for the difficulties in giving such a list. Fact 5.3, which allows for some amount of renaming of variables, is just one example of an equation that cannot be derived from 5.2 for this reason. It seems a good idea to look for a complete calculus for Λ_{AL}, defined below, before doing the same for Λ since substitution can be totally defined in that system.

Theorem 5 1. Λ ⊧ λM.t = λN.t for N = M ∩ F V (t);

2. Λ ⊧ {x_{i}}_{i∈I}t (x_{j}.t_{j})_{j∈J} = [t_{j}/x_{j}, #/x_{i}]_{j∈J′,i∈I′} t , with J′ = J ∩ I and I′ = I \ J, if the substitution is defined.

3. Λ ⊧ {x_{i}}_{i∈I}t (x_{i}.t_{i})_{i∈I} = {z_{i}}_{i∈I}[z_{i}/x_{i}]_{i∈I}t (z_{i}.t_{i})_{i∈I}, where all z_{i} are fresh.

2.2 Partial Application

It is very natural to ask for an operation for partially filling the argument roles of a relation, leaving some of them simply open for more to come. We use the notation t[x_{1}.t_{1}, .., x_{n}.t_{n}] for partial application. The semantics is as follows:

∥t[x_{i}.t_{i}]_{i∈I}∥^{g} =_{df} Φλf Ψ∥t∥^{g} (f ≀ ⟨x_{i} ↦ ∥t_{i}∥^{g}⟩_{i∈I}) .

The following properties of partial application are of particular interest, letting application associate to the left.

Theorem 6 1. Λ ⊧ {x_{i}}_{i∈I}t [x_{j}.t_{j}]_{j∈J} = [t_{j}/x_{j}]_{j∈J′}{x_{i}}_{i∈I′}t, if defined, where J′ = J ∩ I and I′ = I \ J;

2. Λ ⊧ t[x_{i}.t_{i}]_{i∈I}[y_{j}.s_{j}]_{j∈J} = t[x_{i}.t_{i}, y_{j}.s_{j}]_{i∈I,j∈J′} where J′ = J \ {j | ∃i y_{j} = x_{i}};

3. Λ ⊧ t[x_{i}.t_{i}]_{i∈I}(y_{j}.s_{j})_{j∈J} = t(x_{i}.t_{i}, y_{j}.s_{j})_{i∈I,j∈J′} where J′ = J \ {j | ∃i y_{j} = x_{i}}.

2.3 Aczel–Lunnon Abstraction

The SAC is closely related to Barwise and Cooper’s Extended Kamp Notation (EKN), see [Barwise & Cooper 1991], which is based on Aczel and Lunnon’s theory of abstraction. In EKN λ-abstraction operates on injective functions from a set of role indices to parameters. In our case those two notions are merged into one, the variables (thought of as argument roles), which allows us to replace the injections by simple sets. This makes sense because in contrast to AL our semantics does not treat the application to variables in a term like t(x.y) as a filling of the role x by some “indeterminate object” y, but rather as a linking of two roles. There is a price we pay for our simple mindedness: we cannot link a role y with any role x inside the scope of an abstraction over y by a simple application. The same problem was encountered in undefined substitutions such as [y/x]{y}t_{xy}, which indicated a certain deficit of elegance for our system. The following system revises the basic SAC to overcome this problem, using AL-style syntax for abstraction. We will show then that no additional expressive power is gained from such a move.

Definition 5 The terms of Λ_{AL} are built up from constants c, #, .. and parameters X, Y, .. by means of abstraction λχ.t over injective functions χ from parameters to variables (=roles),^{4} and total/partial application t(x_{i}.t_{i})_{i∈I} and t[x_{i}.t_{i}]_{i∈I}.

Semantically we stay in the same space of domains D ⇀ ↽_{Φ}^{Ψ} (Var → D) → D as for Λ, with the only difference being that we now interpret under assignments of objects to parameters, called anchors, and that these have to be obtained from assignments to roles when we define the meaning of abstraction.

Definition 6 A Λ_{AL}-model is a Λ-model, where the denotation of terms under an anchor g is given by:

• ∥c∥^{g} = ℑ(c);

• ∥X∥^{g} = g(X);

• ∥λχ.t∥^{g} = Φ λf∥t∥^{g≀(f∘χ)};

• ∥t(x_{i}.t_{i})_{i∈I}∥^{g} = Ψ(∥t∥^{g})(⟨x_{i} ↦ ∥t_{i}∥^{g}⟩_{i∈I});

• ∥t[x_{i}.t_{i}]_{i∈I}∥^{g} = Φλf Ψ∥t∥^{g} (f ≀ ⟨x_{i} ↦ ∥t_{i}∥^{g}⟩_{i∈I}).

This solves the problems described above as substitution is total by means of renaming parameters e.g., [X/Y]λ⟨X ↦z⟩.t_{XY} = λ⟨Z↦z⟩.t_{ZX}. The question that needs to be addressed is whether there is more to be gained, namely terms which have no equivalent in the original language Λ. To show that there are no such terms we only face one difficulty, namely that of dealing with multiple uses of roles in different levels of abstraction. Such “role recycling” is made easy by using different parameters in a term like λ⟨Y ↦ x⟩λ⟨Z ↦ x⟩.t_{Y Z}. In creating a Λ-term with the same role x used twice we face the potential problem of the outer abstraction to become vacuous. The solution is to inject an intermediate role y to arrive at {x}({y}{x}t_{yx} (y.x)). To have such roles available we assume some form of restriction on Λ_{AL} abstraction to that effect. Alternatively one might employ a way of expanding Var suitably for the purposes of translation. I will be sloppy about the details of this in the following elaboration.

Definition 7 The Translation [x_{i}/X_{i}]_{i∈I}^{†} : Λ_{AL} → Λ under a substitution of all free parameters of a Λ_{AL}-term by variables is defined by:

• [x_{i}/X_{i}]_{i∈I}^{†}X_{i} = x_{i}; • [x_{i}/X_{i}]^{†}c = c;

4In AL, the functions take roles to parameters injectively. In turning them around we could be more liberal in allowing several parameters to be mapped to the same role, which is equivalent to renaming those parameters by one of them which then gets mapped to the role in question. Notice that associating one parameter with many roles in one abstraction clearly makes no sense. Our semantics for Λ_{AL} will not presuppose injectivity, but we will assume it here nevertheless for convenience.

• [x_{i}/X_{i}]_{i∈I}^{†} λ⟨Y_{j} ↦y_{j}⟩_{j∈J}.t = (λ{z_{i}}_{i∈I′′}λ{y_{j}}_{j∈J}.[y_{j}/Y_{j}]_{j∈J}[x_{i}/X_{i}]_{i∈I′}[z_{i}/X_{i}]_{i∈I′′} ^{†}t) (z_{i}.x_{i})_{i∈I′′}, where K = I \ {i|∃j_{∈J} X_{i} = Y_{j}}, I′ = K \ {i|∃j_{∈J} x_{i} = y_{j}}, I′′ = K ∩ {i|∃j_{∈J} x_{i} = y_{j}} and the z_{i} are fresh;

• [x_{i}/X_{i}]^{†}t(y_{j}.t_{j})_{j∈J} = [x_{i}/X_{i}]^{†}t (y_{j}.[x_{i}/X_{i}]^{†}t_{j})_{j∈J};

• [x_{i}/X_{i}]^{†}t[y_{j}.t_{j}]_{j∈J} = [x_{i}/X_{i}]^{†}t [y_{j}.[x_{i}/X_{i}]^{†}t_{j}]_{j∈J}.

Lemma 7 ∥t∥^{g} = ∥[x_{i}/X_{i}]_{i∈I}^{†}t∥^{g∘π}, where π = ⟨x_{i} ↦ X_{i}⟩_{i∈I}.

Translation from Λ to Λ_{AL} is a trivial matter of renaming variables by parameters, and abstracted sets by mappings, under some fixed bijection between P ar and V ar. Hence we conclude the following.

Theorem 8 There are faithful translations from Λ to Λ_{AL} and vice versa.

It is clear that we can define unary abstraction and application in Λ_{AL} in terms of a designated role used solely for that purpose. By the above theorem we see that the same can be done in Λ as well. The SAC thus contains the unary λ-calculus. In particular, α-equivalence for λ-terms becomes an instance of Theorem 5.3 above.

Corollary 9 λ can be embedded into Λ.

2.4 Structured Objects and Systems of Equations

Using some encoding of standard abstraction, which exists for Λ by the previous corollary, we define the following predication operation:

⟨⟨t; (x_{i}.t_{i})_{i∈I}⟩⟩ =_{df} λx. (x(t) (x_{i}.t_{i})_{i∈I}).

Theorem 10 ⟨⟨t; (x_{i}.t_{i})_{i∈I}⟩⟩ = ⟨⟨t′; (x_{i}.t′_{i})_{i∈I}⟩⟩ → t = t′ ∧ ⋀_{i∈I} t_{i} = t′_{i}.

We thus have structured objects and operations of abstraction and application in place that appear to satisfy much of the needs of current Situation Theory. A further demand is to have non well-founded objects, obtained from cyclic sets of equations. To solve systems of equations^{5} (x_{i} = t_{i})_{i∈I} we need to encode assignments by some kind of terms. We could use predication for this, but it is still simpler to define ≪x_{i}.t_{i} ≫_{i∈I}=_{df} λx.x(x_{i}.t_{i})_{i∈I} and π_{z} =_{df} λx.x({z}z). Notice that

π_{x_{i}}(≪x_{j}.t_{j} ≫_{j∈J}) = t_{i} for i ∈ J.

We say that an assignment ā solves a system of equations (x_{i} = t_{i})_{i∈I} iff π_{x_{i}}(ā) = [π_{x_{j}}(ā)/x_{j}]_{j∈I}t_{i} for i ∈ I.

5We need to assume that at least three variables do not occur in such a system, to allow us to form the terms below without accidentally binding some of the x_{i} inside them.

Theorem 11 Every system of equations has a solution.

Proof: Recall that Υ =_{df} λf. (λx.f(xx))(λx.f(xx)) is a fixed point combinator with t(Υt) = (Υt) for any term t. Define from a system of equations (x_{i} = t_{i})_{i∈I} the functor F =_{df} λz. ≪x_{i}.[π_{x_{j}}(z)/x_{j}]_{j∈I}t_{i} ≫_{i∈I}. Then (ΥF) solves the system, as π_{x_{i}}(ΥF) = π_{x_{i}}(F (ΥF)) = π_{x_{i}} ≪ x_{i}.[π_{x_{j}}(ΥF)/x_{j}]_{j∈I}t_{i} ≫_{i∈I} = [π_{x_{j}}(ΥF)/x_{j}]_{j∈I}t_{i}. □

As things stand we do not necessarily have unique solutions to such equations. It may be consistent to assume uniqueness at least for some kinds of systems, in the spirit of [Aczel & Lunnon 1991].

2.5 Equations for Λ_{AL}

The complications in clause three of the translation from Λ_{AL} to Λ indicate why a complete and reasonably simple set of equations for Λ will be hard to find. The slightly more complex language Λ_{AL} seems more suitable for this task. So I give a set of equations for it that I hope to be complete if used in conjunction with rules for congruence relations. The notions of free parameters and substitution are assumed to be defined in the standard way.

Theorem 12 1. ⊧ t(x_{i}.t_{i}, x_{j}.#)_{i∈I,j∈J} = t(x_{i}.t_{i})_{i∈I}; 2. ⊧ λχ.t = λξ.t for ξ = χ|_{F P (t)};

3. ⊧ λ⟨X_{i} ↦x_{i}⟩_{i∈I}t = λ⟨Y_{i} ↦x_{i}⟩_{i∈I}[Y_{i}/X_{i}]_{i∈I}t for fresh Y_{i}’s;

4. ⊧ λ⟨X_{i} ↦x_{i}⟩_{i∈I}t (x_{j}.t_{j})_{j∈J} = [t_{j}/X_{j}, #/X_{i}]_{j∈J′,i∈I′}t with J′ = J ∩ I and I′ = I \ J;

5. ⊧ λ⟨X_{i} ↦x_{i}⟩_{i∈I}t [x_{j}.t_{j}]_{j∈J} = [t_{j}/X_{j}]_{j∈J′}λ⟨X_{i} ↦x_{i}⟩_{i∈I′}t with J′ = J ∩ I and I′ = I \ J;

6. ⊧ t[x_{i}.t_{i}]_{i∈I}[y_{j}.s_{j}]_{j∈J} = t[x_{i}.t_{i}, y_{j}.s_{j}]_{i∈I,j∈J′} where J′ = J \ {j | ∃i y_{j} = x_{i}};

7. ⊧ t[x_{i}.t_{i}]_{i∈I}(y_{j}.s_{j})_{j∈J} = t(x_{i}.t_{i}, y_{j}.s_{j})_{i∈I,j∈J′} where J′ = J \ {j | ∃i y_{j} = x_{i}}.

3 Dynamic Montague Grammar

I now show how the SAC can provide a framework for specifying semantic theories, especially recent ones, which do not easily fit into the traditional λ-calculus. The basic idea for semantics as conceived of in this paper is to think of properties as functions from assignments to propositions.^{6} I will use the term ω-properties to distinguish them from ordinary functions which take entities into propositions. Equipped with this notion we can reconstruct DMG along the lines of [Chierchia 1992].

6Propositions can be very fine grained—there is no need to think of propositions as sets of possible worlds or situations. Even so, Bealer’s fondalee/rajneesh puzzle, see [Bealer 1989], suggests that propositional functions cannot cope with all problems of intensional grain, or at least that function application should be distinguished from a structure preserving predication operation, as was done in 2.4.

3.1 Using the SAC for DMG

For DMG, variables need to come in two kinds: the discourse markers DM, and the remaining ones, which I call meta variables MV. I use greek letters α, β … for meta variables, dotted letters ẋ, ẏ … for discourse markers, and x, y … for variables that can be of either kind. The sorting of our variables is not a matter of the kinds of denotation that they take. It is rather a matter of protecting some of them, namely the meta variables, from the influence of abstraction so that we can bind variables inside the scope of ^{⊓}.

The crucial point of DMG can now be captured easily by abstracting and applying to the infinite set of discourse markers via the following definitions:

• ^{⊓}t =_{df} λDM.t, and

• ^{⊔}t =_{df} t(ẋ.ẋ)_{ẋ∈DM}.

All other abstractions and applications will be the traditional unary ones. Notice that every discourse marker is bound in a term of the form ^{⊓}t, and occurs free in ^{⊔}t. We thus can β-convert a term λα.t (^{⊓}t′) even if some discourse markers of t′ end up in the scope of an abstraction in t. Discourse markers are not free in ^{⊓}t′ and hence do not become bound by a new operator inside t. Another reduction we use in DMG beside the more standard β-conversions is ^{⊔} ^{⊓}t = t.

The sentence ‘A man walks in’ can now be rendered in our notation as

λα.Σẋ(man(ẋ) ∩ walkin(ẋ) ∩ ^{⊔}α)

which can applied to ^{⊓}whistle(ẋ) (‘he whistles’) to yield

Σẋ(man(ẋ) ∩ walkin(ẋ) ∩ whistle(ẋ))

The important action happens at the level of conjunction of ω-properties, which is achieved by abstracting over “possible continuations” of the discourse.^{7}

We use unary abstraction and application in the system in order to get a fairly standard logic that does not require us to rethink the setup of DMG. We saw that these notions can be defined within the confines of Λ.^{8} Logical operations are treated as unary or binary constants whose semantic behavior is captured by our theories of truth, which we choose to give separate from the general model theory in an axiomatic way. The following logical constants are singled out: ∩, ∪, −, ⊃, Σ, Π, ≐, intended to be the operations of conjunction, disjunction, negation, implication, existential and universal quantification, and equality. I will take ∩, −, Σ, ≐ as primitive, and the others to be defined in the standard way.^{9} Logical combinators are written in the conventional form, t ∩ t′ for ∩(t)(t′), Σx t for Σ(λx.t) etc., to enhance readability.

7Lambda conversion on ^{⊓}whistle(ẋ) is only one way to make the conjunction happen; Unification of whistle(ẋ) with the free variable α, as in UCG, is just as intuitive for this. Hence the choice of the term ‘meta variables’, reminiscent of its use in [Zeevat 1991].

8As an alternative to taking these unary operations as defined in terms of Λ-expressions, one could introduce them as basic operations, and give them a semantics in an expanded domain D ⇀ ↽_{Φ}^{Ψ} ((Var → D) → D) + (D → D), in the way [Chierchia 1992] does.

9There may be reasons not to do this, such as to avoid unintended identities in attitude contexts, or to be able to use the less symmetric notion of implication of [Aczel 1980].

3.2 Frege Structure Axioms

For semantics, we need a theory of truth for the propositions that we hope to denote by the Λ-terms. To that end, we introduce a formal language in which to state such a theory. One might do the job in an informal model theoretic way along the lines of [Aczel 1980] but I will make things look more like the formal treatment of [Turner 1990].

Definition 8 We define WFFs of F OL_{Λ} in the standard way:

• if t, t′ ∈ T ERM then T (t), t = t′ ∈ W F F,

• if ψ, ϕ ∈ W F F then ¬ϕ, ϕ ∧ ψ, ∃αϕ ∈ W F F.

The interpretation of WFFs proceeds in the standard way. T is a truth predicate. We define F (t) =_{df} T (−t) (falsity), P (t) =_{df} T (t) ∨ F (t) (being a proposition), and P T Y^{n}(t) =_{df} ∀x_{1} … x_{n} (⋀_{i=1..n} x_{i} ≠ #) → P (t(x_{1}) … (x_{n})) (being an n-place property). Here are the basic axioms:

P (t ≐ t′) ∧ T (t ≐ t′) ↔ t = t′
P (t) →  P (−t) ∧ T (−t) ↔ ¬T (t)
P (t) ∧ P (t′) → P (t ∩ t′) ∧ T (t ∩ t′) ↔ T (t) ∧ T (t′)
P T Y^{1}(t) →  P (Σ t) ∧ T (Σt) ↔ ∃z T (t(z))

3.3 Some DMG Translations

We can only give a short sketch here and refer the reader to [Chierchia 1992] and [Chierchia 1992b] for a more complete treatment. Sentence denotations in DMG are not propositions, but context change potentials (ccp’s), where a ccp is a function from ω-properties to propositions. Two operations are handy to convert props into ccp’s and back: ↑ t =_{df} λα(t ∩ ^{⊔}α) and ↓ t =_{df} t(^{⊓}true). Ccp’s allow for clever ways of leaving holes within quantified structures to be filled by later material in the discourse so that one can use functional composition t; t′ =_{df} λα.t(^{⊓}(t′(α))) for discourse sequencing:

‘ẋ[a]’ ⟹

λαλβ λγΣẋ(^{⊔}α ẋ)^{⊓}(^{⊔}β (ẋ)(γ))

‘ẋ[a man] walks in. ẋ[he] whistles.’⟹

[λγΣẋ(man(ẋ) ∩ walkin(ẋ) ∩ ^{⊔}γ)] ; [λγ. whistle(ẋ) ∩ ^{⊔}γ]

= λγ(Σẋ man(ẋ) ∩ walkin(ẋ) ∩ whistle(ẋ) ∩ ^{⊔}γ)

The flexibility of ccp’s is shown by various possibilities to define dynamic kinds of universal quantification for donkey sentences:

‘every’ ⟹

λαλβ ↑Πẋ − [(^{⊔}α ẋ)(^{⊓}− ↓(^{⊔}β ẋ))] ‘man with ẏ[a donkey]’ ⟹ λẋ λγ(man(ẋ) ∩ Σẏ(donkey(ẏ) ∩ with(ẋ, ẏ) ∩ ^{⊔}γ))

‘beats ẏ[it]’ ⟹ λẋ ↑beat(ẋ, ẏ)

By intensional function application t(^{⊓}t′) on the translations one gets:

↑Πẋ − [man(ẋ) ∩ Σẏ(donkey(ẏ) ∩ with(ẋ, ẏ) ∩ −(beat(ẋ, ẏ) ∩ true))]

An alternative to the above “strong” reading of the universal, would assign the translation:

‘every’ ⟹ λαλβ ↑Πẋ[− ↓(^{⊔}α ẋ) ∪ (^{⊔}α ẋ)(^{⊓} ↓(^{⊔}β ẋ))]

resulting in the “weak” reading:

↑Πẋ[−(man(ẋ) ∩ Σẏ(donkey(ẏ) ∩ with(ẋ, ẏ) ∩ true)) ∪(man(ẋ) ∩ Σẏ(donkey(ẏ) ∩ with(ẋ, ẏ) ∩ beat(ẋ, ẏ) ∩ true))]

4 Discourse Representation Theory

The SAC mirrors very closely the use of discourse referents in DRSs. The similarity with Zeevat’s semantics for those, in terms of pairs consisting of a set of variables and a function from assignments to truth, is undeniable, see [Zeevat 1991]. We have put propositions in the place of truth values and defined an abstraction operation that takes such pairs into appropriate new functions. In addition, we can iterate such abstractions indefinitely and we have a simple notion of application at our disposal.

Our approach is most closely related to Cooper’s Situation Theoretic DRT, see [Cooper 1993], who uses EKN with Aczel–Lunnon abstraction to similar effect. As in Cooper’s treatment our version of DRT imposes a need for some additional abstractions at the right level. I won’t go into the resulting complications for the syntax–semantics interface here.

4.1 ω-Properties

To be a propositional function in the argument roles x_{1} … x_{n} is defined by:^{10}

P F^{x_{1}..x_{n}}(t) =_{df} ∀z_{1}..z_{n} ⋀_{i=1..n}z_{i} ≠ # → P (t(x_{1}.z_{1}, …, x_{n}.z_{n})).

10We will use an infinitary version of F OL_{Λ} to express the theory, though one might get away with axiom shemata in the finitary logic if we stick to finite n here. In particular the definition of P T Y^{M}(t)

below would have to be replaced by an infinite number of implicational axioms.

This is not a sufficiently strict notion of ω-properties to support the forthcoming definitions and theorems. How strict a notion of ω-property one ultimately wants remains to be seen, but a function f that for example maps an assignment ⟨x ↦ d⟩ to the proposition p while mapping ⟨x′ ↦ d′⟩ to −p seems useless for semantics. We exclude such pathological cases by requiring something to the effect that

P T Y^{M}(d) ⇒ ∀N P F^{N}(d) ↔ M ⊆ N.

A too strict definition would have = instead of ⊆. This would exclude any abstracts from denoting ω-properties, because they are insensitive to overdefined assignments:

Λ ⊧ {x_{1}..x_{n}}t (x_{1}.t_{1}, .., x_{n}.t_{n}) = {x_{1}..x_{n}}t (x_{1}.t_{1}, .., x_{n+m}.t_{n+m})

Still one may ask whether the application of a ω-property to an assignment should ever result in something other than a proposition or ⊥. The only sensible possibility seems to be to have application to “underdefined” assignments result in a new ωproperty whose argument roles are those that haven’t been filled on the first attempt. We have introduced the operation of partial application for these purposes, which will also enable us to define the duplex conditions of modern DRT. So for now I stick to the view that (full) application of ω-properties to assignments, if yielding a definite result at all, always yields a proposition.

Definition 9 P T Y^{{x_{i}|i∈I}}(t) =_{df} ⋀_{I⊆J} P F^{{x_{i}|i∈J}}(t) ∧ ⋀_{I⊈J} ∀^{i∈J}z_{i} t(x_{i}.z_{i})_{i∈J} = #.

4.2 Kamp Structures

Let us now try to give a theory of ω-properties and propositions and truth that is capable of dealing with basic ideas of DRT. We add to the logical operations ∩, −, ≐ two new quantificational operators, namely a non selective existential Ξ and a binary conditional ≫. All these are required to be (bi)strict: yielding ⊥ whenever one of their arguments is ⊥. Here are the axioms for Kamp structures:

P (t ≐ t′) ∧ T (t ≐ t′) ↔ t = t′
P (t) →  P (−t) ∧ T (−t) ↔ ¬T (t)
P (t) ∧ P (t′) → P (t ∩ t′) ∧ T (t ∩ t′) ↔ T (t) ∧ T (t′)
P T Y^{x_{1}..x_{n}}(t) →  P (Ξ t) ∧ T (Ξt) ↔ ∃z_{1}..z_{n} T (t(x_{1}.z_{1}, .., x_{n}.z_{n}))

\begin{matrix}P T Y^{\{x_{i}|i∈I\}}(t) ∧ P T Y^{\{x_{j}|j∈J\}}(s) → P (t ≫ s) ∧ \\ T (t ≫ s) ↔ ∀^{i∈I}z_{i} T ( t (x_{i}.z_{i})_{i∈I} ) → ∃z_{j}^{j∈J\I} T ( s (x_{i}.z_{i}, x_{j}.z_{j})_{i∈J∩I,j∈J\I} ) \end{matrix}

Notice that only bound variables in s are quantified in the conditional. To get some kind of “dynamic conjunction” of DRSs we can introduce the operation ⊕ into the system.^{11} For example by means of this definition:

11This operation is used in [Cooper 1993] for the interpretation of discourse. It becomes definable in a slightly richer language that employs variables over assignments.

∥t ⊕ t′∥^{g} =_{df} Φ λf Ψ∥t∥^{g} (f) ∩ Ψ∥t′∥^{g} (f)

The following consequences can now be derived:

Theorem 13 1. P T Y^{X}(t) ∧ P T Y^{Y} (t′) → P T Y^{X∪Y} (t ⊕ t′);

2. ⊧ t ⊕ t′ (x_{1}.t_{1}, .., x_{n}.t_{n}) = t(x_{1}.t_{1}, .., x_{n}.t_{n}) ∩ t′(x_{1}.t_{1}, .., x_{n}.t_{n})

3. ⊧ λM.t ⊕ λN.s = λM ∪N . t ∩ s, if M ∩ F V (λN.s) = N ∩ F V (λM.t) = ∅.

Using partial application we can define DRT-type quantifiers Q_{x} for the so called “duplex conditions,” by means of standard generalized quantifiers Q as relations between ω-properties. The weak and strong readings are obtained as follows:

t⟨Q_{x}⟩^{w}t′ =_{df} Q(λz.Ξ t[x.z] , λz.Ξ t ⊕ t′[x.z]),
t⟨Q_{x}⟩^{s}t′ =_{df} Q(λz.Ξ t[x.z] , λz. t[x.z] ≫ t′[x.z]).

4.3 True Dynamics

It is now time to ask what the relation is between the SAC and systems like the Dynamic Predicate Logic (DPL) of [Groenendijk & Stokhof 1991], that are based on relational interpretations. DPL replaces the non-standard DRT syntax by FOL formulas, but they have shown how to give the relational interpretation for DRSs too. Let us view relations between assignments as functions from assignments to sets of assignments. Call sets of assignments ω-sets, and take conditions to denote just ω-sets. We then get the following denotation for a DRS:

∥{x_{1}...x_{n}}ϕ∥_{DP L}^{g} = {h | g ∼^{{x_{1}..x_{n}}} h ∧ h ∈ ∥ϕ∥}.

This should be compared with extensionalized SAC denotations, which we obtain when we replace propositions by truth values. We then also get ω-sets as denotations under an assignment, but they are different from the DPL ones:

∥{x_{1}...x_{n}}ϕ∥_{SAC}^{g} = {h | g_{h}^{{x_{1}..x_{n}}} ∈ ∥ϕ∥}.

The point is that the h’s in our set can assign anything they like to the variables outside {x_{1}...x_{n}}, while for the DPL style of denotation they have to agree with the incoming g.

A natural development, carried further in [Dekker 1993], is to view “information states” as such ω-sets, and then lift denotations of DRSs to functions from ω-sets to ω-sets, such as:

∥ϕ∥_{DP L↑}(G) = ⋃_{g∈G} ∥ϕ∥_{DP L}^{g}

which is quite different from the trivial lifting from ϕ to λp.(p ⊕ ϕ) that might be used in our system.

The lack of a requirement for assignments to agree on certain variables has consequences for semantics. Thus, in contrast to DPL and most forms of DRT, we must abstract over variables in order to link them anaphorically to preceding discourse by ⊕. If we would use DPL style composition for discourse conjunction instead the link could not be sustained over more than two sentences. A similar divergence can be found in the treatment of the conditional. Again we have to put anaphoric variables into to abstracted set of the consequence, but only those which are anaphoric to the antecedent, not those which refer further back. Abstraction in Λ really is just a way of partitioning roles into different levels, in view of how we want to fill them or quantify over them.

There is something of a philosophical gap between the approach of this paper and the “truly dynamic” ones, which is brought out by these considerations. On the SAC view the functions from assignments to ω-properties are not regarded as ways of “updating” information states by incoming material. It makes no sense on this view to talk of “input” and “output” in reference to the assignments. The guiding intuition is rather that semantic objects should be plausible as things to have attitudes towards. These objects, I take it, are rather static creatures whose role in the changes of mental states are another matter.

5 Conclusion

We have defined a calculus of simultaneous abstraction and shown it to be equivalent to a less simple minded one that is more reminiscent of Aczel and Lunnon’s system. We established the existence of structured, and non well-founded objects in the system, by an embedding of the lambda calculus in it. We then obtained versions of Dynamic Montague Grammar and Discourse Representation Theory, using axiomatic theories of truth. It seems plausible that the same can be done for Situation Theory as well, supporting the claim that we have found a framework which is general enough for a wide range of semantic theories which take notions of propositions and truth as fundamental for the enterprise. It is at odds though with forms of “dynamic” semantics that take the idea of updating (sets of) assignments as their starting point. Many important logical questions remained unanswered in this paper, but I hope to have shown that they may be worth asking.

References

[Aczel 1980] P. Aczel: Frege Structures and the Notions of Proposition, Truth and Set. In Barwise et al. (ed.) The Kleene Symposion, North Holland Studies in Logic 1980.

[Aczel & Lunnon 1991] P. Aczel and R. Lunnon: Universes and Parameters. In Barwise et al. (ed.) Situation Theory and its Applications, Vol. 2. CSLI, Stanford 1991.

[Barendregt 1984] H.P. Barendregt: The Lambda Calculus. Its Syntax and Semantics. Revised edition, North-Holland, Amsterdam 1984.

[Barwise & Cooper 1991] J. Barwise and R. Cooper: Simple Situation Theory and its Graphical Representation. In Jerry Seligman (ed.) Partial and Dynamic Semantics 3, DYANA deliverable R2.1.C, Centre for Cognitive Science, Edinburgh, 1991.

[Bealer 1989] G. Bealer: On the Identification of Properties and Propositional Functions. In Linguistics & Philosophy 12, 1-14, Kluwer, 1989.

[Chierchia 1992] G. Chierchia: Intensionality and Context Change. Towards a Dynamic Theory of Propositions and Properties. Manuscript 1992. To appear in the Journal of Logic, Language and Information.

[Chierchia 1992b] G. Chierchia: Anaphora and Dynamic Binding. In Linguistics & Philosophy 15/2 1992.

[Cooper 1993] R. Cooper: Towards a General Semantic Framework. In R. Cooper (ed.): Integrating Semantic Theories. DYANA-II deliverable R2.1.A, Centre for Cognitive Science, Edinburgh 1993.

[Dekker 1993] P. Dekker: Transsentential Meditations. Ups and downs in dynamic semantics. ILLC dissertation, Amsterdam 1993.

[Groenendijk & Stokhof 1990] J. Groenendijk and M. Stokhof: Dynamic Montague Grammar. Technical Report, ITLI Amsterdam.

[Groenendijk & Stokhof 1991] J. Groenendijk and M. Stokhof: Dynamic Predicate Logic. In Linguistics & Philosophy 14, 1991.

[Kamp 1981] H. Kamp: A Theory of Truth and Semantic Representation. In J. Groenendijk et al. (eds.) Formal Methods in the Study of Language. Mathematical Centre, Amsterdam 1981.

[Turner 1990] R. Turner: Truth and Modality for Knowledge Representation. Pitman, London 1990.

[Zeevat 1990] H. Zeevat: Static Semantics. In J. van Benthem (ed.): Partial and Dynamic Semantics I, DYANA deliverable, Centre for Cognitive Science, Edinburgh 1991.

[Zeevat 1991] H. Zeevat: Aspects of Discourse Semantics and Unification Grammar. Ph.D. Thesis, Amsterdam 1991.