What is a DRS?

Tim Fernando^{∗}

                       fernando@ims.uni-stuttgart.de

August 1994

Abstract

Discourse representation structures (DRSs) are characterized by the transitions they induce on states. Just as first-order logic can be presented either model-theoretically or proof-theoretically, DRS transitions can be described in either semantic or syntactic terms. A semantic conception of states formed from firstorder models and variable assignments (or so-called embeddings) is related (through a determinization of the transitions and the notion of a bisimulation) to a syntactic conception of states given by the DRSs themselves.

1 Introduction

The notion of a discourse representation structure (DRS) was introduced in Kamp [11] to analyze anaphora (in a manner similar to Heim [8]). Unimpressed by this “extra level of explicit syntactic representations”, Barwise [1] eliminated DRSs from the analysis, arguing that what is essential is to

view the utterance of an expression more dynamically, as having an effect on the environment shared by speaker and hearer, the effect being represented by various sorts of changes in variable assignments. (p. 2)

Focussing on the first-order fragment of Barwise [1], Groenendijk and Stokhof [6] kept DRSs out by bringing in programs from (quantified) dynamic logic (e.g., Harel [7]). In the meantime, various formal accounts of natural language semantic phenomena have been encoded in DRSs, going well beyond Kamp [11], Barwise [1] or Groenendijk and Stokhof [6]. Many of these developments are reported in the textbook Kamp and Reyle [10], a glance through which may well suggest (to the reader) that DRSs are here to stay. Or, at the very least, before DRSs are expelled from formal semantics, they deserve a hearing. Indeed, the converse can be argued to hold as well: a reply to the question “what is a DRS?” ought to spell out an interpretation [[K]] of a DRS K that does not refer circularly to the concept of a DRS. For example, equating [[K]] with the (term model) object {K′ | K ≡ K′} (built from DRSs) merely shoves the problem over to providing a semantic basis for the logic behind the equivalence ≡. Saying that a DRS K is a piece of syntax (expressing some notion that can perhaps be captured by Heim [8]’s files) begs the question, what does that piece of syntax denote?

Now, under so-called dynamic semantics, a syntactic entity φ is interpreted as a binary relation [[φ]] on a set of “states”, specifying the change induced by φ

s[[φ]]s′ iff on input s, φ can output s′ .  (1)

The first two sections of the present paper concentrate on an interpretation P of DRSs K as input/output relations P (K). To explain how a DRS effects the changes associated with it — i.e., to say what the word “can” in (1) means —, section 3 transforms the interpretation P to a deterministic form in which DRSs may also be viewed as states. This dual nature of DRSs (as, on the one hand, input/output relations, and as, on the other hand, inputs or outputs) is employed to give non-representational views of the kind expressed above by Barwise computational content. In particular, the operationalizability of what Groenendijk and Stokhof [6] somewhat loosely call programs (“computing” the desired input/output relations) is described by appealing to “an extra level of explicit syntactic representations” — a move that is, with hindsight, hardly surprising, given that computation requires (syntactic) coding.

∗My thanks to Hans Kamp, to Robin Cooper, to the participants of a seminar in Stuttgart (Steve Berman, Ed Keenan, and Robert van Rooy), to Emiel Krahmer and to Josef van Genabith for helpful discussions.

1.1 Related work

The present paper was prompted by Cooper [2], which considers DRSs as abstracts, with the emphasis, as in Barwise [1], on the role played by variable assignments. Without denying the validity of such a view (although stressing also the importance for that view of the first-order models that structure the ranges of the variable assignments), an alternative conception of DRSs as abstracts is developed below that mentions neither variable assignments nor first-order models but only DRSs. That conception is somewhat syntactic, in contrast to Zeevat [18], where a DRS (U, C) (consisting of a set U of variables or discourse markers, and a set C of conditions) is interpreted semantically as (U, F), with F the set of verifying embeddings of C, or to Muskens [14], where DRSs are interpreted as input/output relations (which are encoded in a type theory). The states over which the inputs and outputs vary are taken there to be total functions — i.e., functions defined on all variables from which DRSs are built. In this respect, the account is not faithful to DRT, and, indeed, Muskens [14] concedes that “I leave a partialization of the theory presented in this paper for future research” (p. 469).

1.2 Summary of the present work

Beyond providing a partialization (left open in Muskens [14]) of the relational interpretation of DRSs, the present paper develops a dual interpretation of DRSs as states, in order to understand DRSs as programs (a basic challenge for which is to make sense computationally of the interpretation of negation as the complement of the halting problem). The key is to determinize the interpretation P (K) ⊆ S × S of a DRS K along the lines of the classic “subset construction” that turns a non-deterministic finite automaton into a deterministic one accepting the same language (e.g. Hopcroft and Ullman [9]). Rather than constructing (determinized) transitions from arbitrary subsets of S, it is sufficient to consider sets θ ⊆ S generated by a fixed set θ_{0} ⊆ S of “initial” states. These states θ are named by DRSs K, according to the transitions induced by K from θ_{0}. More precisely, for every accessible set θ, there is a DRS K that names θ inasmuch as P^{0}(K) = θ, where^{1}

P^{0}(K) := {s ∈ S | (∃s_{0} ∈ θ_{0}) s_{0} P (K) s} .

The determinized transitions can then be presented syntactically as

K →^{K′} K′′ iff K′′ = K^{∩}K′

where the merge, K^{∩}K′, of two DRSs is defined to combine discourse markers and conditions respectively,

(U, C)^{∩}(U′, C′) = (U ∪ U′, C ∪ C′) modulo renaming of variables in C (to avoid capture) .

The match-up with the determinization of P can be made precise in terms of the notion of bisimulation equivalence (Park [16]) between states that arise from the possibility (as opposed to the impossibility) of P -transitions. In particular, two DRSs K and K′ are bisimulation equivalent iff P^{0}(K) = P^{0}(K′) (Theorem 10), which is denoted K ≡_{0} K′. The merge K^{∩}K′ can be interpreted incrementally under P as the relational composition P (K̂) ∘ P (K′), for an appropriate K̂ that is ≡_{0}-equivalent to K (Proposition 2).

A certain set of (quantifier-free) formulas φ called updates is isolated such that for every DRS K, there is an update φ that induces a DRS K_{φ} that is ≡_{0}-equivalent to K (Update lemma). A slightly altered definition of a DRS is discussed briefly that avoids complications arising from variable clashes, and yields updates φ that not only support the Update Lemma, but also enjoy the property that P (K_{φ}) can be determined from either P^{0}(K_{φ}) or its fixed points (i.e., verifying embeddings). This property provides a pleasing bridge between static (fixed point) semantics and dynamic (relational) semantics, overcoming the apparent discrepancy in complexity between the meaning of a formula being a binary relation on S (i.e., the state transitions induced by the formula) and the meaning being simply a subset of the set S of states (i.e., the states supporting the formula).

1Throughout the present paper, the notation := will be used for definitional equality, ::== for a Backus-Naur-Form/rewrite/grammar arrow (to alternatives separated by |), and = for ordinary equality.

The present work is confined to the first-order DRSs in Kamp and Reyle [10]. The first-order character of these DRSs is exposed relative to the measure P^{0} by a characterization lemma associating first-order formulas with DRSs (Lemma 1) and DRSs with first-order formulas (Lemma 3). A brief argument is presented in the concluding section suggesting that first-order DRSs capture the “logical core” of DRT, although a careful analysis of the matter will have to be taken up elsewhere.

2 First-order DRSs

Fix a signature L (with equality) and an infinite set X of variables. First-order discourse representation structures (DRSs) K and first-order conditions γ are generated simultaneously from finite subsets U of X, and atomic L-formulas A with variables from X according to

K ::== (U, ∅) | K^{∩}γ
γ ::== A | ¬K .

A DRS K and a (first-order) condition γ are interpreted relative to an L-model M by P_{M}(K) ⊆ S_{M} × S_{M} and v_{M}(γ) ⊆ S_{M} respectively, where S_{M} is the set of M-assignments, or (following Kamp [11]) “embeddings”

— i.e., partial functions f from X to the universe of M. The semantic clauses corresponding to the syntactic clauses above are

P_{M}(U, ∅) := {(f, g) ∈ S_{M} × S_{M} | f ⊆ g and dom(g) = dom(f) ∪ U}
v_{M}(A) := {f ∈ S_{M} | M ⊧ A[f]}
P_{M}(K^{∩}γ) := {(f, g) ∈ S_{M} × S_{M} | f P_{M}(K) g and g ∈ v_{M}(γ)}
v_{M}(¬K) := {f ∈ S_{M} | there is no g such that f P_{M}(K) g}
(= S_{M} − dom(P (K))) .

The overall interpretations are the disjoint sums

P (K) := {((M, f), (M, g)) | M ∈ M̂ and f P_{M}(K) g}
v(γ) := {(M, f) | M ∈ M̂ and f ∈ v_{M}(γ)}

over the class M̂ of all L-models. (The reader worried that M̂ is a proper class can replace it by a sufficiently large set of L-models — e.g., models, by Löwenheim-Skolem, with objects drawn from max(|L|, ℵ_{0}).)

2.1 DRS normal form

A DRS K can be flattened into a pair (U, C) of finite sets U of variables and C of conditions, by setting

(U, C)^{∩}γ := (U, C ∪ {γ}) ,

from which it then follows that

P_{M}(U, C) = {(f, g) ∈ S_{M} × S_{M} | f P_{M}(U, ∅) g and (∀γ ∈ C) g ∈ v_{M}(γ)} .

As relations, DRSs have the normal form

P (U, C) = P (U, ∅) ∘ P (∅, C) ,

where the second relation,

P (∅, C) = {(s, s) | (∀γ ∈ C) s ∈ v(γ)} ,

is independent of U, in contrast to the set of fixed points

V (U, C) := {(s, s) | s P (U, C) s} ,

relative to which P (U, C) can also be characterized as P (U, ∅) ∘ V (U, C). In either case, P (U, C) cannot be determined from the second relation (viz., P (∅, C) or V (U, C)), as can be seen by considering the pair of DRSs ({x}, {x = x}) and (∅, {x = x}). Elements of the set V (K) are precisely the verifying embeddings of K in Kamp and Reyle [10]. The truth of K at a model M is equated there with the assertion ∅ ∈ dom(P_{M}(K)), which (as the same pair of DRSs above shows) cannot be determined from the fixed points (i.e., verification set) of K alone. The complication, however, would seem to be easy enough to overcome, arising only because the set U in a DRS K = (U, C) is independent from the set of discourse markers referred to in C. This matter is pursued in section 3, but first, let us consider another subset of S that is naturally associated with K.

2.2 The moment of a DRS

Concentrating on transitions from the empty (i.e., nowhere defined) embedding ∅, define the moment of a DRS K to be

P^{0}(K) := {(M, f) | ∅ P_{M}(K) f} .

Given a DRS K = (U, C), call a first-order formula χ a characteristic formula of K if the set of variables occurring freely in χ is U, and

P^{0}(K) = {(M, f) | dom(f) = U and M ⊧ χ[f]} .

Lemma 1 (Characterization lemma, Part 1). Every DRS has a characteristic formula.

Proof. An inductive argument is facilitated by strengthening the assertion as follows

for every DRS (U, C) and every finite set U_{0} of variables, there is a first-order formula χ such that for all M, f : U_{0} → |M|, and g,

f P_{M}(U, C) g iff f P_{M}(U, ∅) g and M ⊧ χ[g] .

The cases (U, ∅) and K^{∩}A are trivial. As for (U, C)^{∩}¬K, appeal to the inductive hypothesis, as strengthened above, to form a conjunction of formulas, the second of which is (ignoring pesky subscripts for variables) ¬∃\overline{x} χ_{K}, where \overline{x} is a list of variables declared in K but which are not (already) in U ∪ U_{0}. ⊣

The restriction to transitions from the empty embedding ∅ cannot simply be dropped, in view of the existence of DRSs K such that for every first-order L-formula χ and every finite set U of variables, there is an L-model M satisfying

P_{M}(K) ≠ {(f, g) | f P_{M}(U, ∅) g and M ⊧ χ[g]} .

A trivial example is provided by the DRS (∅, {x = x}), although more interesting examples can be drawn from a certain special family of DRSs (to which (∅, {x = x}) does not belong), specified in the next section. On the positive side, the converse to Lemma 1 will also be established there, with K chosen from that family.

3 DRSs as updates

The present section isolates a certain family of DRSs given by quantifier-free first-order formulas that includes ≡_{0}-representatives of all DRSs. As a first approximation, consider the set of quantifier-free formulas φ obtained by closing atomic formulas A under negation and conjunction

φ ::== A | ¬φ | φ&ψ ,

inducing DRSs K_{φ} according to

K_{A} := (VAR(A), {A})
K_{¬φ} := (∅, {¬K_{φ}})
K_{φ&ψ} := K_{φ} • K_{ψ} ,

where VAR(A) is the set of variables occurring in A, and the operation • combines discourse markers and conditions respectively,

(U, C) • (U′, C′) := (U ∪ U′, C ∪ C′) .

A sequential incremental interpretation of DRSs suggests that P (K • K′) be the relational composition P (K) ∘ P (K′). But how does P (K) ∘ P (K′) square with the normal form of P (K • K′), which requires all variables initializations to precede all tests of conditions? Irreconcilable differences may lurk, but only if some variable in (a condition in) K left uninitialized by P (K) is initialized by P (K′). (For example, consider P (∅, {x = x}) ∘ P ({x}, ∅).) Accordingly, define

(U, C)^{∩}(U′, C′) := (U ∪ U′, C[U, U′] ∪ C′)

where C[U, U′] is the set C of conditions with variables in U′ −U renamed to be disjoint from U ∪U′ (so as to avoid being captured by the DRS (U′, ∅)). A definite scheme for renaming variables can be fixed according to a well-ordering on the set X of variables, but we will not worry about just what that is. Defining

K ≡_{0} K′ iff P^{0}(K) = P^{0}(K′) ,

the important point is that (U, C[U, U′]) ≡_{0} (U, C), which is to say that ^{∩} is just •, with perhaps a happier choice of ≡_{0}-equivalent DRSs.^{2} Let us record this fact as

Proposition 2. For all DRSs K and K′, there is a DRS K̂ ≡_{0} K such that P (K^{∩}K′) = P (K̂) ∘ P (K′). Furthermore, in the absence of variable clashes (i.e., in case K^{∩}K′ = K • K′), K̂ can be chosen to be K.

Now, define the set of (first-order) updates φ inductively by

φ ::== A | ¬φ | φ^{∩}ψ ,

subject to the previous associations K_{φ} of DRSs, with K_{φ^{∩}ψ} arranged to be K_{φ}^{∩}K_{ψ} either directly or by defining φ^{∩}ψ to be φ_{ψ}&ψ for the appropriate alphabetic variant φ_{ψ} of φ. In either case, let us identify φ^{∩}ψ with φ&ψ if K_{φ^{∩}ψ} = K_{φ} • K_{ψ}. Notice that if φ and ψ are updates, then so is ¬(φ&¬ψ), which can be understood (following their equivalence in classical logic) as a definition of φ ⊃ ψ. In terms of DRSs and conditions, the condition ¬(K^{∩}¬K′) can be rewritten as K ⊃ K′ so that

v(K ⊃ K′) = {s | (∀s′ s.t. s P (K) s′) s′ ∈ dom(P (K′))} .

Next, define the interpretation [[φ]] of an update φ to be P (K_{φ}). By Proposition 2, if φ^{∩}ψ is φ&ψ, then [[φ^{∩}ψ]] is equal to the relational composition [[φ]]∘[[ψ]]. Moreover, the converse to Lemma 1 can be established (as promised).

Lemma 3 (Characterization lemma, Part 2). For every first-order formula χ with set U of free variables, there is an update φ such that

P^{0}(K_{φ}) = {(M, f) | dom(f) = U and M ⊧ χ[f]} .

2For this reason, the alternative definition of (U, C)^{∩}(U′, C′) in terms of • where (U′, C′) is modified rather than C has not been adopted, as it seems more reasonable to rename variables buried inside a DRS than free variables visible in the domain of a verifying embedding.

Proof. Assume without loss of generality that a variable x cannot occur both free and bound in χ, and that it is bound (quantificationally) at most once in χ. Then build an update φ_{χ} inductively from χ according to

A ↦ A
χ&χ′ ↦ φ_{χ}^{∩}φ_{χ′}
¬χ ↦ init(U^{φ_{χ}})^{∩}¬φ_{χ}
∃x χ ↦ init(U^{φ_{χ}} − {x})^{∩}¬¬((x = x)^{∩}φ_{χ}) ,

where init(U) is the conjunction (x = x)^{∩} ⋯^{∩} (x′ = x′) over all variables x, …, x′ ∈ U, and where U^{φ} is the set of discourse markers such that K_{φ} = (U^{φ}, C) for some set C of conditions. ⊣

An immediate corollary of the characterization lemma (parts 1 and 2) is

Lemma 4 (Update lemma). For every DRS K, there is an update φ such that K ≡_{0} K_{φ}.

The update lemma can also be proved directly by an inductive argument.

3.1 An example

To illustrate the idea behind updates, let us consider (what else?) the notorious “donkey” sentence

If a farmer owns a donkey, he beats it.

A naive translation into first-order logic (based on a decomposition of the sentence into an implication between two sentences) is

(∃x)(∃y)(farmer(x) & donkey(y) & own(x, y)) ⊃ beat(x, y) ,  (2)

which corresponds (in a sense to be explained below) to the DRS (∅, {K ⊃ K′}), where^{3}

K := ({x, y}, {farmer(x), donkey(y), own(x, y)})
K′ := (∅, {beat(x, y)}) .

Observe that the DRS K′ cannot be induced by an update because the variables x and y are not declared in K′. On the other hand, the DRS (∅, {K ⊃ ({x, y}, {beat(x, y)})}) induced by the (quantifier-free) update

(farmer(x) & donkey(y) & own(x, y)) ⊃ beat(x, y)  (3)

is ≡_{0}-equivalent to (∅, {K ⊃ K′}), with which it shares the characteristic formula

(∀x)(∀y) ((farmer(x) & donkey(y) & own(x, y)) ⊃ beat(x, y)) .

(Indeed, P (∅, {K ⊃ ({x, y}, {beat(x, y)})}) = P (∅, {K ⊃ K′}).) Thus, by restricting ourselves to updates, we lose the faithful formulation of the succedent of (2) by a DRS K′ with an empty set of discourse markers, reflecting the absence of quantification in the succedent. That is to say, the difference between (2) and (3) — or, more precisely, between their corresponding DRSs — concerns explicit quantification. (The quantifierfree character of updates here is reminiscent of Pagin and Westersthl [15].) But if that bit of explicitness is so important, it is rather curious that the semantics of DRSs is defined so that even if U is non-empty, the DRS (U, ∅) cannot change an input assignment whose domain already includes U. That is, while it is tempting to record within the component set U of a DRS (U, C), the “novel” character of the indefinite “a” in “a farmer,” the fact is that even if a variable is in U, P (U, ∅) may have no effect on it.

So why not redefine the semantics of P (U, ∅) so that new values can always be assigned to all variables in U? This is one of the features of the formalism Dynamic Predicate Logic (DPL) of Groenendijk and Stokhof [6] that sets it apart from DRT.^{4} Rather than introducing DRSs and conditions, DPL translates first-order formulas into programs from (quantified) dynamic logic (e.g., Harel [7]), in which variable assignments are total functions defined on the full set X of variables. This use of total functions means that DPL programs (i.e., so-called random assignments) corresponding to P (U, ∅) must be free to overwrite values to variables in U. By contrast, information is never destroyed by a DRS in the sense that variable assignments can only be extended. Even if DPL were to abandon the requirement that variable assignments be total, the question is whether the semantics of P (U, ∅) ought to be redefined, concerning which the present author offers three arguments for the status quo.

3We concentrate here on the so-called “strong” reading, although much the same applies to the “weak” reading which is obtained by taking K to be ({x}, {farmer(x), ¬(∅, {¬({y}, {donkey(y), own(x, y)})})}), and K′ to be ({y}, {donkey(y), own(x, y), beat(x, y)}).

(i) Forcing an assignment of a value to a variable to model the utterance of an indefinite such as “a” in “a farmer” can be arranged without changing the semantics of P (U, C), but simply by a suitable choice of a variable (for the indefinite farmer) to put into the set U. So-called “novelty” and “familiarity” conditions related to this choice belong to part of the passage from natural language utterances to formulas that falls outside the scope of the analysis given by the interpretation P.

(ii) The non-destructive nature of P (U, ∅) is exploited heavily in Fernando [5] to define a Boolean-valued notion of truth for a relational interpretation that extends DRT updates conservatively with witness constructs ϵx : φ for explicit existential quantification ∃x φ. In addition to the update (3), that interpretation supports a translation of the donkey sentence as

(∃x)(∃y)(farmer(x) & own(x, y) & donkey(y)) ⊃ beat(ϵx:∃yφ, ϵy:ψ) ,

where φ is farmer(x) & own(x, y) & donkey(y), and ψ is φ with x replaced by ϵx: ∃yφ. The formula φ in an ϵ-term ϵx:φ can be understood situation-theoretically (e.g., Cooper [2]) as a restriction on the parameter x.

(iii) A final point that the present author owes to a remark by C. Gardent is that the initialization effects of updates (from the clause K_{A} = (VAR(A), {A})) appear useful for treating kataphora.

3.2 Some technical points concerning variables and compositionality

Before proceeding in the next section to provide further evidence for identifying the essence of a DRS K with its moment P^{0}(K), let us pause here to note some wrinkles in such a proposal that have to do with variables.

It is easy to see that ≡_{0} does not imply equivalence relative to P, because of variables that occur internally in a DRS. Let A be a unary relation symbol, and consider the two ≡_{0}-equivalent updates ¬A(x) and ¬A(y), with characteristic formula ∀z¬A(z). This pair shows that P (K) is not (in general) determined by P^{0}(K) or by {(M, f) ∈ V (K) | dom(f) = U} where K = (U, C). It also provides a counter-example to the strengthening of Lemma 1 mentioned in the end of §2.2. Furthermore, the pair refutes the claim that ≡_{0} is a congruence with respect to the merge operation ^{∩} (or, in other words, that P^{0} is compositional with respect to ^{∩})

K_{¬A(x)} ≡_{0} K_{¬A(y)} but K_{x=x}^{∩}K_{¬A(x)} ≢_{0} K_{x=x}^{∩}K_{¬A(y)} .

This defect can be corrected by modifying the operation ^{∩} to +, just as • was modified to ^{∩}

(U, C) + (U′, C′) := (U ∪ U′, C[U, U′] ∪ C′[U′, U]) .

Under this more symmetric revision of •, we again have P (K + K′) = P (K̂) ∘ P (K̂′), for some K̂ ≡_{0} K and K̂′ ≡_{0} K′, where, in the absence of variable conflicts, K̂ and K̂′ can be taken to be K and K′ respectively. Moreover,

Lemma 5 (Congruence lemma). K_{1} ≡_{0} K′_{1} and K_{2} ≡_{0} K′_{2} imply K_{1} + K_{2} ≡_{0} K′_{1} + K′_{2}.

Proof. The lemma, in fact, holds with ≡_{0} weakened to ≡_{0}^{M}, where K ≡_{0}^{M} K′ means that for all f, ∅ P_{M}(K) f iff ∅ P_{M}(K′) f. Assume without loss of generality that K_{1} + K_{2} = K_{1} • K_{2}. (Otherwise, replace the DRSs by ≡_{0}-equivalent DRSs giving the same sums.) Under this assumption, it is easy to see that χ_{K_{1}+K_{2}} is equivalent to χ_{K_{1}}&χ_{K_{2}}, where χ_{K} is the characteristic formula of K given by Lemma 1. Applying the same reasoning to K′_{1} and K′_{2}, conclude χ_{K′_{1}+K′_{2}} is equivalent to χ_{K′_{1}}&χ_{K′_{2}}, and hence to χ_{K_{1}}&χ_{K_{2}}, provided K_{1} ≡_{0} K′_{1} and K_{2} ≡_{0} K′_{2}. ⊣

4A comparative study of variables in dynamic semantics is undertaken in Vermeulen [17]. A more recent paper, closer in spirit to that of the present work, is Dekker [3], which emphasizes the similarities with first-order logic.

Lemma 5 and the failure of ^{∩} to be a congruence suggest the following notion of a safe merge: (U, C) safely merges with (U′, C′) if C′[U′, U] = C′ — i.e., if K^{∩}K′ = K + K′. Now, it is natural to inquire: why not ban merges that are dangerous? Unfortunately, Lemmas 3 and 4 would not survive a substitution of ^{∩} by +; consider, for example, the first-order formula ∀y¬R(x, y) (where R is a binary relation symbol), which is the characteristic formula of the update (x = x)^{∩}¬R(x, y), but not of x = x + ¬R(x, y) or of any update built from atomic formulas using at most ¬ and +.

Of course, Lemma 3 (whence Lemma 4) could be restored by admitting arbitrary first-order L-formulas (and not just atomic ones) as basic conditions. Indeed, if the only conditions allowed are first-order Lformulas (i.e., if all negations ¬K of DRSs K are replaced by first-order L-formulas, with verification conditions given according to the usual semantics of first-order logic), then the irksome variable clashes noted above evaporate. In particular, under this modification, the input/output relations [[φ]] of the resulting updates φ can be determined from their moments P^{0}(K_{φ}), or from their fixed points (i.e., verifying embeddings) as follows:

[[φ]] = {(s, s′) | s P (U_{φ}, ∅) s′ and s′[[φ]]s′} ,

where (by definition)

U_{φ} := ⋂{dom(f) | (M, f)[[φ]](M, f)}

(with [[φ]] = ∅ if [[φ]] has no fixed point). Such harmony between static (fixed point) semantics and dynamic (relational) semantics (which simplifies Zeevat [18] by eliminating the set U of dicourse markers from the interpretation of a DRS (U, C)) is not possible so long as conditions can be built from negations of DRSs under the semantics specified in section 2.^{5} The approach taken in the present paper to overcoming variable conflicts has been to define merge operations ^{∩} and + that modify • by renaming the variables. But such maneuvers can be avoided by identifying conditions with arbitrary first-order formulas, leading to different input/output relations. (Note that none of the DRSs defined in section 2 has, for example, the input/output relation {((M, f), (M, f)) | f ∈ S_{M} and M ⊧ ∀x¬A(x)}.) On the other hand, the same moments P^{0}(K) would result (since these are still characterized by first-order formulas), and thus the DRSs remain essentially the same, provided the essence of a DRS K is taken to be its moment P^{0}(K). We will return to this matter briefly in the next section (§4.3).

4 DRSs as states

Assuming a DRS amounts to an input/output relation, what does it mean for the input/output pair (s, s′) to be in that relation? If there are two input/output pairs (s, s′_{1}) and (s, s′_{2}) with the same input state s, which state does the DRS output on input s? And secondly, whether or not there is a choice of outputs s′_{1}, s′_{2} possible, how is negation, which is interpreted as the complement of the halting problem, computed? (Notice that negation leads, via the reduction ¬∃x ¬A, to universal formulas ∀x A, falling outside the realm of the recursively enumerable.) An attempt to understand the meaning of “can” in the equivalence

s[[φ]]s′ iff on input s, φ can output s′

runs against two questions: “which?” and “how?” The issues here of non-determinism^{6} and operationalizability are not independent, and are best taken up in sequence, by identifying [[·]] not with P but with S ∘ D ∘ P, where D and S “determinize” and “syntacticize” P respectively. Actually, to understand the effects of determinization D, it is useful to fix an L-model M and to determinize P_{M} before summing over all L-models (to get P).

5Consider the update described in the proof of Lemma 3 that corresponds to the unsatisfiable first-order sentence ∃x¬∃y x = y. That update, call it φ, induces a DRS with the same input/output relation as the DRS (∅, {¬(∅, {¬K})}), where K is ({x}, {¬({x, y}, {x = y})}). Now, it follows (by considering an L-model M with at least two elements, and arguing that [[φ]] cannot return an output if the input assignment is undefined on y) that U_{φ} = {y}, yielding the wrong input/output relation [[φ]].

6Non-determinism does not arise in the present context from ambiguity. The formula φ is unambiguous, insofar as [[·]] is a function. As a matter of methodology, ambiguity is shoved over to the (informal) stage of translating an utterance to a formula:

an utterance may admit translations to several formulas.

4.1 Transitions determined by a model

Given a set L of “labels” on transitions s →^{l} s′ between “states” s, s′, it will often prove convenient to repackage the L-transition predicate →, by which is mean any subset of S × L × S for some set S of states, as the L-model ⟨S, {→^{l}}_{l∈L}⟩, where every l ∈ L is understood to be a binary relation symbol. The chief example of L that will concern us is the set DRS of DRSs (construed as binary relation symbols) over a fixed signature L (not to be confused with L), although we will have cause to expand that set later. The interpretation P of DRSs provides a recipe for cooking up a DRS-transition predicate →_{M} from an L-model M; to wit,

f →^{K}_{M} g iff f P_{M}(K) g .

Abusing notation, P_{M} will be identified with the transition predicate it induces above; and similarly for P. Let us agree to understand isomorphism ≅ between L-transition predicates to mean isomorphism between the associated L-models.

Theorem 6 (essentially Fernando [4]). For all finite or countable L-models M and N, P_{M} ≅ P_{N} iff M ≅ N.

The proof of the non-trivial direction (from left to right) involves a notion that will interest us further below, and has come to be known in the computer science literature as a bisimulation (Park [16]). Given two L-transition predicates → ⊆ S × L × S and and ⇁ ⊆ S′ × L × S′, a binary relation E ⊆ S × S′ is a bisimulation if whenever sEs′ then for every l ∈ L,

(∀x ←^{l} s) (∃x′ ↽^{l} s′) xEx′ and (∀x′ ↽^{l} s′) (∃x ←^{l} s) xEx′ .

Because E occurs only positively in the condition above, there is a ⊆-largest bisimulation (relative to → and ⇁), called bisimilarity and denoted \underline{↔}. When s\underline{↔}s′, the two states are said to be bisimilar, or to be more explicit, the pointed transition predicates (→, s) and (⇁, s′) are bisimilar, denoted again (→, s) \underline{↔} (⇁, s′). Now, returning to Theorem 6, it is easy to see (appealing to DRSs of the form (∅, {x = x})) that P_{M} ≅ P_{N} implies (P_{M}, ∅) \underline{↔} (P_{N}, ∅). Moreover, so long as the label set L includes the DRSs (\{x\}, ∅) (for countably many x ∈ X) and (∅, {A}) for all atomic L-formulas over X, a bisimulation between P_{M} and P_{N} relating ∅ to itself yields a partial isomorphism family, supporting a standard “back-and-forth” argument in model theory (e.g., Keisler [13]) that sums, over finite or countable models, to an isomorphism.

The dependence of the transition predicate P_{M} on its underlying model M can be reduced by internalizing the non-determinism within “disjunctive” states by an operation D, which is essentially the well-known subset construction reducing non-deterministic finite automata to deterministic ones (e.g., Hopcroft and Ullman [9]). It will be convenient for our purposes to define D on pointed transition predicates (→, s_{0}), restricting the newly formed states to non-empty sets accessible from s_{0}. More precisely, given a transition predicate → and a state s_{0}, let D(→, s_{0}) be the pointed transition predicate (⇒, {s_{0}}) generated inductively from its point {s_{0}} as follows: for all l and l′ ∈ L,

(i) if U = {s : s_{0} →^{l} s} ≠ ∅, then {s_{0}} ⇒^{l} U, and

(ii) if U′ ⇒^{l′} U and V = {s : (∃x ∈ U) x →^{l} s} ≠ ∅, then U ⇒^{l} V.

Note that we have only included sets of states accessible from s_{0}, and, moreover, only non-empty sets. Adding the empty set would have amounted to creating a transition from the absence of a transition, trivializing the notion of a bisimulation relative to ⇒. Observe that ⇒ is deterministic in the sense that s ⇒^{l} s′ and s ⇒^{l} s′′ imply s′ = s′′.

Lemma 7. Over deterministic transition predicates → and ⇁, bisimilarity \underline{↔} is just trace equivalence, or, in other words, s\underline{↔}s′ iff tr_{→}(s) = tr_{⇁}(s′), where

tr_{→}(s) = {(l_{1}, l_{2}, …, l_{n}) | n < ω and (∃s_{1}, s_{2}, … s_{n}) s →^{l_{1}} s_{1} and s_{1} →^{l_{2}} s_{2} and ⋯ and s_{n−1} →^{l_{n}} s_{n}}

and similarly for tr_{⇁}.

Now, it turns out that D extracts the first-order content of an L-model M,

T h(M) := {φ | φ is a first-order L-sentence true in M} ,

in the following sense.

Theorem 8 (essentially Fernando [4]). For all L-models M and N, the following are equivalent.

(i) D(P_{M}, ∅) ≅ D(P_{N}, ∅).

(ii) T h(M) = T h(N).

(iii) D(P_{M}, ∅) \underline{↔} D(P_{N}, ∅).

Theorem 8 can be proved from parts 1 and 2 of the characterization lemma (helped along by Lemma 7). Recall that over finite models, elementary equivalence relative to a language with equality (i.e., condition (ii) of Theorem 8) is the same as isomorphism. Over infinite models, elementary equivalence is far weaker. In contrast to Theorem 6, Theorem 8 is very sensitive to additions to the label set. (In particular, it breaks down if labels are built from Kleene star ·^{∗}, although the equivalences can be restored if negation ¬ is thrown out the same time that ·^{∗} is thrown in.)

4.2 Transitions determined by a family of models

It will be useful to strengthen Theorem 8 by passing from a single L-model M to a family M of such. Towards that end, note that there is an obvious definition of a sum ∑_{i∈I}(→_{i}, s_{i}) of pointed deterministic transition predicates (→_{i}, s_{i}) such that

∑_{M∈M} D(P_{M}, ∅) ≅ D̂(P, {(M, ∅) | M ∈ M})

where D̂(→, U) is D(→, s_{0}) except that the initial state {s_{0}} is replaced by U. More precisely, define ∑_{i∈I}(→_{i}, s_{i}) to be the pointed transition predicate (⇒, {s_{i} | i ∈ I}) where ⇒ is generated inductively as

follows: (i) for all l ∈ L, if U = {s | (∃i ∈ I) s_{i} →^{l}_{i} s} ≠ ∅, then {s_{i} | i ∈ I} ⇒^{l} U, and (ii) for all l, l′ ∈ L, if

U′ ⇒^{l′} U and V = {s | (∃x ∈ U) x →^{l}_{i} s} ≠ ∅, then U ⇒^{l} V. Now, Theorem 8 generalizes easily to families of L-models.

Theorem 9 (essentially Fernando [4]). For all families M and N of L-models, the following are equivalent.

(i) ∑_{M∈M} D(P_{M}, ∅) ≅ ∑_{N∈N} D(P_{N}, ∅).

(ii) ⋂_{M∈M} T h(M) = ⋂_{N∈N} T h(N).

(iii) ∑_{M∈M} D(P_{M}, ∅) \underline{↔} ∑_{N∈N} D(P_{N}, ∅).

Given that line (ii) of Theorem 9 can hold for very different families M and N of L-models, Theorem 9 suggests the possibility of building a much cheaper copy of the pointed transition predicate ∑_{M∈M} D(P_{M}, ∅).

4.3 Transitions determined syntactically

Insofar as ∑_{M∈M} D(P_{M}, ∅) is determined by ⋂_{M∈M} T h(M), it is natural to seek a syntactic presentation of the transition predicate. With that in mind, given a first-order L-theory T, define a DRS K = (U, C) to be T -consistent if T ∪ {∃x_{0} ⋯ ∃x_{n} χ_{K}} is consistent, where U = {x_{0}, …, x_{n}} and χ_{K} is a characteristic formula of K given by Lemma 1. (The definition is clearly independent of the exact choice of χ_{K}.) Now, let →_{T} be the following DRS-transition predicate between T -consistent DRSs

{(K, K̂, K′) | K̂ ∈ DRS, and K and K′ are T -consistent DRSs such that K′ = K^{∩}K̂} .

Theorem 10. Let M be a non-empty family of L-models, T = ⋂_{M∈M} T h(M), and P_{M}^{0} be the function from DRSs obtained by relativizing P^{0} to M as follows

P_{M}^{0}(K) := {(M, f) ∈ P^{0}(K) | M ∈ M} .

(a) (→_{T} , (∅, ∅)) \underline{↔} ∑_{M∈M} D(P_{M}, ∅).

(b) DRSs K and K′ are bisimilar relative to →_{T} (i.e., K \underline{↔}_{T} K′) iff P_{M}^{0}(K) = P_{M}^{0}(K′).

(c) ∑_{M∈M} D(P_{M}, ∅) is “strongly extensional.” That is, over the transition predicate of the pointed transition predicate ∑_{M∈M} D(P_{M}, ∅), bisimilarity is equality.

(d) Assume T is r.e. Then there is an r.e. transition predicate ⇝_{T} with the same state set as →_{T} but with one more label than →_{T} such that two DRSs are bisimilar relative to ⇝_{T} iff they are bisimilar relative to →_{T}.

The bisimulation witnessing part (a) is given by the function P_{M}^{0}, which also explains (b) and (c). (Note that the transition predicates are deterministic, whence, by Lemma 7, bisimilarity is just trace equivalence.) The equivalence asserted between the syntactic and semantic transition predicates is not terribly surprising, although a few words about the use of ^{∩} rather than • or + to define →_{T} are perhaps in order. To be more

precise, why not define K →^{K̂} K′ to hold between T -consistent DRSs K and K′ precisely if K • K̂ = K′, or alternatively K +K̂ = K′? The point is that • may conflict with the interpretation of K as P_{M}^{0}(K), while + may conflict with the interpretation of K̂ as P (K̂). Brushing aside such fine points, the reader unimpressed by the syntactic reformulation of ∑_{M∈M} D(P_{M}, ∅) may very well ask: so what? While the strong extensionality of ∑_{M∈M} D(P_{M}, ∅) does not survive the passage to →_{T}, the pay-off in syntacticization is the computational formulation of ∑_{M∈M} D(P_{M}, ∅) described by (d), where ⇝_{T} is →_{T} with the T -consistency restrictions dropped, but an inconsistency check ⊥ added. That is, ⇝_{T} is the (DRS ∪ {⊥})-transition predicate

{(K, K̂, K′) | K^{∩}K̂ = K′} ∪ {(K, ⊥, K) | K is not T -consistent} ,

where T -consistency is co-r.e., provided T is r.e. and consistency is understood in the sense of first-order logic. In summary, the computationally puzzling connective ¬ motivates a syntactic system of non-unique names, under which two names K and K′ denote the same object exactly when they are bisimilar relative to a certain r.e. transition predicate.

The reference above to bisimulations may seem a bit of overkill, given that bisimilarity reduces to trace equivalence, since the relevant transition predicates are deterministic. Except, that is, for the transition predicate P, which is highly non-deterministic, and for which the notion of a bisimulation, rather than that of a trace, supplies the appropriate equivalence lying behind Theorem 6. While there is no denying that the notion of a trace is simpler than that of a bisimulation, the greater scope of bisimilarity as an extensional notion of equivalence can be said to make it that more interesting.

A final point worth mentioning concerns the relativization of the notion of a transition to a first-order L-theory T. Beyond providing a bridge between P_{M} and P, the introduction of a background theory T suggests relegating to that background, conditions in a DRS that are “static” in the sense that they can be replaced by first-order L-sentences (with no free variables). More precisely, given a DRS (U, C), the static conditions referred to form a set C′ ⊆ C such that P (U, C) = P (∅, C′) ∘ (U, C − C′). Transitions from the DRS (U, C) can then be treated as T -transitions from the DRS (U, C − C′), where T is the theory given by the characteristic formula of the DRS (∅, C′). In addition to providing a separation between static and dynamic components, first-order formulas can also be employed to avoid pesky variable clashes (of the kind taken up in §3.2) if we go the whole hog and admit first-order formulas as conditions. (Recall §3.2.) Another way to avoid variable clashes is to keep disjoint sets of variables and parameters, requiring that

(i) in a DRS (U, C), U be a set of variables, whereas the discourse markers in C not declared in U be parameters, and

(ii) embeddings (i.e., variable assignments) be defined only on variables.

Whether this or any of the modifications to DRSs suggested above are worth pursuing are, in the final analysis, probably matters of taste, pure and simple.

5 Discussion

First, a brief review of the preceding sections. Inasmuch as a DRS K is a pair (U, C) of finite sets of discourse markers and of conditions, it is natural to build up a DRS from two DRSs (U, C) and (U′, C′) by merging their sets of discourse markers and conditions respectively, (U, C)•(U′, C′) = (U ∪U′, C ∪C′). But an incremental (sequential) interpretation of a DRS K as an input/output relation P (K) ⊆ S × S suggests analyzing • as relational composition ∘ (by which is meant arranging the equation P (K • K′) = P (K) ∘ P (K′)) which may run afoul of the normal form of a DRS program P (K) because of variable clashes. This defect is easily corrected by redefining the merge K^{∩}K′ of two DRSs K = (U, C) and K′ = (U′, C′) by

(U, C)^{∩}(U′, C′) := (U ∪ U′, C[U, U′] ∪ C′) ,

where C[U, U′] is C with variables occuring in C that belong to U′ − U renamed (according to some fixed scheme) so as to be disjoint from U ∪ U′. Focussing on transitions P^{0}(K) = {(M, f) | (M, ∅) P (K) (M, f)} from the empty embedding ∅, every DRS is induced up to P^{0} by a quantifier-free first-order formula. Unfortunately, the equivalence ≡_{0} modulo P^{0} is not a congruence with respect to ^{∩}, although the blemish can again be repaired by defining + through a careful choice of representatives of ≡_{0}-equivalence classes

(U, C) + (U′, C′) := (U ∪ U′, C[U, U′] ∪ C′[U′, U]) .

Rather than revising the simple-minded merge • by renaming variables (yielding^{∩} or +), variable clashes can be avoided altogether by identifying DRS conditions with arbitrary first-order formulas (instead of closing the set of conditions under negations of DRSs). This modification to the definition of a DRS is a modest proposal, in view of the close correspondence between first-order formulas and DRSs (Lemmas 1 and 3). Under such an alteration or not, the dual nature of DRSs as states and as programs can be brought out by considering transitions between DRSs labelled by DRSs. More precisely, for the unaltered notion of a DRS, define a transition predicate →_{T} relative to a first-order theory T by

K →^{K̂}_{T} K′ iff K^{∩}K̂ = K′, and K and K′ are T -consistent DRSs .  (4)

These transitions can be analyzed semantically by interpreting the program K̂ as P (K̂), and the states K and K′ as P^{0}(K) and P^{0}(K′), respectively (Theorem 10). But as they stand, the transitions in (4) mention only DRSs, and make no reference to variable assignments, so long as consistency is understood syntactically (i.e., as the underivability of a contradiction). As such they are readily mechanizable in a slightly modified form (by ⇝_{T}, Theorem 10 (d)), thereby providing an operational realization of dynamic intuitions about meaning. The “operational realization” here is completely analogous to (and, in fact, depends upon) the introduction in first-order logic of a (syntactic) proof theory to reason about Tarski’s definition of truth relative to abstract objects (such objects being ill-suited for mechanical representation).

Inspecting line (4), observe that two ideas underly →_{T}: a merge operation ^{∩} and a notion of consistency. Let us conclude by taking up these ideas in turn.

5.1 DRSs as abstracts

Inasmuch as abstraction is meaningful only in relation to application, the idea that DRSs are abstracts^{7} can be investigated by considering notions of application on DRSs. DRSs aside, notions of application are particularly interesting from a logical point of view in cases where self-application is permitted. Such a possibility is provided by interpreting application · on DRSs according to the merge operation ^{∩} on DRSs. That is, the application K · K′ of two DRSs K and K′ can be interpreted as K^{∩}K′ modulo a consistency restriction that leads to partiality either (i) by allowing (as in →_{T}) for the possibility of undefinedness, or (ii) by introducing (as in ⇝_{T}) a bottom element ⊥. In either case, self-application is not on its face paradoxical because of the absence of lambda abstraction (and hence paradoxical combinators). In particular, there is no constant k-combinator meeting the requirement kxy = x. The fact is that as functions on DRSs, DRSs have a very special form.

7This theme was suggested by R. Cooper, and taken up in the DYANA meeting of April 1994.

Apart from the merge ^{∩}, there is also the matter of consistency in characterizing →_{T}. If the logic underlying consistency is first-order logic, then the completeness theorem of first-order logic provides a purely syntactic analysis of consistency. In this sense, variable assignments are (pace Barwise [1]) completely dispensable notions (and indeed are, as pointed out in section 4, computationally problematic). This is not to say, of course, that these notions are useless, and indeed consistency might be most naturally studied on the basis of such concepts. But even under a semantic approach, states are more than variable assignments. A DRS applies uniformly to different L-models, and it is not so much f that is interesting as it is the (L ∪ dom(f))-model (M, f). So long as this point is kept in mind, the present author sees little to choose in Cooper [2] between (i) viewing a DRS as a situation-theoretic relation K, with

M ⊧ ⟨⟨K, f; +⟩⟩ iff (M, f) ∈ V (K) (= {s | s P (K) s}) ,

and (ii) interpreting a DRS as a situation-theoretic type V (K), obtained by abstracting out M as well as f from the situation-theoretic (parametric) proposition M ⊧ ⟨⟨K, f; +⟩⟩.

The preceding has been predicated on a first-order notion of consistency. But can such a premiss always be defended? This question takes us to our final subsection.

5.2 Higher-order extensions

Although the terms “DRS” and “condition” were initially qualified in §2 as “first-order DRS” and “firstorder condition”, the designation “first-order” was then promptly dropped. Is there any reason other than laziness lying behind this practice? The clauses syntactically generating DRSs and conditions in §2 are strikingly simple compared to those in Kamp and Reyle [10] and Kamp [12], the latter of which describes seven different formal languages associated with DRT. By contrast, the expressiveness of the DRSs considered here is determined once the background signature L is fixed. Surely the matter cannot be left simply at that, can it?

One reason for optimism is the “adequacy” of first-order logic as a framework for formalizing mathematics. The adequacy referred to here concerns the possibility of encoding most (if not all) mathematical notions in set theory, which, in turn, admits a formulation in the first order language L(∈) with signature L = {∈} given by a single binary relation symbol ∈. Of course, the simplicity of the “universal” language L(∈) has hardly led to its universal use in mathematics (universality in principle being one thing, and universality in practice, quite another). One type of complication when working in L(∈) is easily overcome. Rather than encoding all notions as sets (e.g., presenting real numbers as Cauchy sequences of rational numbers, which are reduced further to sets built from the empty set), the signature can be expanded beyond the binary relation symbol ∈ (introducing, for example, a unary predicate symbol R, and binary function symbols + and × to talk about arithmetic over real numbers). A second, more delicate complication has to do with the notion of an arbitrary set (the root of many foundational headaches). The rather heavy ontological commitments of standard set theory (e.g., ZFC) can be weakened by making more modest demands, capturing the sets of immediate interest. Unfortunately, just what sets are of “immediate interest” may not be terribly clear. Nor is it obvious what is gained by describing such sets relative to some logic with mysterious higher-order notions built in. (But how else can we frame a notion of consistency stronger than first-order logic?) At any rate, if we agree to expel such set-theoretic complications from the province of logic, then it is plausible that first-order DRSs constitute the “logical core” of DRT.

To be more concrete, consider the analysis of plurals and generalized quantifiers in chapter 4 of Kamp and Reyle [10]. The abstraction and duplex conditions there are expressible in first-order logic in exactly the same sense that higher-order logic is first-orderized via Henkin generalized models — i.e., by expanding the signature to accomodate a sort for sets. (Observe that a well-defined generalized quantifier ceases to be “definable” only by banning references to sets.) Of course, if we insist on a particular notion of set given, for example, by the full power set of some infinite set of “atoms,” then the Löwenheim-Skolem Theorem rules out the existence of a set of first-order sentences (over whatever signature) that is satisfied by precisely such models (and their isomorphic copies). Furthermore, assuming the atoms bear a modest resemblance to the natural numbers, the first-order theories of such models, equipped with an additional sort for all sets of atoms, are bound to be unaxiomatizable. But these points are old hat, and the reader is entitled to ask what’s new? The basic thrust of the present paper has been to expose the close relationship between firstorder logic and a fragment of DRT (which was, moreover, described both in semantic and syntactic terms inherited from first-order logic). Alas, if there is any substance to the move from a “static” (truth-centered) view of semantics (in which first-order logic occupies a singular position) to a “dynamic” one, then surely quite a bit remains to be said.

References

[1] Jon Barwise. Noun phrases, generalized quantifiers and anaphora. In E. Engdahl and P. Gärdenfors, editors, Generalized Quantifiers, Studies in Language and Philosophy. Dordrecht: Reidel, 1987.

[2] Robin Cooper. Situation theoretic discourse representation theory. Manuscript, HCRC, Edinburgh, 1992.

[3] Paul Dekker. Predicate logic with anaphora. In Proc. Fourth Annual Semantics and Linguistic Theory Conference. Rochester, New York. May 1994.

[4] Tim Fernando. Transition systems and dynamic semantics. In D. Pearce and G. Wagner, editors, Logics in AI, LNCS 633 (subseries LNAI). Springer-Verlag, Berlin, 1992. A slightly corrected version has appeared as CWI Report CS-R9217, June 1992.

[5] Tim Fernando. A persistent notion of truth in dynamic semantics. In Proc. Fourth Situation Theory and Appplications Conference. Moraga, California. June 1994.

[6] J. Groenendijk and M. Stokhof. Dynamic predicate logic. Linguistics and Philosophy, 14, 1991.

[7] David Harel. Dynamic logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 2. Dordrecht: Reidel, 1984.

[8] Irene Heim. The semantics of definite and indefinite noun phrases. Dissertation, University of Massachusetts, Amherst, 1982.

[9] J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Language and Computation. Addison-Wesley, 1979.

[10] H. Kamp and U. Reyle. From Discourse to Logic. Kluwer Academic Publishers, Dordrecht, 1993.

[11] Hans Kamp. A theory of truth and semantic representation. In J. Groenendijk, T. Janssen, and M. Stokhof, editors, Formal Methods in the Study of Language. Mathematical Centre Tracts 135, Amsterdam, 1981.

[12] Hans Kamp. Discourse Representation Theory as a knowledge representation language. Handout for a talk, 1993.

[13] H. Jerome Keisler. Fundamentals of model theory. In J. Barwise, editor, Handbook of Mathematical Logic. North-Holland, Amsterdam, 1977.

[14] Reinhard Muskens. A compositional discourse representation theory. In Proc. Ninth Amsterdam Colloquium. ILLC, University of Amsterdam, 1994.

[15] P. Pagin and D. Westersthl. Predicate logic with flexibly binding operators and natural language semantics. J. Logic, Language and Information, 2(2), 1993.

[16] David Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proc. 5th GI Conference, LNCS 104. Springer-Verlag, Berlin, 1981.

[17] C.F.M. Vermeulen. Merging without mystery. Technical report, Logic Group Preprint Series Number 70, Philosophy Department, Utrecht, December 1991.

[18] Henk Zeevat. A compositional approach to discourse representation theory. Linguistics and Philosophy, 12, 1989.