if P is a term of type et, R is a term of type e (et) and the τ’s are either
discourse referents or terms of type e. This gives us our basic conditions of
the DRT language as terms of type st. In order to have complex conditions
and boxes as well, we shall write
not Φ for
Φ or Ψ for
Φ ⇒ Ψ for
[u1 . . . un | γ1 ,. . . ,γm] for
Φ ; Ψ for
λi-∃j φ(i )(j),
λi∃j(Φ(i)(j) ∨ Ψ(i)(j)),
λi∀j (Φ(i)(j) → ∃k Ψ(j)(k)),
λiλj(i[u1,...,un]j ∧ γ1(j) ∧...∧ γm(j)),
λiλj∃k(Φ(i)(k) ∧ Ψ(k)(j)).
Here Φ and Ψ stand for any term of type s(st), which shall be the type
we associate with boxes, and the γ's stand for conditions, terms of type st.
[u1 . . . un | γ1 ,. . . ,γm] will be our linear notation for standard DRT boxes and
the last clause embodies an addition to the standard DRT language: in order
to be able to give compositional translations to natural language expressions
and texts, we borrow the sequencing operator ‘;’ from the usual imperative
programming languages and stipulate that a sequence of boxes is again a
box. The following useful lemma is easily seen to hold.
Merging Lemma. If ~u0 do not occur in any of ~γ then
|=AX [~u | ~γ]; [~u0 | ~γ0] = [~u~u0 | ~γ~γ0]
The present emulation of DRT in type logic should be compared with the
semantics for DRT given in Groenendijk & Stokhof [1991]. While Groe-
nendijk & Stokhof give a Tarski definition for DRT in terms of set theory
and thus interpret the object DRT language in a metalanguage, the clauses
given above are simply abbreviations on the object level of standard type
logic. Apart from this difference, the clauses given above and the clauses
given by Groenendijk & Stokhof are much the same.
5 From Semantic Recipes to Boxes
Now that we have the DRT language as a part of type logic, connecting Lam-
bek proofs for sentences and texts with Discourse Representation Structures
is just plain sailing. All that needs to be done is to define a function type
of the kind described in section 3 and to specify a lexicon for some frag-
ment of English. The general mechanism that assigns meanings to proofs