Parsing as Sequential Construction of Logical Forms

Wilfried Meyer Viol

Abstract

In this paper we give a formal description of the parsing model that underlies the treatment of Long Distance Dependencies, Topic and Focus, Ellipsis and Quantification in, amongst others, the papers [1996],[1997], [1999a],[1998],[1999b]. In this model, a natural language string consists of a sequence of ‘instructions packages’ to construct some term in a formal representation language, the logical form of the string in question. Parsing, then, is the process of executing these packages in a left to right order.

Contents

1 Terms as Decorated Trees 2

2 Goal-Directedness 7

3 Actions 10

4 The Parsing Process 12

5 Conclusion 14

Introduction

In this paper we will give a formal description of the parsing model that underlies the treatment of Long Distance Dependencies, Topic and Focus, Ellipsis and Quantification in, amongst others, the papers [1996],[1997],[1999a],[1998],[1999b]. Although the intuition behind the model is quite natural, nevertheless, it seems not to have been explored to any extent. The main idea is to view a natural language string s = w_{1}w_{2} … w_{n} as projecting a sequence of ‘instructions packages’ to construct some term T in a formal representation language, this term being the supposed interpretation or logical form of the string in question. Parsing, then, is the process of executing these packages in a left to right order:

P ARSE(s) = (⟨w_{1}, T_{1}⟩, … ⟨w_{n}, T_{n}⟩),

where each T_{i+1} is a partial logical form, the result of executing w_{i} on form T_{i}, T_{1} is the result of processing w_{1} on a starting form T_{0} and, provided s is grammatical, T_{n} is a complete logical form. The model we are going to introduce to formalize this process is shamelessly eclectic.

— The partial logical forms constitute the domain P T of a partially ordered Kripke frame M = ⟨P T, ≤⟩ on which the standard logical connectives and operators are given an intuitionistic interpretation.

— The partial logical forms in this frame are themselves represented as partial decorated binary trees T and the partial order ≤ reflects tree growth. On these trees the modal operators of the Logic of Finite Trees are interpreted. So the structure up to this point is an intuitionistic multi-modal frame M = ⟨P, ≤, ≺_{i}⟩_{i∈I} and represents the space of partial logical forms.

— The parsing process is now a goal-directed movement through this space towards the set LoF o ⊂ P T of complete Logical Forms. This goal-directedness will be represented by a requirement function R which adds to every node of a partial tree a (finite) set of requirements that have to be fulfilled (so, if T ∈ LoF o and n is a node in T , then R(n) = ∅). Addition of a requirement function gives the structure M = ⟨P, ≤, ≺_{i}, R⟩.

— Finally, the words the words w_{1}, …, w_{n} of a string natural language s and the general principles of that language will be represented as incremental actions which map partial logical forms to enriched ones. That is, on top of the intuitionistic modal frame with requirements, we now add a PDL like structure^{1} of actions A such that w_{1}, …, w_{n} ∈ A. This gives our final structure M = ⟨P T, ≤, ≺_{i}, R, A⟩.

1 Terms as Decorated Trees

In order to handle partiality of logical forms in a flexible way, we represent the elements of each D_{i} as decorated finite partial trees. Logical forms are built up by one or more ways of putting together basic semantic entities.

1PDL stands for Propositional Dynamic Logic.

\underbrace{[_{0}[_{0} ] [_{1}[_{1} ] [_{1} [_{0} ][_{1} ]]]}_{T ree}

\underbrace{\{00:john, 011:λxλyread(x)(y), 0111:λP (someP), 0110:(x, bookx)\}}_{Decorations}.

Figure 1: A Term as a decorated tree

Each of these modes of combination can be associated with a product typeconstructor. A term in a language appropriate for these type-constructors can be represented as a finite binary branching tree, where every binary branching ⟨b_{1}, b_{2}⟩ reflects the presence of a subterm O(b_{1}, b_{2}) for some operator binary O. As an example, let APL be the operation of function application in a typed lambda calculus. The sentence John read a book, represented by the formula read(john, some(x,book(x))), can be seen as resulting from the unreduced lambda term

APL(APL(λxλyread(y)(x), APL(λP (someP), (x, bookx)), john)

by β-reduction. In Figure 1. we have represented this term as a binary tree structure with an associated set of node decorations. (Here ‘[_{0}’ means argumentand ‘[_{1}’ function-daughter of the APL operator.) By representing terms in this way, we can address term structure and term content separately. In particular, we can represent partially specified trees that are, moreover, only partly decorated. Such decorated tree structures have to be constructed in the course of a parse through an NL string. In order to deal with the partial logical forms arising during a parse we consider T -structures,

Definition 1 (T -Structures) A T -structure is a quintuple of the form T = ⟨T, ≺_{0} , ≺_{1}, ≺_{↓}, ≺_{∗}⟩ where T is a non-empty domain of tree nodes and ≺_{i},for i ∈ I = {0, 1, ↓ , ∗}, is a (possibly empty) binary relation on T. The set BT consists of those T -structures which are ordered as binary trees, where ≺_{0} is the right-daughter and ≺_{1} the left-daughter relation, ≺_{↓} is the immediate dominance relation (≺_{↓}=≺_{0} ∪ ≺_{1}), and ≺_{∗} is the dominance relation, i.e., the reflexive and transitive closure of ≺_{↓}.

Definition 2 (Partial Trees) A function f is a T r-morphism from T -structure T in T -structure T′ if it maps T in T′ such that for all n, m ∈ T, for all i ∈ I: n ≺_{i} m ⇒ f(n) ≺_{i} f(m). The set P T, of partial trees, consists of all T -structures T such that there is a T r-morphism mapping T to an element of BT, i.e., a binary tree.

In a full-blown binary tree, n ≺_{∗} m implies that there is a sequence of immediate dominance steps relating n to m, but in a partial tree this does not need to be the case. The under-specified tree relations (≺_{↓} and in particular ≺_{∗}), play an essential role in constructing the term while traversing the string in a left to right fashion: we cannot always decide on the spot where specifically a certain subterm has to function in the eventual term. Given the string A book John read, we do not yet know what to do with A book at the start of the sentence.

\underbrace{[_{0}[_{0} ] [_{∗} [_{0} ],[_{1} ] ]…]}_{T ree} \underbrace{\{00 : John, 0 ∗ 1 : λP (someP), 0 ∗ 0 : (x, bookx)\}}_{Decorations}.

Figure 2: A Partial Term as a partial decorated tree

After having parsed A book john the partial logical form constructed is shown in Figure 2, which gives a partial tree model with an under-specified tree relation. This under-specified relation constrains the set of completions to those binary trees which have this relation witnessed by an immediate dominance sequence.

Partial trees are constructed in stages and node by node and we need a pointer to identify the nodes at which action is to take place, that is, our representations of partial logical forms consist of pairs ⟨T , n⟩, which we will write as T n, a partial tree T together with a pointer indicating some node n ∈ T.

Definition 3 (Structure of Pointed Partial Trees) Let P P T = {T n | T ∈ P T, n ∈ T } be the set of pointed partial trees. We set T n ≺_{i} T′n′ if T = T′ and n ≺_{i} n′, and T n ≤ T′, n′ if there is a T r-morphism f : T ↦ T′ such that f(n) = n′. The frame of Pointed Partial Tree structures can now be defined as

PPT = ⟨P P T, ≺_{i}, ≤⟩_{i∈{0,1,↓,∗}}.

Along ≤, a pair n, m ∈ T such that n ≺_{∗} m may be mapped by T r-morphism f to a pair such that f(n) ≺_{↓} f(m) and later, by some T r-morphism g, to a fully specified relation g(f(n)) ≺_{0} g(f(m)).

The Language DU

On Pointed Partial Tree Structures we can interpret the Language of Finite Trees, LF T (see [1]), a propositional modal language with the modalities ⟨0⟩ϕ (“ϕ holds on the first daughter”), ⟨1⟩ϕ (“ϕ holds on the second daughter”), ⟨↓⟩ϕ (“ϕ holds on some daughter”), ⟨∗⟩ϕ (“ϕ holds here or somewhere below”), ⟨L⟩ϕ (“ϕ holds on a linked node”), their converses ⟨i^{−1}⟩, and their universal variants [ i ], [ i^{−1} ], for i ∈ {0, 1, ↓, ∗}. In the tree of Figure 1, for instance we have the following

— ⟨0⟩F o(John) and ⟨1⟩⟨1⟩λxλyread(x)(y) hold at the top node 0.

— ⟨↓^{−1}⟩⟨∗⟩F o(x, bookx)) holds at node 00 decorated by F o(John).

where the atomic formulas are designed to describe Declarative Units decorating binary (linked) tree structures. Declarative units are pairs consisting of a sequence of labels followed by a content formula. We have seen examples of content formulas in the denotations john, (x, Bookx) and λxλyread(x)(y). The types e, t and e → t from these examples are instances of labels. The descriptions of declarative units determine the atomic vocabulary. So, our language has monadic predicates La_{1}, … La_{n}, F o, standing for n label dimensions and a formula dimension and individual constants from D_{La_{1}}, … D_{La_{n}}, D_{F o} respectively, denoting values on these dimensions. The atomic propositions of the language then have the form La_{i}(t) or F o(t) where t is either an element of the appropriate domain D_{La_{i}}, D_{F o}, or it is a meta variable. A declarative unit can then be completely represented by a finite set of atomic propositions.

{La_{1}(l_{1}), … La_{n}(l_{n}), F o(Ψ)},

and a partial declarative unit, an object naturally arising in the course of a parse, is merely a subset of a description of a declarative unit.

The language, DU, we have settled on to describe partial \underline{D}eclarative \underline{u}nits and their developments towards logical forms, includes the tree modalities from LFT, the standard Boolean constants and connectives and existential and universal quantifiers ranging over the set of label and formula values.

Definition 4 (The Representation Language DU) A proposition A of the language DU has one of the following shapes:

A ::= ⊤ | ⊥ | La_{1}(l_{1}) | … | La_{n}(l_{n}) | F o(ϕ) | Eq(t_{1}, t_{2}) | A ∧ A | A ∨ A | | A → A | ∃xA | ∀xA | ⟨#⟩A | [#]A

for VAR= {x, x_{1}, x_{2}, …, y, …} a denumerable set of individual variables, MV a denumerable set of meta variables, predicate values l_{i} ∈ D_{La_{i}} ∪ VAR ∪ MV, for each i: 1 ≤ i ≤ n, ϕ a logical form in D_{F o} ∪ Var ∪ MV, t_{1}, t_{2} ∈ D_{La_{i}} ∪ D_{F o} ∪ V AR ∪ MV and # a modality i or i^{−1} for i ∈ {0, 1, ↓, ∗}. The quantifier variables are rendered in boldface to distinguish them from the variable bound by quantifiers in the domain D_{F o}, i.e., variables occurring in the logical forms under construction.

As is standard, this language is interpreted over Pointed Partial Trees by means of Valuation functions V.

Definition 5 (Pointed Partial Tree Models) A Pointed Partial Tree Model M is a pair M = ⟨PPT , V ⟩ consisting of a Pointed Partial Tree Structure PPT and a valuation V assigning finite sets of atomic formulas to elements T n ∈ P P T, and satisfying the following principle

T n ≤ T′n′ ⇒ V (T n) ⊆ V (T′n′).

This principle guarantees that once an atomic proposition has been established at some node in a partial tree, this proposition will remain to hold there throughout all future developments of that tree. These pointed partial tree will now be used to represent (unreduced) partial lambda terms as in Figures 1 and 2.

Definition 6 (Truth Definition for DU) Given a Pointed Partial Tree Model M = ⟨PPT , V, ⟩, a set D = ⋃_{i≤n} D_{La_{i}} ∪ D_{F o} of label and formula values, a set MV of meta variables, t_{1}, t_{2} ∈ D ∪ MV we say that pointed tree T n ∈ P P T of M satisfies formula ϕ, with the notation

T n ⊧_{M} ϕ,

if ϕ is atomic and ϕ ∈ V (T n) ϕ ≠ ⊥ ϕ = ⊤

ϕ = Eq(t_{1}, t_{2}) and t_{1} = t_{2}
ϕ = ψ ∧ χ  and T n ⊧_{M} ψ & T n ⊧_{M} χ
ϕ = ψ ∨ χ  and T ⊧_{M} ψ or T n ⊧_{M} χ
ϕ = ψ → χ  and for all T′n′ : T n ≤ T′n′,
if T′n′ ⊧_{M} ψ then T′n′ ⊧_{M} χ
ϕ = ∃xψ  and there is a t ∈ D : T n ⊧_{M} ψ[t/x]
ϕ = ∀xψ  and for all T′n′ : T n ≤ T′n′ and all t ∈ D
T′n′ ⊧_{M} ψ[t/x]

if i ∈ {0, 1, ↓, ∗} and

ϕ = ⟨i⟩ψ  and ∃T′n′ ∈ P P T : T n ≺_{i} T′n′ and T′n′ ⊧_{M} ψ
ϕ = ⟨i^{−1}⟩ψ and ∃T′n′ ∈ P P T : T′n′ ≺_{i} T n and T′n′ ⊧_{M} ψ
ϕ = [i]ψ  and for all T′n′ : T n ≤ T′n′ and all T′′n′′ ∈ P P T
if T′n′ ≺_{i} T′′n′′ then T′′n′′ ⊧_{M} ψ
ϕ = [i^{−1}]ψ and for all T′n′ : T n ≤ T′n′ and all T′′n′′ ∈ P P T
if T′′n′′ ≺_{i} T′n′ then T′′n′′ ⊧_{M} ψ

As usual, we can introduce negation by the definition

¬ϕ ≡_{df} ϕ → ⊥.

The operators and modalities with universal force (‘ →′, ‘∀′, ‘[#]′) quantify not only over (nodes of the) current (partial) decorated trees, but over possible developments of the current structure. For instance, the top node of the current decorated partial tree need not be the root node of the eventual tree. Given that we have a falsum ⊥ (satisfied by no node) and verum ⊤ (satisfied by all nodes) in our language we can ‘close off’ the top node by T n ⊧_{M} [↓^{−1}] ⊥. This closing off is an operation that can take place on a tree the moment all words of the NL string have been processed: the node that happens to be the top one at that moment is turned into a root node. At the other end of the tree we can declare bottom nodes to be terminal nodes by annotating them with [↓]⊥. This is a task of the lexical entries associated with the words: a word closes off a branch downwards.

By definition we have persistence of atomic DU-formulas. By the form of the Truth definition, this can be lifted to the whole of DU. So, if ϕ is a DU-formula, T n ⊧_{M} ϕ and T n ≤ T′n′, then T′n′ ⊧_{M} ϕ.

It may be illuminating to view some typical interactions between the tree modalities and connectives, like implication, with universal force. In a model M we can have T n ⊧_{M} ⟨∗⟩ϕ without there being a sequence T n ≺_{↓} … ≺_{↓} T n′ such that T n′ ⊧_{M} ϕ. In a partial tree the relation ≺_{∗} between two nodes entails only that the path between them can always be completed to a fully specified one. So, on Pointed Partial Tree Models the basic logic of finite trees holds ‘under double negation’: if ϕ is an LF T theorem, i.e., ⊧_{LF T} ϕ, then T n ⊧_{M} ¬¬ϕ for every model M.

The meta variables can be distinguished from the proper values by the fact that only for a proper value l_{i} ∈ D_{La_{i}} we have the satisfaction of ∃xLa_{i}(x). ∃xψ holds at a node if ψ[t/x] holds there for some t ∈ D. That is, a meta variable U won’t do as this is not an element of D. We want the existential quantifier to be able express that some label or feature predicate has a proper value. Apart from the LF T principles we will have to introduce axioms regulating the behaviour of the F o and T y predicates on the trees. For instance, a node may be annotated by at most one type. This requires a principle of the form

∀x∀y(T y(x) ∧ T y(y) → ¬Eq(x, y)).

Furthermore, the F o and T y values at the daughters of some node have to be related to the values on those predicates at the node itself

∀x∀y(⟨0⟩T y(x) ∧ ⟨1⟩T y(x → y) → T y(y)).

2 Goal-Directedness

Within the domain P P T of a partial tree model M = ⟨PPT , V ⟩, we can identify the set LoF o consisting of the decorated partial trees that correspond to (unreduced) terms of the typed lambda calculus. Grammatical strings, the words of which project actions mapping one pointed partial tree to a next one, must create elements of this subset of P P T. In all elements of LoF o, the root node, for instance, will be annotated by a lambda term of type t. Thus, in any partial stage, that root node will have a requirement that it be annotated by a lambda-term of type t, a sub-node of the root that it be annotated by a term of type e, and so on.^{2} All nodes are introduced with requirements. Requirements form an essential feature of the tree - they determine a set of ‘successful’ extensions of a given (partial) tree, namely those in which all requirements are satisfied. Consequently, our basic data structures are tree structures, the nodes of which consist of (partial) declarative units paired with finite sets of requirements. To model these requirements we add a requirement function R to the model assigning a finite number of (arbitrary) DU-formulas to elements T n. These formulas represent a finite number of requirements on that node (as opposed to the facts at that node assigned by V). Figure 3 represents a decorated partial tree resulting from having parsed John read. This tree includes a node with a requirement for an object of type e (this node-plus-requirement is introduced, “sub-categorized for”, by the verb read).

Definition 7 (Models with Requirements) A Pointed Partial Tree Model with requirements is a tuple M = ⟨M, R⟩, where M = ⟨PPT , V ⟩ is a Pointed Partial Tree Model and R is a function assigning finite sets of DU formulas to elements of P P T and satisfying the following constraint:

T n ≤ T′n′ ⇒ R(T n) ⊆ (T h(T′n′) ∪ R(T′n′)),

2This use of requirements on the development of a tree node has some resemblance to the familiar concept of ‘sub-categorisation’, as a node decorated by the labelled formula T y(e → (e → t))), F o(read) within a tree may have a mother node which is decorated with a requirement ⟨1⟩T y(e) (that is, a requirement for an internal argument for ‘read’).

\underbrace{[_{0} [_{0} ], [_{1}[_{0}], [_{1}]]]}_{T ree}

{00 : John, 011 : λxλyread(x)(y), 010 : ?Ty(e)}

Decorations

Figure 3: Partial decorated tree with requirements

where T h(T n) = {ϕ ∈ DU | T n ⊧_{M} ϕ}. The successful developments, that is, the developments in which all requirements are satisfied, of a pointed partial tree T n we collect in the set LoF o(T n) of (supposed) \underline{Lo}gical \underline{Fo}rms into which T n can develop.

LoF o(T n) = {T′n′ ∈ P P T | T n ≤ T′n′ : R(T′n′) = ∅}.

Unlike the valuation functions, a requirement function is not restricted to atomic propositions; we are free to require any (finite number of) DU-formula(s) at some tree node. Along the growth relation ≤ requirements may disappear, but only by becoming facts. For instance, we have

[_{a} ?T y(e) ] ≤ [_{a} F o(ϕ), T y(e),?T y(e) ] ≤ [_{a} F o(ϕ), T y(e) ].

But also, (for U a meta variable),

[_{a} F o(U),?∃xF o(x),?T y(e) ] ≤ [_{a} F o(U), F o(John), T y(e) ].

Having introduced the concept of a requirement over Pointed Partial Tree Models we will exploit it by introducing some constants to the language DU which address the status of the requirements.

Definition 8 (Truth Definition for Requirements) Given a Pointed Partial Tree Model with requirements, M = ⟨M, R⟩, we say that pointed tree T n of M satisfies formula ϕ, with the notation

T n ⊧_{M} ϕ,

if

ϕ ∈ DU and T n ⊧_{M} ϕ,
ϕ =?ψ and ψ ∈ R(T n)
ϕ =?∅  and R(T n) = ∅
ϕ = Fψ and ∃T′n′ ∈ LoF o(T n) : T′n′ ⊧_{M} ψ
ϕ = Gψ and ∀T′n′ ∈ LoF o(T n) : T′n′ ⊧_{M} ψ

A requirement ?ϕ holds if the formula ϕ occurs on the the requirement list of that node, and ?∅ is a constant which holds at a node if it has an empty requirement list. Proposition Fψ holds at node T n if there is at least one development of T n to (a node in ) a logical form where ψ holds, and Gψ holds at node T n if ψ holds at all developments of T n to logical forms. A tree node T n has requirements that can be satisfied iff F⊤ holds at T n. This allows us to define a conditional: ϕ →_{gr} ψ ≡_{d} (F⊤ ∧ ϕ) → ψ. This conditional expresses invariances shared only by successful developments. If the procedure that leads from Axiom to an element of LoF o is sound, then the final tree represents, is isomorphic to, an unreduced term in the language of our logical forms.

The uses of requirements

Consider all terms of the typed lambda calculus we use to formulate our logical forms, the representations of the formal meanings of the natural Language strings under consideration. The elements of this set are our target structures the NL strings have to construct. We represent these terms as trees by their applicative structure (that is, a subterm (λxϕ, ψ) is represented as a binary branching point with λxϕ annotating the function - and ψ the argument daughter). At the nodes of these representations we hang empty sets. These empty sets represent empty sets of requirements. This we now turn into the set LoF o of some Pointed Partial Tree Model M, by adding all partial versions that can be extended to elements of the LoF o. Now, in order to guarantee that the set LoF o, defined in terms of fulfilled requirements, and the set of representations of terms in our typed lambda calculus coincide, every abstraction of such a term to a partial object has to be compensated by the introduction of a requirement. Starting, for instance, from the term read(John, (a, x, bookx)) we can create a partial term by abstraction over John. This abstraction is not a term of our typed lambda calculus, so it should not belong to LoF o. By definition, this means that there must be some unfulfilled requirement associated with it. But this does not have to be a requirement for exactly ‘John’. It may (and, in fact, will) be merely a requirement for type e. So here is where the invariances of the process come in.

Given a specific feature of the logical forms we are interested in, the first question is now always: can we devise a system of requirement introduction such that the fulfillment of all requirements annotating a given tree corresponds exactly to a completing this tree to a term of our typed Lambda Calculus with the desired feature?. We will give an example of a requirement strategy to the effect that the set LoF o coincides with the set of a binary tree structures. That is, no under-specified tree relations of the form ≺_{∗} or ≺_{↓} are left in LoF o that are not the reflexive transitive closure of the immediate dominance relation or the union of argument and function daughter relation, respectively. The idea is to introduce a Tree Node label, a monadic predicate ‘T n’ with values in D_{T n} = {a · x, x | a ∈ A, x ∈ {0, 1, L}^{∗}}. That is, a value of this predicate is a finite sequence of elements of {0, 1, L} possibly preceded by a constant from a set A. When trees are constructed in the parsing process, in general it is not known whether a description that starts off as a top node will remain so (and thus be the root node of the eventual tree. This is why we introduce a new node invariably with ‘address” a ∈ A, satisfying a formula T n(a), a is a constant not yet occurring in the construction. In interaction with the tree modalities various constellations are expressible. So, given the formula T n(a), expressing the location of a node description in the tree under construction, we can fix

T n(a0) ↔ ⟨0^{−1}⟩T n(a),
T n(a1) ↔ ⟨1^{−1}⟩T n(a),^{3}

and we can fix the root node of a tree as follows,

3We will also need T n(aL) ↔ ⟨L^{−1}⟩T n(a) when we consider Linked Trees.

T n(0) ↔ [↓^{−1}]⊥.

(Significantly, we do not ‘internalize’ the under-specified modalities ⟨∗⟩ and ⟨↓⟩ as values of the T n predicate.) The Tree Node formula T n(0) holds at a node if it is a top node and remains so throughout all developments. (Note the use of the ‘falsum’ - “At every node above the current one ⊥ holds.” As ⊥ is satisfied by no node at all (Definition 6) this means that there are no nodes above the current one.) Now when we introduce a tree node with an under-specified relation to the source node, as we do in Figure 5, we add the requirement for ∃xT n(x) to the node with under-specified address:

\frac{[_{a} ?T y(t)], a}{[_{a} ?T y(t), [_{∗} ?T y(e),?∃xT n(x)]]}

The point is that this requirement can only be satisfied when the node it decorates is merged with one that has a fully specified relation to the top node of the tree: only in that case will there be a t ∈ D_{T n} such that T n(t) holds at the node. So if, starting from the Axiom, we introduce tree nodes with underspecified tree only if they are accompanied by requirements for values on the T n predicate, then in all elements of LoF o that we can reach all underspecification with respect to tree relations will have been resolved.

As a second example, an analogous mechanism allows us to introduce meta variables or placeholder values projected by pronominals with the requirement that they have to be substituted by a proper value in order for the term to be complete.

\frac{[_{a} ?T y(e) ]}{[_{a} F o(U), T y(e),?∃xF o(x) ]}

An object of type e has been supplied, but a new, weaker, requirement has taken its place. Only a development that supplies a concrete value for the meta variable U in F o(U) can end up in LoF o.

3 Actions

In a final enrichment we now extend the Pointed Partial Tree models with requirements by a set A of actions. An action α is an element of A ⊆ P P T^{P P T}, that is, actions are functions over PPT. An action α may map a Pointed Partial Tree to a number of other such trees. The actions we will introduce are fitted to the Pointed Partial Tree Models in that they are incremental in the sense that T′n′ = α(T n) entails that either T n ≤ T′n′ or T = T′. So an incremental action is either some construction or a pointer movement. The actions are put together from basic or atomic actions. The basic actions consist of: creation of new nodes relative to old ones; decoration of nodes, moving to nodes, and substitution at nodes. These action may now be combined to complex ones by, essentially, the PDL operations.^{4}

4PDL is Propositional Dynamic Logic.

Definition 9 (Actions) For M a Pointed Partial Tree Model with Requirements, # is i or i^{−1} for i ∈ {0, 1, , ↓, ∗, L}, ϕ either an atomic DU formula or of the form ?ψ for arbitrary ψ ∈ DU, the set A of actions contains the following elements:

Basic Actions

1. 1 = {⟨T n, T n⟩ | T n ∈ M}, AB = ∅. These represent the halting action and the Abort action respectively.

2. make(#). This action creates a node T′n′ such T′ = T ∪ {n′} and that T′n ≺_{#} T′n′.

3. go(#). Here go(T n) = (T′n′) implies T n ≺_{#} T′n′.

4. put(ϕ). Here, put(ϕ)(T n) = T′n′ implies that T = T′ except that V (T′n′) =

V (T n) ∪ {ϕ} if ϕ is atomic and R(T′n′) = R(T n) ∪ {ψ} if ϕ =?ψ. Complex Actions We can put actions together by executing one after the other (sequential composition ‘;’) and doing that any finite number of times (finite iteration ‘∗’), or by indeterministically choosing between them (indeterministic choice ‘+’).

5. if α, α′ are actions, then so are α; α′, α + α′, α^{∗}. Finally, we can put actions together in a conditional IF THEN ELSE statement.

7. If Σ is a set of formulas all free variables of which occur in \overline{x} and α, α′ are actions then ⟨Σ(\overline{x}), α, α′⟩ is a conditional action with the definition: ⟨Σ(\overline{x}), α, α′⟩ = \{⟨T n, T′n′⟩ ∈ α[\overline{t}/\overline{x}] | \overline{t} ∈ (D ∪ MV)^{∗}, T ⊧_{M} Σ[\overline{t}/\overline{x}]\}∪

\{⟨T n, T′n′⟩ ∈ α′ | ¬∃\overline{t} ∈ (D ∪ MV)^{∗}, T n ⊧_{M} Σ[\overline{t}/\overline{x}\}.

That is, if Σ holds at T n, for some substitution of t for variable x, then action α is executed where in the body of this action the variable x is also replaced by t. If Σ does nor hold at T n for any substitution for x, then action α′ is executed.^{5} For instance we can define actions which transport features from one node (e.g. a ‘head’) to another.

• ⟨{F o(x)}, go(⟨0⟩); put(F o(x)), AB⟩ maps the value of the F o feature at the current node, if there is such a value, to the F o feature at the left daughter, otherwise it aborts.

We may also define an action that enables pointer movement to the closest clausal node:

• gofirst(?T y(t)) = ⟨{?T y(t)}, 1, go(⟨↓^{−1}⟩)⟩^{∗}; ⟨{?T y(t)}, 1, AB⟩. The action gofirst(X) moves the pointer upwards to the first higher node with annotation X, i.c. the requirement T y(t), and then stops.

The actions projected by the words of a language are conditional statements like

• John = IF {?T y(e)} THEN put(F o(john), T y(e), [↓]⊥) ELSE AB The word test whether the pointed node requires an object of type e. If so, then it places the Formula John there and closes off the node downwards. We have two ‘pure’ classes of actions. Complex constructions (that is, compositions of actions without the go action) induce complex tree growth. Complex movements on the other hand (the family of go(⟨#i⟩) instructions closed under the given operations) represent pointer strategies. In general, for instance, in case of actions projected by words, the actions are a mixture of these classes.

5The PDL tests do not suffice over this propositional logic because we want the ability to formulate IF THEN ELSE statements and only in the context of excluded middle can these be defined in terms of the PDL test.

4 The Parsing Process

The object of the parsing process is to construct a binary tree structure the top node of which is decorated by a formula of type t while using all information in an NL string. The minimal element in the model M, the starting point of every parse^{6} is the Axiom

Axiom: [_{a} ?T y(t)], a.

The Axiom is the Pointed Partial Tree Model consisting of a single node (thus the location of the pointer), the putative top node, with empty valuation function and requirement for an object of type t.

In the course of a parse starting from the Axiom the description of a tree is created. A parse ends essentially after the last word of an NL string has been processed. A successful parse of a grammatical NL string must result in a logical form, that is, a Pointed Binary Tree in the set LoF o of M. That is, it must end with a Tree where all nodes are associated with an empty list of requirements.

Goal [_{a}, …, T y(t) ], [_{a0}…], [_{a1}…] …], a ∈ LoF o.

If the procedure that leads from Axiom to an element of LoF o is sound, then the final tree represents, is isomorphic to, an unreduced term in the language of our logical forms. Now, this (representation of an) unreduced lambda term may be normalized in ways depending on a variety of labels collected on the tree during the parse.

Figure 4 shows the structures arising in the course of parsing “John read a book”. Notice that each new structure is a development under the ≤ relation.

The course from Axiom to Goal must be licensed by the natural language under consideration within the context of some language external, pragmatic, mechanisms. That is, with a natural language L there are associated three sets of actions.

— A set C of Computational rules. These are actions which bring out information contained in the current Tree and make hypotheses about structure.

— A set L Lexical actions. These actions map one Tree to a next one adding information in the process. The elements of L are projected by the Natural Language words. Lexical transition are defined as conditional actions of the IF

6of an NL string in isolation, i.e., without a context.

[_{a} ?T y(t)], a  Axiom
⇒_{C} [_{a} [_{0} ?T y(e)], [_{1} ?T y(e → t)]], a0  ↓
⇒_{L} [_{a} [_{0} , F o(John), T y(e)], [_{1} ]], a1  John
⇒_{L} [_{a} [_{0} ], [_{1} [_{1} F o(λxλyread(x)(y)), T y(e → (e → t))], [_{0} ?T y(e)]]], a10 read
⇒_{LC} [_{a}[_{0} ], [_{1}[_{1} ], [_{0} F o((a, x, bookx), T y(e)]]], a10  a book
⇒_{C} [_{a} [_{0} [_{1} F o(λyread)(a, x, bookx)(y), T y(e → t), [_{1} ], [_{0} ]]], a1  ↓
⇒_{C} [_{a} read(a, x, bookx)(John), T y(t), [_{0} ], [_{1} [_{1} ][_{0} ]]], a  ∈ LoF o

Figure 4: Pointed Partial Tree Models arising in the course of parsing “John read a book.” At every transition only the new aspects are highlighted.

THEN ELSE variety. A lexical transitions tests IF the some finite set of formulas (the condition) holds at the Node Description where the pointer is located — this may include the presence (or absence) of labels at that node, modal statements about decorations located at Descriptions related to the pointed one and it may also involve requirements. If the condition holds there, THEN a (sequence of) action(s) is undertaken resulting in a new Tree Description, ELSE (i.e., the condition does not hold) a second action is undertaken, usually an ‘abort’ action.

— A set P of Pragmatic actions. These add information to a Tree Description which is neither contained in the natural language string, nor follows from language specific principles. These are actions of two sorts, (i) substitution processes which “enrich” aspects of the tree structure description as it is projected, primarily by processes of substitution replacing some lexical

A configuration is now a pair

(T n, s)

of a Pointed Partial Tree T n and a string s of lexical actions, i.e., s ∈ L^{∗}. The basic rewrite relation of our parsing model is the binary relation on configurations,

(T n, s) ⇒_{LCP} (T′n′, s′)

defined by, either s = αs′ for α ∈ L and α(T n) = T′n′, or s = s′ and there is some rule ρ ∈ C ∪ P such that ρ(T n) = T′n′.

As usual we let ⇒^{∗} be the reflexive and transitive closure of ⇒.

Definition 10 (Grammatical Strings) The set of grammatical strings, given C, L and P, can be defined as: L(L, C, P) = {s ∈ L^{∗} | ∃T n ∈ Goal : (AXIOM, s) ⇒_{LCP}^{∗} (T n, e)}. A natural language must be able to project any logical form in our representation language. That is, language L(C, L, P) is expressively adequate (EA) if for every T n ∈ Goal there is a s ∈ L^{∗}: (AXIOM, s) ⇒_{LCP}^{∗} (T n, e).

The progress from Axiom to Goal is non-deterministic: at every state of the parse the word currently under consideration can generally be assigned more than one structural role in the Tree Description. That is, the path from Axiom to Goal is one through a space of alternative parse courses. For instance, an

[_{a} ?T y(t)], a  Axiom
⇒_{C} [_{a} ?T y(t), [_{∗} ?T y(e)]], a∗  ↓
⇒_{LC} [_{a} ?T y(t), [_{∗} (a, x, bookx), T y(e)]], a  a book
⇒_{C} [_{a} [_{0} ?T y(e)], [_{1} ], [_{∗} ]], a0  ↓
⇒_{L} [_{a} [_{0} , F o(John), T y(e)], [_{1} ?T y(e → t)], [_{∗} ]], a1  John
⇒_{L} [_{a} [_{0} ], [_{1} [_{1} F o(λxλyread(x)(y)), T y(e → (e → t))], [_{0} ?T y(e)]][_{∗} ]], a10 read
⇒_{C} [_{a}[_{0} ], [_{1}[_{1} ], [_{0} F o(a, x, bookx), T y(e)]]], a10  ∗ := 10
⇒_{C} [_{a} [_{0} [_{1} F o(λyread)(a, x, bookx)(y), T y(e → t), [_{1} ], [_{0} ]]], a1  ↓
⇒_{C} [_{a} read(a, x, bookx)(John), T y(t), [_{0} ], [_{1} [_{1} ][_{0} ]]], a  ∈ LoF o

Figure 5: Pointed Partial Tree Models arising in the course of parsing “A book John read.” At every transition only the new aspects are highlighted.

NP heading an NL string may end up as subject John read a book, it may be a fronted object, A book John read, or it may be a topic constituent, (As for) a book John read it. The first two possibilities are worked out in Figures 4 and 5 respectively. Notice that parse of “John read a book” and “A book John read” end with the same logical form, but this form is reached starting from the Axiom along different routes. Thus the Axiom must be able to access a (finite!) number of alternative partial Tree Descriptions to accommodate the first NP of the sentence.

5 Conclusion

In papers and books cited in the references (especially the forthcoming [1999b]) applications of this model are found involving a wide variety of linguistic phenomena in a number of languages. Of course, the main difference between the approach to parsing suggested by the model in this paper and the more familiar approaches based on a Montagovian framework is the absence of a syntactic algebra and thus of a homomorphic relation between syntactic and semantic structure. A natural language string is seen as a sequence of PDL programs and any syntactic structure in this sequence derives from processing constraints: a word occurring in an NL string leaves the parser with a given partially constructed logical form together with a pointer; the syntactic correctness of a subsequent word then comes down to whether or not the current logical form satisfies the condition of that word.

References

[1994] P. Blackburn & W. Meyer Viol 1994, Linguistics, logic and finite trees, Bulletin of IGPL.

[1996] Kempson, R., W Meyer Viol and D. Gabbay: Language Understanding: a Procedural Perspective, in C. Retore (ed.), Logical Aspects of Computational Linguistics, First International Conference, LACL 1996,228–247. Lecture Notes in Computer Science Vol 1328, Springer Verlag.

[1997] Meyer Viol, W., R. Kibble, R. Kempson and D. Gabbay (1997) ‘Indefinites as Epsilon Terms: A Labelled Deduction Account,’ in H. Bunt and R. Muskens (eds.) Computing Meaning: Current Issues in Computational Semantics. Kluwer Academic Publishers. Dordrecht and Boston.

[1999a] Kempson, R., W Meyer Viol and D. Gabbay, VP-ellipsis: towards a dynamic structural account. In S. Lappin, E. Benmamoun, 1999, Fragments: studies in ellipsis and gapping, OUP.

[1998] [5] Kempson, R., and Meyer Viol, W., Topic and Focus Structures: the Dynamics of Tree Growth, in Proceedings of the 4d Formal Grammar Conference, Saarbruecken, 1998.

[1999b] Kempson, R. Meyer-Viol, W. and Gabbay, D. Dynamic Syntax. Blackwell’s, Oxford, 1999.