Bericht Nr. 81, Dezember 1996

ISSN 0947-6954/96

Arbeitspapiere des Sonderforschungsbereichs 340

Sprachtheoretische Grundlagen für die Computer linguistik

Laura Kallmeyer :

Underspecification in Tree Description Grammars

Universität Stuttgart Universität Tübingen Deutschland Informationssysteme GmbH Arbeitspapiere des SFB 340

Bericht Nr. 81, Dezember 1996

UNDERSPECIFICATION IN TREE DESCRIPTION GRAMMARS

LAURA KALLMEYER

Abstract. In this article Tree Description Grammars (TDG) are presented, a constraint based extension of Tree Adjoining Grammars (TAG). The idea to define TAGs or similar tree grammars in a constraint based way comes from Vijay-Shanker (1992). One of the advantages of using tree descriptions instead of trees in a grammar is the possiblility of underspecification. In a TDG for certain ambiguities there can be underspecified descriptions in the style of the underspecified representations Muskens derives in Muskens (1995) for quantifier scope ambiguities. In principle the idea of TDGs is the following: The grammar consists of a set of tree descriptions, i.e. formulas in some first order logic, and the grammar is derivation based. Every derivation step is a conjunction of two formulas and additional equivalences of node names. The formalism of Tree Description Grammars was introduced in Kallmeyer (1996). Here the definitions of TDGs and related notions (e.g. the derivation mode, the language etc.) are repeated. Some definitions will be slightly different from those in Kallmeyer (1996). The main focus will be on the formal properties of TDGs. I will show the decidability of lexicalized TDGs and the fact that the languages of TDGs are a true superset of tree adjoining languages.

1. Introduction

A lot of attention has been paid to underspecification recently, mainly to underspecified semantic representations. There are two reasons for replacing several analyses of a single expression by one underspecified analysis. The more practical reason is the desire to avoid combinatorial explosion. This so-called “combinatorial explosion puzzle” really can be a problem. To get an idea of the number of readings available for a single

To appear in: Kolb, H.-P. & U. Mönnich (eds.), The Mathematics of Syntactic Structure.

ISSN 0947-6954/96 \begin{matrix}c \\ ◯ \end{matrix}1996 Die Autorin

expression consider the following two examples from Poesio (1996):

(1) We should move the engine at Avon, engine E1, to Dansville to pick up the boxcar there, then move it from Dansville to Corning, load some oranges, and then move it on to Bath.

(2) A politician can fool most voters on most issues most of the time, but no politician can fool all voters on every single issue all of the time.

Poesio points out that in (1) the alternative analyses probably number in the hundreds and that (2) has at least 14400 readings. The second reason for exploring underspecification is psychological plausibility. From a cognitive point of view it does not seem plausible that we process sententences by first generating all readings and then testing them. It appears more cognitively adequate to allow for underspecified representations. To give an idea of what underspecified tree descriptions look like, Fig. 1 shows a descriptions for the two syntactic analyses for minimal modifier ambiguities as in ancienne maison bleue in French. (All examples in this paper are French examples.)

Besides underspecification there are some other advantages of using grammars consisting of tree descriptions instead of the more traditional Tree Adjoining Grammars. As pointed out by Rambow, Vijay-Shanker and Weir 1995, one of the defficencies of TAGs is the way complement clauses are treated. Only for technical reasons they must be analized differently than other arguments. Rambow, Vijay-Shanker and Weir propose D-Tree Grammars where the substitution operation of TAGs is replaced by subsertion. In D-Tree Grammars all arguments including complement clauses are added by subsertion, i.e. they are treated in a uniform way. In TDGs subsertion-like derivation steps are possible as well, so arguments also can be treated uniformly.

Other problems with TAGs arise for phenomena where it is necessary to add several trees in one derivation step. Becker, Joshi and Rambow 1991 show that this is the case for scrambling in German. To deal with this multicomponent TAGs (MCTAG, cf. Joshi (1987)) have been proposed. Shieber and Schabes 1990 use MCTAGs to treat quantifiers. As it is possible to describe several subtrees of one tree in one description without specifying linear precedence between these subtrees, TDGs also

the two syntactic structures of ancienne maison bleue

[figure: ancienne; A; AP; N; N; maison; bleue; A; AP; N; N; ancienne; A; AP; N; N; maison; bleue; A; AP; N; N]

an underspecified tree description describing these two structures as minimal trees:

[figure: ancienne; A; AP; N; N; N; maison; N; bleue; A; AP; N; N]

Figure 1. syntactic underspecification: ancienne maison bleue

offer the advantages of MCTAGs.

In this article I will first present the tree logic used in TDGs, a simple quantifier-free first order logic mainly based on Rogers (1994b). Using this logic the TDG formalism will be introduced and some formal properties of TDGs will be proved. In the end I will give some examples to show that underspecification and subsertion-like derivation steps are possible in TDGs.

2. Tree descriptions

2.1. Logic. A TDG consists of tree descriptions, i.e. constraints for finite labelled trees. In these trees internal nodes are labelled by finite feature structures and leaves by terminal symbols. The logic of tree descriptions used for TDGs is a quantifier-free first order logic. It is similar to the logic Rogers proposes in chapter 3 of his dissertation Rogers (1994b) for feature structure based TAGs (FTAGs, see Vijayashanker (1987), Vijay-Shanker (1992) and Vijay-Shanker and Joshi (1988)).

Definition 1. (Syntax) Let A be a set of attribute names, V a set of attribute values and T a set of terminals such that A, V and T are pairwise disjoint finite sets. Formulas (for A, V and T) are then words over the alphabet of the following symbols:

- the symbols of V ∪ A ∪ T ∪ {ϵ, ⊥}

- a nonempty countable set K of variables called node names,

- constants ⊲, ⊲^{∗}, ≺, ≈ (for binary relations) and δ (for the labeling function),

- logical connectives ∧, ∨, ¬

- bracket symbols (, ). Formulas are inductively defined:

1. Terms:

(a) Each x ∈ T ∪{ϵ} and each δ(k) for all k ∈ K is a l-term (denoting labels).

(b) Each x ∈ V ∪ {⊥} and each a(δ(k)) for all a ∈ A and k ∈ K is a v-term (denoting attribute values).

(c) All k ∈ K are n-terms (denoting nodes).

2. Formulas:

(a) For all τ_{1}, τ_{2}, that are either both l-terms or both v-terms or both n-terms, τ_{1} ≈ τ_{2} is a formula.

(b) For alle n-terms k_{1}, k_{2}: k_{1}⊲k_{2}, k_{1}⊲^{∗}k_{2} and k_{1} ≺ k_{2} are formulas.

(c) If ϕ is a formula, then ¬ϕ also is a formula.

(d) If ϕ, ψ are formulas, then (ϕ ∧ ψ) and (ϕ ∨ ψ) are also formulas. Formulas containing at most one negation and no other logical con-

nective are called elementary formulas. node(ϕ) is the set of all node names occuring in a formula ϕ.

If the order of logical connectives does not matter or if there is only one possible order, brackets will be sometimes omitted.

2.2. Intended models. The set of intended models is restricted to finite labelled trees. Such a tree consists of a set of nodes structured by binary relations parent, dominance and linear precedence. Each leaf is labelled by a terminal symbol or the empty word and each internal node by a finite atomic feature structure.

Definition 2. (Finite labelled trees) A finite labelled tree is a tuple (U, u_{0}, P, P^{∗}, L, μ, N, T) such that 1. N, T are disjoint finite nonempty sets, the nonterminals and termi-

nals.

2. U is a finite nonempty set, the set of nodes, with U ∩ (N ∪ T) = ∅.

3. u_{0} ∈ U is a special node, the root.

4. P, L, P^{∗}, ∈ U × U, such that for all w, x, y, z ∈ U:

(a) (u_{0}, x) ∈ P^{∗}

(b) P^{∗} is the reflexive transitive closure of P.

(c) (x, y) ∈ P^{∗} or (y, x) ∈ P^{∗} or (x, y) ∈ L or (y, x) ∈ L

(d) (x, y) ∈ L ⇒ (x, y) ∉ P^{∗} and (y, x) ∉ P^{∗}

(e) x ≠ u_{0} ⇒ there is exactly one v ∈ U mit (v, x) ∈ P

(f) (x, y) ∈ L and (x, w), (y, z) ∈ P^{∗} ⇒ (w, z) ∈ L

(g) P irreflexive, asymmetric and intransitive

(h) L irreflexive, asymmetric and transitive

5. μ : U → T ∪ N ∪ {ϵ} is a function, such that for all u ∈ U: μ(u) ∈ T ∪ {ϵ} iff there is no u′ ∈ U with (u, u′) ∈ P (u is a leaf).

Definition 3. (Finite atomic feature structures) A set of finite atomic feature structures N_{A,V} consists of sets N, A (attriutes) and V (attribute values), such that

1. N and V are finite sets, N ∩ V = ∅.

2. A is a finite set of pairs ⟨a, α_{a}⟩, where α_{a} is a partial function from N to V and a is the unique name of α_{a}.

2.3. Semantics. The notion of satisfiability in this logic is the same as in ordinary predicate logic. Satisfiability of a formula in a certain model is considered with respect to a node assignment function assigning nodes to all node names.

Definition 4. (Satisfiability) Let B = (U, u_{0}, P, P^{∗}, L, μ, N_{A,V} , T) be a finite tree labelled with finite atomic feature structures N_{A,V} as nonterminals and terminals T. g : K → U is a function, the node assignment function. ϕ, ϕ_{1} and ϕ_{2} are formulas with attribute names {a; there is a partial function α_{a} such that ⟨a, α_{a}⟩ ∈ A}, attribute values V and terminals T. B satisfies ϕ wrt g, B ⊧_{g} ϕ is inductively defined:

1. For all k_{1}, k_{2} ∈ K:

- B ⊧_{g} k_{1} ⊲ k_{2} iff (g(k_{1}), g(k_{2})) ∈ P

- B ⊧_{g} k_{1} ⊲^{∗} k_{2} iff (g(k_{1}), g(k_{2})) ∈ P^{∗}

- B ⊧_{g} k_{1} ≺ k_{2} iff (g(k_{1}), g(k_{2})) ∈ L

- B ⊧_{g} k_{1} ≈ k_{2} iff g(k_{1}) = g(k_{2})

2. For all l-terms l_{1}, l_{2}:

B ⊧_{g} l_{1} ≈ l_{2} iff [[l_{1}]]_{g} = [[l_{2}]]_{g} where

- [[δ(k)]]_{g} = μ(g(k)) for all k ∈ K,

- [[x]]_{g} = x for all x ∈ T ∪ {ϵ}.

3. For all v-terms v_{1}, v_{2}:

B ⊧_{g} v_{1} ≈ v_{2} iff [[v_{1}]]_{g} = [[v_{2}]]_{g} where

- for all k ∈ K: [[a(δ(k))]]_{g} = α_{a}(μ(g(k))), if ⟨a, α_{a}⟩ ∈ A and if α_{a}(μ(g(k))) is defined, else [[a(δ(k))]]_{g} = ⊥.

- [[v]]_{g} = v for all v ∈ V ∪ {⊥}.

4. B ⊧_{g} (ϕ_{1} ∧ ϕ_{2}) iff B ⊧_{g} ϕ_{1} and B ⊧_{g} ϕ_{2}.

5. B ⊧_{g} (ϕ_{1} ∨ ϕ_{2}) iff B ⊧_{g} ϕ_{1} or B ⊧_{g} ϕ_{2}.

6. B ⊧_{g} ¬ϕ_{1} iff not B ⊧_{g} ϕ_{1}. B ⊧ ϕ iff there is an assignment function g, such that B ⊧_{g} ϕ. ϕ_{1} ⊧ ϕ_{2} iff for all trees B and all assignments g: B ⊧_{g} ϕ_{1} ⇒ B ⊧_{I} ϕ_{2}.

3. Properties of the tree logic

In this section I will define some syntactic equivalent for the semantic consequence relation “⊧”. This can be done by using inference rules as proposed by Rogers. The idea is that starting from a formula ψ by applying inference rules it is possible to construct a conjunctive normal form of all the consequences of ψ. A syntactic notion of consequence can then be defined by comparing two such conjunctive normal forms of consequences (see Kallmeyer (1996)). The syntactic consequence defined in this way is decidable, sound and even complete as will be shown below.

3.1. Syntactic consequence. Instead of conjunctions of disjunctions of formulas we will deal with sets of sets of formulas and interprete the whole set (branch) conjunctively and the elements (clauses) disjunctively. This is only a different notation which is used in order to see more clearly how inference rules work.

Definition 5. (clause and branch)

1. A clause is a set Φ of formulas . B ⊧_{g} Φ iff there is a ϕ ∈ Φ such that B ⊧_{g} ϕ. Notation: [Φ]

2. A branch is a set Γ of clauses. B ⊧_{g} Γ iff B ⊧_{g} Φ for all Φ ∈ Γ. Notation: ∥Γ∥.

This definition does not exclude infinite disjunctions or conjunctions. But for our purposes we only need finite clauses and branches.

Before introducing the inference rules a general definition of the syntax and semantics of inference rules must be given.

Definition 6. (inference rule)

1. Syntax: Let V_{Γ} := {Γ_{1}, Γ_{2}, ⋯ }, V_{Φ} := {Φ_{1}, Φ_{2}, ⋯ } and V_{ϕ} := {ϕ_{1}, ϕ_{2}, ⋯ } be pairwise disjoint countable sets.

(i) A branch schema can be inductively defined:

(a) All ψ_{1} ∈ V_{ϕ} are formula schemata, and for all formula schemata ψ_{1} and ψ_{2}: ¬ψ_{1}, (ψ_{1}∧ψ_{2}) and (ψ_{1}∨ψ_{2}) are formula schemata.

(b) Each formula schema and each Ψ ∈ V_{Φ} is a clause schema, and for all clause schemata Ψ_{1}, Ψ_{2}: Ψ_{1}, Ψ_{2} is a clause schema.

(c) For each clause schema Ψ, [Ψ] is a branch schema, each Γ ∈ V_{Φ} is a branch schema, and for all branch schemata Γ_{1}, Γ_{2}: Γ_{1}, Γ_{2} is a branch schema.

(ii) An inference rule \frac{Γ_{old}}{Γ_{new}} ⟨name⟩ consists of two branch schemata Γ_{old} and Γ_{new} such that all x ∈ V_{Γ} ∪ V_{Φ} ∪ V_{ϕ} occuring in Γ_{new} occur as well in Γ_{old}. ⟨name⟩ is the name of the rule.

2. Semantics: Let Γ be a branch.

(i) Γ satisfies a branch schema Γ_{s}, if there is a function f such that - f(Γ_{i}) is a branch for all Γ_{i} ∈ V_{Γ}, f(Ψ_{i}) is a clause for all

Ψ_{i} ∈ V_{Ψ} and f(ψ_{i}) is a formula for all ψ_{i} ∈ V_{ϕ}.

- f(¬a) = ¬f(a), f((a ∧ b)) = (f(a) ∧ f(b)) and f((a ∨ b)) = (f(a) ∨ f(b)) for all formula schemata a and b.

- f([a]) = {f(a)} for all clause schemata a.

- f(a, b) = f(a) ∪ f(b) for all clause or branch schemata a, b - f(Γ_{s}) = Γ.

(ii) A rule \frac{Γ_{old}}{Γ_{new}} ⟨name⟩ can be applied to Γ, if there is a function f such that Γ satisfies Γ_{old} wrt f. The result of the application is f(Γ_{new}).

The following inference rules in principle correspond to those proposed by Rogers (1994b). The logical and structural rules and res are exactly as in Rogers (1994b) and the tree axiom rules are similar to those in Rogers (1994b). Only node symbol rules do not figure there because Rogers does not consider labelled trees.

8 LAURA KALLMEYER

Definition 7. (inference rules for the tree logic) The inference rules for our tree logic are the following:

1. Logical rules (elimination of logical connectives)

\frac{Γ, [Φ, ¬¬ϕ]}{Γ, [Φ, ϕ]}¬¬ \frac{Γ, [Φ, (ϕ ∨ ψ)]}{Γ, [Φ, ϕ, ψ]} ∨ \frac{Γ, [Φ, ¬(ϕ ∨ ψ)]}{Γ, [Φ, ¬ϕ], [Φ, ¬ψ]}¬∨

\frac{Γ, [Φ, (ϕ ∧ ψ)]}{Γ, [Φ, ϕ], [Φ, ψ]} ∧ \frac{Γ, [Φ, ¬(ϕ ∧ ψ)]}{Γ, [Φ, ¬ϕ, ¬ψ]}¬∧

2. Structural rules taut (elimination of tautologies) and abs (absorbtion

of a clause by a second clause, that implies the first one)

\frac{Γ, [Φ, ϕ, ¬ϕ]}{Γ}taut \frac{Γ, [Φ], [Φ, Ψ]}{Γ, [Φ]}abs

3. Resolution res

\frac{Γ, [Φ, ϕ], [Ψ, ¬ϕ]}{Γ, [Φ, ϕ], [Ψ, ¬ϕ], [Φ, Ψ]}res

4. Tree axiom rules: For all k_{1}, k_{2}, k_{3}, k_{4} ∈ K:

Properties of P, P^{∗}, L and = ({(u, u); u ∈ U}):

\frac{Γ}{Γ, [¬k_{1} ≈ k_{2}, ¬k_{2} ≈ k_{3}, k_{1} ≈ k_{3}]}tr_{=} \frac{Γ}{Γ, [¬k_{1} ≈ k_{2}, k_{2} ≈ k_{1}]}sy_{=}

\frac{Γ}{Γ, [k_{1} ≈ k_{1}]}rf_{=} \frac{Γ}{Γ, [¬k_{1} ⊲^{∗} k_{2}, ¬k_{2} ⊲^{∗} k_{3}, k_{1} ⊲^{∗} k_{3}]}tr_{P^{∗}}

\frac{Γ}{Γ, [¬k_{1} ≈ k_{2}, k_{1} ⊲^{∗} k_{2}]}rf_{P^{∗}} \frac{Γ}{Γ, [¬k_{1} ⊲^{∗} k_{2}, ¬k_{2} ⊲^{∗} k_{1}, k_{1} ≈ k_{2}]}antis_{P^{∗}}

\frac{Γ}{Γ, [¬k_{1} ⊲ k_{2}, ¬k_{2} ≈ k_{1}]}irrf_{P} \frac{Γ}{Γ, [¬k_{1} ⊲ k_{2}, ¬k_{2} ⊲ k_{3}, ¬k_{1} ⊲ k_{3}]}intr_{P}

\frac{Γ}{Γ, [¬k_{1} ≺ k_{2}, ¬k_{1} ≈ k_{2}]}irrf_{L} \frac{Γ}{Γ, [¬k_{1} ≺ k_{2}, ¬k_{2} ≺ k_{3}, k_{1} ≺ k_{3}]}tr_{L}

Relations between L, P and P^{∗}:

\frac{Γ}{Γ, [¬k_{1} ⊲ k_{2}, k_{1} ⊲^{∗} k_{2}]}T_{1} \frac{Γ}{Γ, [k_{1} ⊲^{∗} k_{2}, k_{2} ⊲^{∗} k_{1}, k_{1} ≺ k_{2}, k_{2} ≺ k_{1}]}T_{2}

\frac{Γ}{Γ, [¬k_{1} ⊲^{∗} k_{2}, ¬k_{1} ≺ k_{2}], [¬k_{2} ⊲^{∗} k_{1}, ¬k_{1} ≺ k_{2}]}T_{3}

\frac{Γ}{Γ, [¬k_{1} ⊲ k_{2}, ¬k_{3} ⊲ k_{2}, k_{1} ≈ k_{3}]}T_{4}

\frac{Γ}{Γ, [¬k_{1} ≺ k_{2}, ¬k_{1} ⊲^{∗} k_{3}, ¬k_{2} ⊲^{∗} k_{4}, k_{3} ≺ k_{4}]}T_{5}

5. Node symbol rules: Let T = {t_{1}, ⋯, t_{n}} be the terminals, A = {a_{1}, ⋯ a_{m}} the attribute names and V = {v_{1}, ⋯, v_{l}} the attribute values. For all k, k_{1}, k_{2} ∈ K:

Nonterminal labels for all internal nodes:

\frac{Γ}{Γ, [¬k_{1} ⊲ k_{2}, ¬δ(k_{1}) ≈ t_{1}], ⋯, [¬k_{1} ⊲ k_{2}, ¬δ(k_{1}) ≈ t_{n}]}μ(u)

Uniqueness of μ:

\frac{Γ}{Γ, [¬k_{1} ≈ k_{2}, δ(k_{1}) ≈ δ(k_{2})]}unique_{μ}

Uniqueness of the attribute functions: for all attribute names a:

\frac{Γ}{Γ, [¬k_{1} ≈ k_{2}, a(δ(k_{1})) ≈ a(δ(k_{2}))]}attr_{1}

Attribute functions undefined for terminals: for all t ∈ T and a ∈ A:

\frac{Γ}{Γ, [¬δ(k_{1}) ≈ t, a(δ(k_{1})) ≈ ⊥]}attr_{2}

Attribute values in V or undefined: for all a ∈ A:

\frac{Γ}{Γ, [a(δ(k)) ≈ v_{1}, ⋯, a(δ(k)) ≈ v_{l}, a(δ(k)) ≈ ⊥]}attr_{3}

Proposition 1. (Model invariance) If Γ_{2} can be constructed from Γ_{1} in finitely many steps by applying inference rules, then:

⋀_{Φ_{1}∈Γ_{1}} ⋁_{ϕ_{1}∈Φ_{1}} ⊧ ⋀_{Φ_{2}∈Γ_{2}} ⋁_{ϕ_{2}∈Φ_{2}} and ⋀_{Φ_{1}∈Γ_{1}} ⋁_{ϕ_{1}∈Φ_{1}} ⊧ ⋀_{Φ_{2}∈Γ_{2}} ⋁_{ϕ_{2}∈Φ_{2}}

This can be shown by induction on the number of rule applications.

The following definition is again taken from Rogers (1994b):

Definition 8. (Saturated, open, closed and satisfiable branches)

1. A branch Γ is saturated, if:

- No logical rule can be applied to Γ.

- Neither abs nor taut can be applied to Γ.

- For all applications of res to Γ the new clause introduced by this application can be removed by abs or taut.

- For all applications of tree axiom or node symbol rules with node names occuring in Γ the resulting new clauses can be removed by abs.

2. A branch is closed, if it contains an empty clause.

3. A branch is open, if it is not closed.

4. A branch Γ is satisfiable, if there is a tree B and a node assignment function g such that B ⊧_{g} Γ.

Proposition 2. Let ψ be a formula with attribute names A, values V and terminals T and Υ ⊆ K a finite set such that node(ψ) ⊆ Υ. In finitely many steps a unique saturated branch Γ can be constructed for ψ and Υ, such that

ψ ⊧ ⋀_{Φ∈Γ} ⋁_{ϕ∈Φ} and ⋀_{Φ∈Γ} ⋁_{ϕ∈Φ} ⊧ ψ

Notation: Γ(ψ) is the saturated branch for ψ (wrt to a given set Υ). If it does not matter which set Υ was used, we simply write “Γ(ψ)”.

Prop. 2 can be proved by first giving an algorithm for constructing Γ(ψ) for a given ψ and then showing that the result has the properties mentioned in the proposition. The construction is very similar to the one proposed in Prop. 5 in Rogers (1994b).

Proof: Construction: Γ_{1} := ∥[ψ]∥

1. Apply each tree axiom and each node symbol rule with symbols from A, V and T and node names from Υ once to Γ_{1}. The result is called Γ_{2}.

2. Apply the logical rules as often as possible to Γ_{2}. The result is called Γ_{3}.

3. Apply res repeatedly to Γ_{3}, as long as new clauses can be added by res. The result is called Γ_{4}.

4. Apply the structural rules as often as possible to Γ_{4}. The result is Γ. (The order of the first two steps is of no importance because neither tree axiom rules nor node symbol rules add any logical connectives.)

To show: The construction terminates after finitely many steps and the result is a saturated branch Γ, such that B ⊧_{g} ψ iff B ⊧_{g} Γ.

(i) Construction terminates after finitely many steps, i.e. each of the four parts 1. to 4. only consists of a finite number of rule applications:

(a) 1. part: There are only finitely many rules with node names from Υ and symbols from A, V and T that are applied to Γ_{1}.

(b) 2. part: There is only a finite number of applications of logical rules to Γ_{2} because Γ_{2} is finite and each logical rule removes some logical connective.

(c) 3. part: Each application of res in 3. adds a new clause. But the number of possible clauses containing elementary formulas with node names from Υ and symbols from A, V and T is finite: There are only finitely many elementary formulas, that can occur as elements of a clause. If n is the number of possible elementary formulas, then there are 2^{n} possible clauses and consequently at most 2^{n} applications of res in 3.

(d) 4. part: Each structural rule removes a clause. Consequently only

finitely many applications of taut and abs are possible. (ii) Γ is saturated:

(a) No logical rule can be applied to Γ because no logical connectives are added in 2., 3. or 4.

(b) Because of the 4. part no structural rules can be applied to Γ.

(c) Because of Γ ⊆ Γ_{4} all applications of res, that are possible in Γ have already been done in 3. Each additional application of res either does not change anything or adds a clause that can be removed by taut or abs.

(d) In the beginning all tree axiom rules and all node symbol rules with names from Υ have been applied. The clauses added by these rules are no tautologies and contain only elementary formulas. Because of this they have not been removed by taut or by a logical rule. Perhaps they have been diminished by abs. Consequently for each result ∥Γ, Φ_{1}, Φ_{2} ⋯ ∥ of an application of a tree axiom rule or a node symbol rule to ∥Γ∥: For each new clause Φ_{i} there is a clause Ψ_{i} in Γ with Ψ_{i} ⊆ Φ_{i}, i.e. Φ_{i} can be eliminated by abs.

(iii) Model invariance: Holds because of ψ = ⋀_{Φ∈∥[ψ]∥} ⋁_{ϕ∈Φ} and Prop. 1.

□

Closed branches are not satisfiable. This means that a necessary condition for the satisfiability of a formula ϕ is, that Γ(ϕ) must be open. We will see that this is even sufficient, i.e. that if Γ(ϕ) is open, then ϕ is satisfiable.

By comparing the saturated branches Γ(ϕ_{1}) and Γ(ϕ_{2}) of two formulas ϕ_{1} and ϕ_{2} a syntactic notion of consequence ϕ_{1} ⊢ ϕ_{2} can be defined:

Definition 9. (Syntactic consequence ϕ_{1} ⊢ ϕ_{2}) Let ϕ_{1} and ϕ_{2} be formulas, Γ_{1} and Γ_{2} the corresponding saturated branches with node names from node(ϕ_{1}) ∪ node(ϕ_{2}). ϕ_{1} ⊢ ϕ_{2} iff for all Ψ_{2} ∈ Γ_{2} there is a Ψ_{1} ∈ Γ_{1}, such that Ψ_{1} ⊆ Ψ_{2}.

⊢ is transitive and because of Prop. 2 it is also decidable.

3.2. Soundness and Completeness. If ϕ_{1} ⊢ ϕ_{2}, then for all trees B and all node assignment functions g: If B ⊧_{g} ϕ_{1}, then B ⊧_{g} ϕ_{2}. This immediately follows from Def. 9 together with Prop. 2 and Def. 5. Consequently the following holds:

Proposition 3. (Soundness) For all ϕ_{1}, ϕ_{2}: If ϕ_{1} ⊢ ϕ_{2}, then ϕ_{1} ⊧ ϕ_{2}.

In order to prove completeness we first need the following proposition:

Proposition 4. (Satisfiability of open saturated branches) For all formulas ψ and all Γ = Γ(ψ): Γ is open iff Γ is satisfiable (iff ψ is satisfiable).

Proof: We only have to show, that: Γ open ⇒ ψ satisfiable. Let Γ = Γ(ψ) be open, Γ is constructed wrt a set Υ of node names.

(i) First we will extend Γ to a branch Γ′, such that for all k_{1}, k_{2} ∈ Υ:

[k_{1} ≺ k_{2}] ∈ Γ′ or [¬k_{1} ≺ k_{2}] ∈ Γ′, [k_{1} ⊲ k_{2}] ∈ Γ′ or [¬k_{1} ⊲ k_{2}] ∈ Γ′, [k_{1} ⊲^{∗} k_{2}] ∈ Γ′ or [¬k_{1} ⊲^{∗} k_{2}] ∈ Γ′ and [k_{1} ≈ k_{2}] ∈ Γ′ or [¬k_{1} ≈ k_{2}] ∈ Γ′. This means that Γ′ must be completely specified wrt ≺, ⊲, ⊲^{∗}, ≈ (in general Γ′ is not unique).

Construction:

Γ_{0} := Γ ∪ {[k_{1} r k_{2}, ¬k_{1} r k_{2}]| r ∈ {≺, ⊲, ⊲^{∗}, ≈}, k_{1}, k_{2} ∈ Υ}.

Γ′ := Γ_{0}. Apply first res (as long as no tautology is introduced) and then abs as often as possible to Γ′ (only finitely many applications). (*): If |[Φ]| = 1 for all [Φ] ∈ Γ′, then the construction is terminated.

Else: Choose one [Φ] ∈ Γ′, such that |[Φ]| > 1, and then choose one ϕ ∈ Φ. Γ′′ := Γ′ ∪ {[ϕ]}. Apply res as often as possible to Γ′′, as long as res does not introduce any tautologies (these applications of res add only subsets of clauses that are already in Γ′′). Apply then abs as often as possible to Γ′′ (this only removes clauses that are supersets of [ϕ] or of the clauses just added by res). Let Γ′ be the resulting branch. Continue with (*). The construction terminates after finitely many steps because no

new clauses are introduced and in each step at least one [Φ] is diminished.

No clause is completely removed. Consequently for each tautology added to Γ in the beginning a subset containing one formula is in Γ′.

(ii) To show: Γ′ is saturated. - No logical rule can be applied to Γ.

- res and abs have been applied as often as possible.

- taut cannot be applied to Γ′ because |Φ| = 1 for all Φ ∈ Γ′.

- Γ ⊆ Γ_{0} and for all Ψ ∈ Γ_{0} there is a Φ ∈ Γ′, such that Φ ⊆ Ψ. ⇒ for all Ψ ∈ Γ there is a Φ ∈ Γ′′, such that Φ ⊆ Ψ. This means that all clauses, that can be added to Γ′ by tree axiom rules or node symbol rules, can be removed by abs, and that for all trees B and all node assignments g: B ⊧_{g} Γ′ ⇒ B ⊧_{g} Γ. Rogers (1994b) shows that for each saturated branch that is com-

pletely specified wrt ⊲, ⊲^{∗}, ≺ and ≈ in the way described above, there is a tree satisfying that branch. Consequently Γ′ (and also Γ) is satisfiable.

□

With this proposition completeness can be shown:

Proposition 5. (Completeness) For all ϕ_{1}, ϕ_{2}: If ϕ_{1} ⊧ ϕ_{2}, then ϕ_{1} ⊢ ϕ_{2}.

As a first part of the completeness proof we will show the following lemma:

Lemma. For all ϕ = ψ_{1} ∨⋯ ψ_{n−1} and ψ_{n}, such that ψ_{i} is an elementary formula for 1 ≤ i ≤ n: ϕ ⊢ ϕ ∨ ψ_{n}.

Proof of the lemma: Let Γ = Γ(ϕ) and Γ′ = Γ(ϕ ∨ ψ_{n}) be those saturated branches that can be constructed using node names from node(ϕ ∨ ψ_{n}). If ϕ is a tautology, then Γ = Γ′ holds. ⇒ ϕ ⊢ ϕ ∨ ψ_{n} trivially holds. Let ϕ be no tautology. Construction of Γ and Γ′ (here the logical rules will be applied first): ∥[ψ_{1}, ⋯, ψ_{n−1}]∥ and ∥[ψ_{1}, ⋯, ψ_{n−1}, ψ_{n}]∥ are the results of all possible applications of logical rules to ∥[ϕ]∥ and ∥[ϕ ∨ ψ_{n}]∥. Let Γ_{n} be the result of applying n rules to ∥[ψ_{1}, ⋯, ψ_{n−1}, ψ_{n}]∥. Claim: For all Ψ_{n} ∈ Γ_{n}, that cannot be removed by taut, there is a Φ ∈ Γ such that Φ ⊆ Ψ_{n}. Induction on n:

(i) Induction start n = 0: As Γ is constructed from ∥[ψ_{1}, ⋯, ψ_{n−1}]∥ and as taut cannot be applied to any subset of this branch, Γ still contains a subset of [ψ_{1}, ⋯, ψ_{n−1}] (and also of [ψ_{1}, ⋯, ψ_{n−1}, ψ_{n}]).

(ii) Induction step n ⇒ n + 1: Possible rules that can be applied to Γ_{n} to construct Γ_{n+1}:

1. Tree axiom or node symbol rules: Because of saturatedness of Γ the claim still holds.

2. res: Let [Φ, ϕ], [Ψ, ¬ϕ] ∈ Γ_{n}, res adds the clause [Φ, Ψ]. There are [Φ′] ⊆ [Φ, ϕ] and [Ψ′] ⊆ [Ψ, ¬ϕ], such that [Φ′], [Ψ′] ∈ Γ (induction claim).

- 1. case: [Φ′] ⊆ [Φ] or [Ψ′] ⊆ [Ψ] ⇒ [Φ′] ⊆ [Φ, Ψ] or [Ψ′] ⊆ [Φ, Ψ].

- 2. case: [Φ′] = [Φ′′, ϕ] and [Ψ′] = [Ψ′′, ¬ϕ] ⇒ (Γ saturated) there is a subset of [Φ′′, Ψ′′] (and of [Φ, Ψ]) in Γ, or [Φ′′, Ψ′′] (and consequently also [Φ, Ψ]) is a tautology and can be removed by taut.

3. taut and abs only remove clauses, i.e. claim still holds for the

result of applying taut or abs.

□

Proof of Prop. 5: Let ϕ_{1}, ϕ_{2} be formulas, ϕ_{1} ⊧ ϕ_{2}, and let Γ_{1} = Γ(ϕ_{1}), Γ_{2} = Γ(ϕ_{2}) be constructed with Υ = node(ϕ_{1}) ∪ node(ϕ_{2}). Without loss of generality ϕ_{2} is in conjunctive normal form without double negations. If ϕ_{1} is not satisfiable, then Γ_{1} = ∥[ ]∥ and ϕ_{1} ⊢ ϕ_{2} trivially holds. Let ϕ_{1} be satisfiable. Because of ϕ_{1} ⊧ ϕ_{2} ϕ_{2} is then satisfiable as well. To show: ϕ_{1} ⊢ ϕ_{2}. Induction on the structure of ϕ_{2}:

(i) Induction start: Let ϕ_{2} be an elementary formula. Then [ϕ_{2}] ∈ Γ_{2}.

Suppose that [ϕ_{2}] ∉ Γ_{1}. ϕ_{2}^{neg} := ¬ϕ_{2} if ϕ_{2} does not contain negations, ϕ_{2}^{neg} := ϕ′_{2}, if ϕ_{2} = ¬ϕ′_{2}.

⇒ starting from Γ_{1} ∪ {[ϕ_{2}^{neg}]} no closed branch can be constructed by applying res. ⇒ (Prop. 4) ϕ_{1} ∧ ¬ϕ_{2} is satisfiable. Contradiction to ϕ_{1} ⊧ ϕ_{2}. ⇒ [ϕ_{2}] ∈ Γ_{1}. Γ_{1} and Γ_{2} are saturated, and all rule applications, that were done

to construct Γ_{2}, were done as well (with the same instantiation f of the V_{Γ}, V_{Φ} and V_{ϕ}) to construct Γ_{1}.

⇒ ϕ_{1} ⊢ ϕ_{2}. (ii) Induction step for disjunctions: ϕ_{2} = ψ_{1} ∨ψ_{2} ⋯∨ψ_{n} with elementary

formulas ψ_{i}, 1 ≤ i ≤ n.

Because of ϕ_{1} ⊧ ϕ_{2} either ϕ_{1} ⊧ ψ_{1} ∨ ψ_{2} ⋯ ∨ ψ_{n−1} or ϕ_{1} ⊧ ψ_{n} hold.

⇒ (induction claim) ϕ_{1} ⊢ ψ_{1} ∨ ψ_{2} ⋯ ∨ ψ_{n−1} or ϕ_{1} ⊢ ψ_{n}. ψ_{1} ∨ ψ_{2} ⋯ ∨ ψ_{n−1} ⊢ ψ_{1} ∨ ψ_{2} ⋯ ∨ ψ_{n−1} ∨ ψ_{n} (lemma) and ψ_{n} ⊢

ψ_{1} ∨ ψ_{2} ⋯ ∨ ψ_{n−1} ∨ ψ_{n} (transitivity of ⊢).

⇒ (transitivity of ⊢) ϕ_{1} ⊢ ψ_{1} ∨ ψ_{2} ⋯ ∨ ψ_{n−1} ∨ ψ_{n}. (iii) Induction step for conjunctions: ϕ_{2} = ψ_{1} ∧ ψ_{2} ⋯ ∧ ψ_{n} and ϕ_{1} ⊧ ϕ_{2}.

⇒ ϕ_{1} ⊧ ψ_{1} ∧ ⋯ ψ_{n−1} and ϕ_{1} ⊧ ψ_{n}. ⇒ (induction claim) ϕ_{1} ⊢ ψ_{1} ∧ ⋯ ψ_{n−1} and ϕ_{1} ⊢ ψ_{n}. Γ_{n−1} := Γ(ψ_{1} ∧ ⋯ ψ_{n−1}), Γ′ := Γ(ψ_{n}) with node names from

node(ϕ_{1}) ∪ node(ϕ_{2}). For all Ψ ∈ Γ_{n−1} ∪ Γ′ there is a Φ ∈ Γ_{1}, such that Φ ⊆ Ψ (induction claim).

Γ_{2} = Γ(ϕ_{2}) with names from node(ϕ_{1}) ∪ node(ϕ_{2}) can be constructed from Γ_{n−1} ∪ Γ′ by repeatedly applying res, taut and abs. Let Γ_{n,k} be the branch we get after k applications of res, taut and abs to Γ_{n−1} ∪ Γ′.

To show: For all Ψ ∈ Γ_{n,k} there is a Φ ∈ Γ_{1}, such that Φ ⊆ Ψ. Induction on k:

- Induction start k = 0: Claim holds because of ϕ_{1} ⊢ ψ_{1} ∧ ⋯ ψ_{n−1} and ϕ_{1} ⊢ ψ_{n}.

- Induction step k ⇒ k + 1: Possible rule applications:

res: Let res add a clause to Γ_{n,k}, that is no tautology. ⇒ There are [Ψ_{1}, ψ], [Ψ_{2}, ¬ψ] ∈ Γ_{n,k}, such that [Ψ_{1}, Ψ_{2}] ∈ Γ_{n,k+1}. There are subsets Ξ_{1} of [Ψ_{1}, ψ] and Ξ_{2} of [Ψ_{2}, ¬Ψ] in Γ_{1}.

1. case: ψ ∉ Ξ_{1} or ¬ψ ∉ Ξ_{2} ⇒ Ξ_{1} ⊆ [Ψ_{1}, Ψ_{2}] or Ξ_{2} ⊆ [Ψ_{1}, Ψ_{2}].

3. case: Ξ_{1} = [Ψ′_{1}, ψ], Ξ_{2} = [Ψ′_{2}, ¬ψ] ⇒ there is a subset of [Ψ′_{1}, Ψ′_{2}] in Γ_{1} and [Ψ′_{1}, Ψ′_{2}] ⊆ [Ψ_{1}, Ψ_{2}] holds. Structural rules: taut and abs only remove clauses. Consequently ϕ_{1} ⊢ ψ_{1} ∧ ⋯ ψ_{n−1} ∧ ψ_{n} also holds.

□

4. TDG-Formalism

4.1. Grammar. A Tree Description Grammar consists of a set of formulas (more precisely equivalence classes of formulas), that have a certain specific form (see Fig. 2). The idea is that certain subtrees are completely described whereas between these subtrees only dominance relations are known. This is formalized by the notion of “description”. The definition of description given here is more restricted than in Kallmeyer (1996). In contrast to Kallmeyer (1996) negation is not allowed here and disjunction is only allowed for equivalences of l-terms or v-terms.

possible tree descriptions:

[figure: ⋯; ⋯; ⋯; ⋯]

tree description, that should not be allowed:

[figure: or; L not specified for daughters]

Figure 2. tree descriptions in TDGs In the following definition, a few notions will be introduced, that are frequently used in course of the article.

Definition 10. (minimal name, strong dominance, leaf name) Let ϕ be a formula, k, k_{1}, k_{2} ∈ node(ϕ)

1. k is a minimal name in ϕ iff ϕ ⊢ k ⊲^{∗} k′ for all k′ ∈ node(ϕ).

2. k_{1} ⊲^{∗} k_{2} is a strong dominance in ϕ, (ϕ ⊢_{s} k_{1} ⊲^{∗} k_{2}), if (apart from the order of the conjuncts in ϕ) ϕ = ϕ_{1} ∧ k_{1} ⊲^{∗} k_{2} and ϕ_{1} ⊬ k_{1} ⊲^{∗} k_{2} holds.

3. k is a leaf name in ϕ, if for all k′ ∈ node(ϕ): ϕ ⊢ k⊲^{∗}k′ ⇒ ϕ ⊢ k ≈ k′.

Definition 11. (Description) A formula ϕ is called a description, if:

1. ϕ is satisfiable.

2. There is at least one minimal name in ϕ.

3. ϕ does not contain any negations.

4. If ϕ_{d} is a disjunction (ϕ_{1}∨ϕ_{2}) occuring in ϕ, then each of the formulas ϕ_{1} and ϕ_{2} is either a disjunction itself or it is of the form t_{1} ≈ t_{2} where t_{1} and t_{2} are either l-terms or v-terms.

5. For all k_{1}, k_{2}, k_{3} ∈ K: If ϕ ⊢ k_{1}⊲k_{2}∧k_{1}⊲^{∗}k_{3}, then either ϕ ⊢ k_{1} ≈ k_{3} holds or there is a k_{4}, such that ϕ ⊢ k_{1} ⊲ k_{4} ∧ k_{4} ⊲^{∗} k_{3}.

6. For all k_{1}, k_{2}, k_{3} ∈ K: If ϕ ⊢ k_{1} ⊲k_{2} ∧k_{1} ⊲k_{3}, then either ϕ ⊢ k_{2} ≈ k_{3} or ϕ ⊢ k_{2} ≺ k_{3} or ϕ ⊢ k_{3} ≺ k_{2} holds.

The first condition holds iff Γ(ϕ) is open (see Prop. 4), i.e. this condition also can be formulated in a syntactic way. This means especially that the satisfiability of a formula is decidable. Then the question whether a formula is a description or not, is also decidable because of the finiteness of node(ϕ).

It is easy to see that for each description ϕ and each k ∈ node(ϕ):

- k minimal in ϕ or there is a k′ such that ϕ ⊢ k′ ⊲ k or ϕ ⊢_{s} k′ ⊲^{∗} k.

- k leaf name in ϕ or there is a k′ such that ϕ ⊢ k ⊲ k′ or ϕ ⊢_{s} k ⊲^{∗} k′.

The following equivalence relation is necessary to make sure that in each derivation step descriptions with disjoint sets of node names can be chosen.

Definition 12. Let ϕ, ϕ′ be formulas. ϕ ≈_{K} ϕ′ iff ϕ and ϕ′ differ only in a bijection of K.

≈_{K} is an equivalence relation. Let \overline{ϕ} be the equivalence class containing ϕ.

For all trees B and formulas ϕ and ϕ′ with ϕ ≈_{K} ϕ′: B ⊧ ϕ iff B ⊧ ϕ′.

Definition 13. (Tree Description Grammar) A Tree Description Grammar (TDG) is a tuple G = (A, V, T, D, ϕ_{S}), such that:

1. A, V and T are pairwise disjoint finite sets, the attribute names, attribute values and the terminal symbols.

2. D is a finite set of equivalence classes \overline{(ψ, K_{ψ})}, such that for all (ψ, K_{ψ}) ∈ \overline{(ψ, K_{ψ})} ψ is a description (with A, V and T) and K_{ψ} ⊆ node(ψ).

(ψ_{2}, K_{ψ_{2}}) ∈ \overline{(ψ_{1}, K_{ψ_{2}})} iff ψ_{1} ≈_{K} ψ_{2} with a bijection f_{K} : K → K and K_{ψ_{2}} = {k ∈ K| there is a k′ ∈ K_{ψ_{1}} such that k = f_{K}(k′)}.

Each representative of a class in D is called an elementary description.

3. ϕ_{S} is a description (with A, V and T), the start description.

An elementary description ψ is a description with certain marked node names (those in K_{ψ}). These are important for the derivation process.

4.2. Derivation. A derivation starts with the start description ϕ_{S}. In each derivation step the description that is already derived is extended by adding a new elementary description and some additional node name equivalences.

Definition 14. (Derivation mode) Let G = (A, V, T, D, ϕ_{S}) be a TDG, ϕ_{1}, ϕ_{2} descriptions, and (ψ, K_{ψ}) an elementary description in G. Without loss of generality node(ϕ_{1}) and node(ψ) are disjoint (if not, choose an appropriate representative of \overline{(ψ, K_{ψ})}).

1. ϕ_{2} can be derived in one step from ϕ_{1} using (ψ, K_{ψ}) (ϕ_{1} ⇒^{ψ} ϕ_{2} or

ϕ_{1} ⇒^{(ψ,K_{ψ})} ϕ_{2}), if:

(A1) ϕ_{2} ⊢ ϕ_{1} ∧ ψ.

(A2) For all k_{ψ} ∈ node(ψ): There is a k ∈ node(ϕ_{1}) such that ϕ_{2} ⊢

k_{ψ} ≈ k iff k_{ψ} ∈ K_{ψ} or k_{ψ} minimal in ψ. (A3) For all k_{1} ∈ node(ϕ_{1}), k_{2} ∈ node(ψ), such that ϕ_{2} ⊢ k_{1} ≈ k_{2}:

There are no k′_{1} ∈ node(ϕ_{1}), k′_{2} ∈ node(ψ), such that ϕ_{1} ⊢ k_{1}⊲k′_{1} and ψ ⊢ k_{2} ⊲ k′_{2}.

(A4) For all k_{1}, k_{2}, such that ϕ_{2} ⊢ k_{1} ⊲ k_{2}: there are k_{3}, k_{4}, such that

ϕ_{2} ⊢ k_{1} ≈ k_{3} ∧ k_{2} ≈ k_{4} and ϕ_{1} ∧ ψ ⊢ k_{3} ⊲ k_{4}. (A5) For all ϕ_{3} fulfilling (A1) - (A4) the following holds: If ϕ_{2} ⊢ ϕ_{3},

then ϕ_{3} ⊢ ϕ_{2}.

2. ϕ_{2} can be derived in one step from ϕ_{1}, ϕ_{1} ⇒ ϕ_{2}, if there is an elementary description ψ such that ϕ_{1} ⇒^{ψ} ϕ_{2}.

3. ϕ′ can be derived from ϕ (in finitely many steps), ϕ ⇒^{∗} ϕ′, if there are descriptions ϕ_{1}, ⋯ ϕ_{n}, such that ϕ = ϕ_{1} ⇒ ϕ_{2} ⋯ ⇒ ϕ_{n} = ϕ′.

The definition of the derivation mode is slightly different from the one in Kallmeyer (1996). There (A4) does not occur in the definition of derivation, and for names in ψ, that are neither minimal nor marked, equivalent names in the old description are allowed.

A derivation step in TDGs is a conjunction of two descriptions and additional equivalences of node names. According to (A2) exactly for those names in the new elementary description ψ, that are minimal or marked names, there must be names in the old description describing the same nodes (i.e. the two names are equivalent). The marking of names somehow says how to put the two descriptions together. (A3) states that two node names cannot be identified if they both describe internal nodes in completely described subtrees (k_{2} and k_{5} in fig. 4 for example cannot be identified). At least one of them must be a leaf name or on the left side of a strong dominance in the old descriptions. (A4) simply says that in a derivation step no new ⊲ relations can be added. The last condition means that ϕ_{2} must be ”maximally underspecified”.

Proposition 6. If ϕ_{1} ⇒^{(ψ,K_{ψ})} ϕ_{2}, then node(ϕ_{2}) = node(ϕ_{1}) ∪ node(ψ).

Proof:

1. To show: node(ϕ_{1}) ∪ node(ψ) ⊆ node(ϕ_{2}). ϕ_{1} and ψ are descriptions ⇒ there is a k_{r}^{ϕ_{1}} such that ϕ_{1} ⊢ k_{r}^{ϕ_{1}} ⊲^{∗} k_{ϕ_{1}} for all k_{ϕ_{1}} ∈ node(ϕ_{1}),

and there is a k_{r}^{ψ} such that ψ ⊢ k_{r}^{ψ} ⊲^{∗} k_{ψ} for all k_{ψ} ∈ node(ψ).

⇒ (transitivity of ⊢) ϕ_{2} ⊢ k_{r}^{ϕ_{1}} ⊲^{∗} k_{ϕ_{1}} for all k_{ϕ_{1}} ∈ node(ϕ_{1}) and ϕ_{2} ⊢ k_{r}^{ψ} ⊲^{∗} k_{ψ} for all k_{ψ} ∈ node(ψ). ⇒ node(ϕ_{1}) ∪ node(ψ) ⊆ node(ϕ_{2}).

2. To show: node(ϕ_{2}) ⊆ node(ϕ_{1}) ∪ node(ψ).

Suppose there is a k ∈ node(ϕ_{2}) \ (node(ϕ_{1}) ∪ node(ψ)).

(i) 1. case: there is a k′ ∈ node(ϕ_{1}) ∪ node(ψ) such that ϕ_{2} ⊢ k ≈ k′. Let ϕ′_{2} be the description resulting from replacing all occurences of k by k′. (A1) - (A4) hold for ϕ′_{2}, and ϕ_{2} ⊢ ϕ′_{2} and ϕ′_{2} ⊬ ϕ_{2} hold.

Contradiction to (A5). (ii) 2. case: There is no k′ ∈ node(ϕ_{1})∪node(ψ) such that ϕ_{2} ⊢ k ≈ k′,

and there is a k′ ∈ node(ϕ_{2}) such that ϕ_{2} ⊢ k′ ⊲ k or ϕ_{2} ⊢ k ⊲ k′.

[figure: ϕ_{2}:; k; k′; k′; k; or]

Contradiction to (A4). (iii) 3. case: There is no k′ ∈ node(ϕ_{1})∪node(ψ) such that ϕ_{2} ⊢ k ≈ k′.

There is a k_{t} such that ϕ_{2} ⊢_{s} k_{t} ⊲^{∗} k, and k either is a leaf name in ϕ_{2} or there is a k_{b} such that ϕ_{2} ⊢_{s} k ⊲^{∗} k_{b}.

[figure: ϕ_{2}:; k_{b}; k_{t}; k]

ϕ′_{2} is the description resultung from adding all conjuncts k_{1} r k_{2} for r ∈ {⊲^{∗}, ≺} such that ϕ_{2} ⊢ k_{1} r k_{2} and k_{1}, k_{2} ≠ k to ϕ_{2} and by then removing all conjuncts containing an occurence of k. ϕ′_{2} is a description, (A1) - (A4) hold for ϕ′_{2}, and ϕ_{2} ⊢ ϕ′_{2} and ϕ′_{2} ⊬ ϕ_{2} hold. Contradiction to (A5).

(iv) 4. case: There is no k′ ∈ node(ϕ_{1}) ∪ node(ψ) such that ϕ_{2} ⊢ k ≈ k′, and k is minimal in ϕ_{2}: Because of (i)-(iii), for all k′ ∈ node(ϕ_{2}) \ (node(ϕ_{1}) ∪ node(ψ)), ϕ_{2} ⊢ k ≈ k′ holds. ϕ′_{2} is the result of removing all conjuncts with occurences of any element of node(ϕ_{2})\(node(ϕ_{1})∪node(ψ)) from ϕ_{2}. ϕ′_{2} is a description. (A1)

- (A4) hold for ϕ′_{2}, and ϕ_{2} ⊢ ϕ′_{2} and ϕ′_{2} ⊬ ϕ_{2} hold. Contradiction to (A5).

□

The operations substitution and adjunction defined for TAGs can be imitated in TDGs: For a derivation step similar to substitution (see Fig. 3) an elementary description (ψ, K_{ψ}) with K_{ψ} = ∅ must be added. Then only for the minimal names in ψ there are equivalent node names in the old description. For an adjunction-like derivation step (ψ, K_{ψ}) must be such that all marked names are equivalent and they are all leaf names. In the old description ϕ_{1} there must be a strong dominance k_{1} ⊲^{∗} k_{2}. Then a derivation step adding ψ can consist of putting ψ between k_{1} and k_{2}, which is

Additional to the descriptions a graphical representation is given. P (normal edges) and P^{∗} (dotted edges as in fig. 4) are represented.

ϕ_{1} ⇒^{(ψ,K_{ψ})} ϕ_{2} with ϕ_{2} = ϕ_{1} ∧ ψ ∧ k_{2} ≈ k_{6}

[figure: ϕ_{1}; ϕ_{2}; ψ; ^{^{k_{6}}^{k_{7}} Jean NP}; NP; k_{2}; VP; k_{3}; S; k_{1}; V; k_{4}; vient; k_{5}; ^{^{k_{2}≈k_{6}}^{k_{7}} Jean NP}; NP; VP; k_{3}; S; k_{1}; V; k_{4}; vient; k_{5}]
ϕ_{1} = k_{1} ⊲ k_{2} ∧ k_{1} ⊲ k_{3} ∧ k_{2} ≺ k_{3} ∧ k_{3} ⊲ k_{4} ∧ k_{4} ⊲ k_{5}

∧cat(δ(k_{1})) ≈ S ∧ cat(δ(k_{2})) ≈ NP ∧ cat(δ(k_{3})) ≈ VP ∧cat(δ(k_{4})) ≈ V ∧ δ(k_{5}) ≈ vient

ψ = k_{6} ⊲ k_{7} ∧ cat(δ(k_{6})) ≈ NP ∧ δ(k_{7}) ≈ Jean
K_{ψ} = ∅

Figure 3. Jean vient: derivation step similar to substitution in TAGs

like an adjunction in a TAG (see Fig. 4). If ϕ_{1} ⊢ ¬δ(k_{1}) ≈ δ(k_{2}), then this is comparable to an OA-condition (obligatory adjunction) in a TAG. This idea of two node names k_{1}, k_{2} with a strong dominance such that other descriptions can be put in between, is first mentioned by Vijay-Shanker (1992).

4.3. Language. In contrast to TAGs for TDGs three different languages can be distinguished: First the set of descriptions derived by a grammar (the description language), second the set of corresponding “minimal” trees (tree language) and then as in TAGs the set of strings (string language) for these trees.

A possible start description for example is ϕ_{S} = cat(δ(k_{1})) ≈ S, cat ∈ A, S ∈ V in order to make sure, that the root has the category S.

Definition 15. (Description language) Let G = (A, V, T, D, ϕ_{S}) be a TDG. The description language of G is L_{D}(G) := {ϕ| ϕ_{S} ⇒^{∗} ϕ}.

ϕ_{1} ⇒^{(ψ,K_{ψ})} ϕ_{2} with ϕ_{2} = ϕ_{1} ∧ ψ ∧ k_{1} ≈ k_{4} ∧ k_{2} ≈ k_{10}

[figure: k_{8}; ancienne; k_{7}; A; k_{6}; AP; k_{9}; N; k_{5}; N; k_{10}; N; k_{4}; N; k_{1}; N; k_{2}; N; k_{3}; maison; k_{8}; ancienne; k_{7}; A; k_{6}; AP; k_{9}; N; k_{5}; N; k_{2}≈k_{10}; N; k_{3}; maison; k_{1}≈k_{4}; N; ϕ_{1}; ϕ_{2}; ψ]
ϕ_{1} = k_{1} ⊲^{∗} k_{2} ∧ k_{2} ⊲ k_{3} ∧ cat(δ(k_{1})) ≈ N ∧ cat(δ(k_{2})) ≈ N

∧δ(k_{3})) ≈ maison

ψ = k_{4} ⊲^{∗} k_{5} ∧ k_{5} ⊲ k_{6} ∧ k_{5} ⊲ k_{9} ∧ k_{6} ≺ k_{9} ∧ k_{6} ⊲ k_{7} ∧ k_{7} ⊲ k_{8}

∧k_{9} ⊲^{∗} k_{10} ∧ cat(δ(k_{4})) ≈ N ∧ cat(δ(k_{5})) ≈ N ∧ cat(δ(k_{6})) ≈ AP ∧cat(δ(k_{7})) ≈ A ∧ δ(k_{8}) ≈ ancienne ∧ cat(δ(k_{9})) ≈ N ∧cat(δ(k_{10})) ≈ N

K_{ψ} = {k_{10}}

Figure 4. ancienne maison: adjunction-like derivation step

Now the minimal trees of a description ϕ must be defined. Such a tree must satisfy ϕ, and it has to be minimal in the sense that its P relation is already described in ϕ. This means that it is sufficient to add term equivalences to ϕ in order to get a complete description of one of its minimal trees. To avoid some undesirable special cases a third condition for minimal trees is necessary. This condition says that if two node names are not equivalent in the description but describe the same node in a minimal tree, then they both have to be part of some strong dominance in the description.

Definition 16. (Minimal tree) Let G = (A, V, T, D, ϕ_{S}) be a TDG, ϕ ∈ L_{D}(G). A tree B is a minimal tree of ϕ, if there is a function g such that 1. B ⊧_{g} ϕ.

2. For all u_{1}, u_{2} in U: If ⟨u_{1}, u_{2}⟩ ∈ P, then there are k_{1}, k_{2} ∈ K such that B ⊧_{g} k_{1} ⊲ k_{2} and g(k_{1}) = u_{1}, g(k_{2}) = u_{2}.

3. For all k_{1}, k_{2} with g(k_{1}) = g(k_{2}): If ϕ ⊬ k_{1} ≈ k_{2}, then there are k′_{1}, k′_{2} such that first either ϕ ⊢_{s} k_{1} ⊲^{∗} k′_{1} or ϕ ⊢_{s} k′_{1} ⊲^{∗} k_{1} holds and second either ϕ ⊢_{s} k_{2} ⊲^{∗} k′_{2} or ϕ ⊢_{s} k′_{2} ⊲^{∗} k_{2} holds.

A description ϕ ∈ L_{D}(G) can have more than one minimal tree (see ϕ_{2} in fig. 8) or even no minimal tree. The set of minimal trees of a given description is decidable:

Proposition 7. Let G be a TDG. For each ϕ ∈ L_{D}(G) the set of minimal trees of ϕ can be constructed in finitely many steps.

More precisely we will construct representatives of classes of isomorphic minimal trees. Two trees B_{1} = (U_{1}, u_{1}, P_{1}, P_{1}^{∗}, L_{1}, μ_{1}, N_{1}, T_{1}) and B_{2} = (U_{2}, u_{2}, P_{2}, P_{2}^{∗}, L_{2}, μ_{2}, N_{2}, T_{2}) are isomorphic if there is a bijection f : U_{1} → U_{2} such that for all u_{1}, u_{2} ∈ U_{1}:

1. For all R ∈ {P, P^{∗}, L} : ⟨u_{1}, u_{2}⟩ ∈ R_{1} iff ⟨f(u_{1}), f(u_{2})⟩ ∈ R_{2}, and 2. μ_{1}(u_{1}) = μ_{2}(f(u_{1})). Henceforward we will not distinguish between isomorphic trees. A tree will be identified with the equivalent class it presents.

Proof: ϕ ∈ L_{D}(G). To find a minimal tree of ϕ a description ϕ′ must be found such that ϕ′ ⊢ ϕ, node(ϕ) = node(ϕ′) and for all k_{1}, k_{2} ∈ node(ϕ):

(a) ϕ′ ⊢_{s} k_{1} ⊲^{∗} k_{2} does not hold.

(b) ϕ′ ⊢ k_{1} ≈ k_{2} or ϕ′ ⊢ ¬k_{1} ≈ k_{2}.

(c) ϕ′ ⊢ k_{1} ⊲ k_{2} ⇒ there are k_{3}, k_{4} such that ϕ′ ⊢ k_{1} ≈ k_{3} ∧ k_{2} ≈ k_{4} and ϕ ⊢ k_{3} ⊲ k_{4} (no new parent relations).

(d) If ϕ′ ⊢ k_{1} ≈ k_{2} and ϕ ⊬ k_{1} ≈ k_{2}, then there are k′_{1}, k′_{2} such that first either ϕ ⊢_{s} k_{1} ⊲^{∗} k′_{1} or ϕ ⊢_{s} k′_{1} ⊲^{∗} k_{1} holds and second either ϕ ⊢_{s} k_{2} ⊲^{∗} k′_{2} or ϕ ⊢_{s} k′_{2} ⊲^{∗} k_{2} holds.

(e) For all k ∈ node(ϕ′): If k is a leaf name in ϕ, then there is a t ∈ T ∪{ϵ} such that ϕ′ ⊢ δ(k) ≈ t (leaves labelled by terminal symbols).

(f) For each k ∈ node(ϕ′), that is no leaf name in ϕ′ and for each attribute name a, there is a v ∈ V ∪ {⊥}, such that ϕ′ ⊢ a(δ(k)) ≈ v.

To find such a ϕ′ term equivalences are added as conjuncts to ϕ in the following way:

ϕ′ := ϕ

Add arbitrary conjuncts k_{1} ≈ k_{2} to ϕ′ with k_{1} ≠ k_{2} and k_{1}, k_{2} ∈ node(ϕ). Add arbitrary conjuncts δ(k) ≈ t to ϕ′ with k ∈ node(ϕ) and t ∈ T ∪ {ϵ}. For all k ∈ node(ϕ) where no formula δ(k) ≈ t was added and for all a ∈ A, choose a v ∈ V ∪ {⊥} and add the conjunct a(δ(k)) ≈ v to ϕ′.

If the result ϕ′ is a description such that conditions (a) - (f) hold (decidable), then it is one of the descriptions we wanted to construct.

The construction of course is non-deterministic. But as node(ϕ), A, V and T are finite, there are only finitely many possibilities to construct a ϕ′ in this way. Consequently all possible ϕ′ can be found in finitely many steps.

Now we must show that the resulting ϕ′ really correspond to minimal trees:

(i) Each of the ϕ′ uniquely describes a minimal tree B_{ϕ′} of ϕ:

B_{ϕ′} = (U_{ϕ′}, u_{0}_{ϕ′}, P_{ϕ′}, P_{ϕ′}^{∗}, L_{ϕ′}, μ, N_{A,V} , T) such that

(a) U_{ϕ′} = \{\overline{k} | \overline{k} is equivalence class wrt \{⟨k_{1}, k_{2}⟩|ϕ′ ⊢ k_{1} ≈ k_{2}\}\} (b) u_{0}_{ϕ′} = \{\overline{k} | all k ∈ \overline{k} are minimal in ϕ′\}

(c) P_{ϕ′} = \{⟨\overline{k_{1}}, \overline{k_{2}}⟩ | ϕ′ ⊢ k_{1} ⊲ k_{2} for all k_{1} ∈ \overline{k_{1}}, k_{2} ∈ \overline{k_{2}}\}

(d) P_{ϕ′}^{∗} = \{⟨\overline{k_{1}}, \overline{k_{2}}⟩ | ϕ′ ⊢ k_{1} ⊲^{∗} k_{2} for all k_{1} ∈ \overline{k_{1}}, k_{2} ∈ \overline{k_{2}}\}

(e) L_{ϕ′} = \{⟨\overline{k_{1}}, \overline{k_{2}}⟩ | ϕ′ ⊢ k_{1} ≺ k_{2} for all k_{1} ∈ \overline{k_{1}}, k_{2} ∈ \overline{k_{2}}\}

(f) A are the attribute names, V the attribute values for N_{A,V}. For all k_{1}, k_{2} ∈ K, that are no leaf names in ϕ′, we define: k_{1} ≈_{μ} k_{2} :iff ϕ′ ⊢ a(δ(k_{1})) ≈ a(δ(k_{2})) for all a ∈ A. N_{A,V} := \{\overline{k}_{μ}; \overline{k}_{μ} is equivalence class wrt ≈_{μ} \}. For all a ∈ A: ⟨a, α_{a}⟩ ∈ A such that for all \overline{k}_{μ} ∈ N_{A,V} and v ∈ V: α_{a}(\overline{k}_{μ}) = v iff ϕ′ ⊢ a(δ(k)) ≈ v for all k ∈ \overline{k}_{μ}.

(g) T are the terminals of the TDG.

(h) μ : U_{ϕ′} → N_{A,V} ∪ T ∪ \{ϵ\} such that for all \overline{k} ∈ U_{ϕ′}: 1. For all t ∈ T ∪ \{ϵ\}: μ(\overline{k}) = t iff ϕ′ ⊢ δ(k) ≈ t for all k ∈ \overline{k}.

2. For all N ∈ N_{A,V}: μ(\overline{k}) = N iff \overline{k} ⊆ N. Because of the inference rules, it is easy to see that B_{ϕ′} is a tree. To show: B_{ϕ′} is a minimal tree of ϕ:

1. B ⊧_{g} ϕ holds if g(k) = \overline{k} for all k ∈ node(ϕ′) and g(k) = u_{0}_{ϕ′} for all k ∉ node(ϕ′)

2. For all ⟨u_{1}, u_{2}⟩ ∈ P_{ϕ′} (definition of P_{ϕ′}) there are k_{1}, k_{2} ∈ node(ϕ) such that ϕ′ ⊢ k_{1} ⊲ k_{2} and g(k_{1}) = u_{1}, g(k_{2}) = u_{2}. ⇒ (condition (c) for ϕ′) there are k_{3}, k_{4} ∈ node(ϕ) such that ϕ ⊢ k_{3} ⊲ k_{4} and ϕ′ ⊢ k_{1} ≈ k_{3} ∧ k_{2} ≈ k_{4} ⇒ (definition of U_{ϕ′}) there are k_{3}, k_{4} ∈ node(ϕ) such that ϕ ⊢ k_{3} ⊲ k_{4} and g(k_{3}) = u_{1}, g(k_{4}) = u_{2}.

3. Let g(k_{1}) = g(k_{2}) and ϕ ⊬ k_{1} ≈ k_{2} hold.

⇒ ϕ′ ⊢ k_{1} ≈ k_{2} and ϕ ⊬_{1}≈ k_{2} ⇒ (cond. (d)) there are k′_{1}, k′_{2} such that first either ϕ ⊢_{s} k_{1}⊲^{∗}k′_{1} or ϕ ⊢_{s} k′_{1}⊲^{∗}k_{1} holds and second either ϕ ⊢_{s} k_{2}⊲^{∗}k′_{2} or ϕ ⊢_{s} k′_{2}⊲^{∗}k_{2} holds.

(ii) For each minimal tree B of ϕ there is a ϕ′ that can be constructed

from ϕ such that B is isomorphic to B_{ϕ′}:

Let B be a minimal tree of ϕ ∈ L_{D}(G) wrt the node assignment g. For all k, k_{1}, k_{2} ∈ node(ϕ): If k_{1} ≠ k_{2} and g(k_{1}) = g(k_{2}), then add k_{1} ≈ k_{2} as a conjunct to ϕ. If there is a t ∈ T ∪ {ϵ} such that μ(g(k)) = t, then add δ(k) ≈ t as a conjunct to ϕ. If g(k) is no leaf, then for all ⟨a, α_{a}⟩ ∈ A: If there is a v ∈ V such that α_{a}(g(k)) = v, then add the conjunct a(δ(k)) ≈ v, else add the conjunct a(δ(k)) ≈ ⊥. The resulting description ϕ′ is one of the descriptions, that can be constructed from ϕ in the way described above.

Obviously the corresponding tree B_{ϕ′} is isomorphic to B.

□

Definition 17. (Tree language) Let G = (A, V, T, D, ϕ_{S}) be a TDG. The tree language of G is L_{T} (G) := {B; B is minimal tree of a ϕ ∈ L_{D}(G)}.

Definition 18. (String language) Let G = (A, V, T, D, ϕ_{S}) be a TDG, B ∈ L_{T} (G).

1. The string of B, word(B) is the string w = t_{1}t_{2}...t_{n} ∈ T^{∗} such that:

If b_{1}, b_{2}, ..., b_{n} are all leaves in B, that are not labelled by the empty word and if ⟨b_{i}, b_{i+1}⟩ ∈ L_{B}, 1 ≤ i ≤ n − 1, then μ(b_{j}) = t_{j}, 1 ≤ j ≤ n.

2. The string language of G is L_{S}(G) := {w; there is a B ∈ L_{T} (G) such that w = word(B)}.

3. A language L ⊆ T^{∗} is a Tree Description Language (TDL), if there is a TDG G such that L_{S}(G) = L.

5. Formal properties of TDGs

In this section I will first show that TDLs are a true superset of TALs. Then I will define lexicalized TDGs and prove their decidability.

5.1. Relation to TAGs. In order to prove that every TAL is a TDL, we have to construct an equivalent TDG for a given TAG. The idea is that a TAG is a special kind of TDG, where for each node name either daughters are described or there is exactly one strong dominance with this name on the left side. Before showing that TALs are a subset of TDLs I will define which descriptions correspond to a tree derived in a TAG:

Definition 19. (Description of a tree) Let γ be a tree derived wrt to a TAG from an elementary tree. The description of γ, d(γ), is one unique description ϕ, that can be inductively constructed in the following way:

(i) Choose an arbitrary node name k_{r}. ϕ := k_{r} ≈ k_{r} (ii) Let u_{r} be the root node of γ and β_{1}, ⋯ β_{k} those auxiliary trees that

cannot be adjoined to u_{r}.

If u_{r} is labelled by A ∈ N, then ϕ := ϕ ∧ cat(δ(k_{r})) ≈ A. If u_{r} is labelled by t ∈ T ∪ {ϵ}, then ϕ := ϕ ∧ δ(k_{r}) ≈ t. Choose a new name k_{f}. k_{r} is called the top-name, and k_{f} the

bottom-name of u_{r}.

If u_{r} has a OA-constraint, then ϕ := ϕ ∧ k_{r} ⊲^{∗} k_{f} ∧ adj(δ(k_{r})) ≈ root ∧ aux(δ(k_{r})) ≈ yes ∧ adj(δ(k_{f})) ≈ foot ∧ β_{1}(δ(k_{r})) ≈ no ∧ ⋯ ∧ β_{k}(δ(k_{r})) ≈ no.

If u_{r} has a SA-constraint, then ϕ := ϕ ∧ k_{r} ⊲^{∗} k_{f} ∧ aux(δ(k_{r})) ≈ yes ∧ adj(δ(k_{f})) ≈ foot ∧ β_{1}(δ(k_{r})) ≈ no ∧ ⋯ ∧ β_{k}(δ(k_{r})) ≈ no.

[figure: OA:; SA:; adj≈foot; adj≈root,aux≈yes; adj≈foot; aux≈yes]

If W has a NA-constraint, then ϕ := ϕ ∧ k_{r} ≈ k_{f}.

If γ_{1}, ⋯ γ_{n} are from left to right the trees immediately dominated by W in γ, then choose new names k_{1}, ⋯ k_{n}. ϕ := ϕ ∧ k_{f} ⊲ k_{1} ∧ ⋯ k_{f} ⊲ k_{n} ∧ k_{1} ≺ k_{2} ∧ ⋯ k_{n−1} ≺ k_{n}. Then from i = 1 up to i = n: γ := γ_{i}, k_{r} := k_{i}, i := i + 1 and go to (ii).

Proposition 8. For every TAG G_{A} a TDG G_{D} can be constructed, such that L_{S}(G_{A}) = L_{S}(G_{D}). The tree languages of G_{A} and G_{D} only differ wrt to the nonterminal symbols.

Before showing the proposition we will prove the following lemma:

Lemma. For a TAG G there is an equivalent TAG G′ such that L_{S}(G) = L_{S}(G′), the tree languages differ only in nonterminal symbols, and in G′ for all nodes u_{1}, u_{2}: If u_{1} and u_{2} are both on a spine of some auxiliary tree (not necessarily the same), if both are neither root nor foot and if for both adjunction is possible, then they are labelled by different nonterminals.

Proof of the lemma: Let G_{A} be a TAG. Without loss of generality let G_{A} be without feature structures and without substitution. The nodes can have adjunction constraints NA, SA({β_{1}, ⋯ β_{n}}) or OA({β_{1}, ⋯ β_{n}}).

For all auxiliary trees: All labels of nodes on the spine other than the foot are different from the label of the root (cf. Lemma 1 in Rogers (1994a)). Construction of an equivalent TAG G′_{A}:

If there are two nodes with the same label X, both on a spine of some auxiliary tree and both neither root nor foot, such that adjunction is possible for both, then replace one of the X by a new label X_{i}. Continue until there is no such pair of nodes.

Then for each new label X_{i} all auxiliary trees β with root label X are copied, and in the new tree β_{i} the labels X of foot and root are replaced by X_{i}. In the adjunction constraint for a node labelled by X_{i}, β is replaced by β_{i}.

Let G′_{A} be the new TAG constructed in this way, N′ the new nonterminals.

Clearly L_{S}(G_{A}) = L_{S}(G′_{A}) holds, and the trees of L_{T} (G_{A}) and L_{T} (G′_{A}) only differ wrt nonterminal symbols.

□

To prove Prop. 8 it is not enough to take the descriptions d(γ) for all elementary trees γ in G_{A} (or G′_{A}) as elementary descriptions in G_{D}. The

construction of G_{D} is more complicated because derivation steps ϕ_{1} ⇒^{ψ} ϕ_{2} as shown in the following figure must be avoided:

[figure: k_{2}; k_{1}; ϕ_{1}; k_{3}; k_{4}; ψ = d(β); ϕ_{2}; k_{1} ≈ k_{3}; k_{2} ≈ k_{4}]

Proof of Prop. 8: Let G′_{A} = ⟨I′, A′, N′, T′⟩ be the TAG constructed from G_{A} as described in the lemma. Without loss of generality let the root nodes of auxiliary trees have a NA-constraint. Construction of a TDG G_{D} = (A_{D}, V, T_{D}, D, ϕ_{S}) equivalent to G′_{A}: ϕ_{S} := k_{1} ≈ k_{1}, T_{D} := T′. A_{D} := {cat, adj, aux} ∪ {β_{i}; β_{i} ∈ A′}, V := N′ ∪ {root, foot, yes, no}. Elementary descriptions: For all α ∈ I′: \overline{(d(α), ∅)} ∈ D. For all β ∈ A′:

(i) If there is no node different from the foot on the spine of β where

adjunction is possible, then:

\overline{(d(β) ∧ β(δ(k_{r})) ≈ yes ∧ adj(δ(k_{r})) ≈ root ∧ aux(δ(k_{r})) ≈ yes, \{k_{b}\})} ∈ D with k_{r} minimal and k_{b} bottom-name of the foot in d(β).

(ii) If K_{1}, ⋯, K_{n} are all nodes (different from the foot) on the spine of β, where adjunction is possible, K_{i} is labelled B_{i} and K_{i} dominates K_{k+1} for 1 ≤ i ≤ n − 1, then:

[figure: β; A; B_{1}; .; .; .; B_{n}; A]

Let γ be β without the subtree with root K_{1}. Then:

\overline{(d(γ)′ ∧ adj(δ(k_{r})) ≈ root ∧ aux(δ(k_{r})) ≈ yes ∧ β(δ(k_{r})) ≈ yes, \{k_{b}\})} ∈ D with k_{r} minimal and k_{t}, k_{b} is the top and bottom pair of K_{1} in d(γ), and d(γ)′ results from removing the conjunct aux(δ(k_{t})) ≈ yes from d(γ).

For all i, 1 ≤ i ≤ n: Let γ_{i} be the subtree with root K_{i} without the one with root K_{i+1}, d(γ_{i}) the description of γ_{i}, such that k_{min} minimal in d(γ_{i}) and k_{t}, k_{b} the top and bottom pair of K_{i+1}. d(γ_{i})′ results from removing the conjunct aux(δ(k_{t})) ≈ yes from d(γ_{i}). Then:

\overline{(d(γ_{i})′ ∧ adj(δ(k_{min})) ≈ foot ∧ aux(δ(k_{min})) ≈ no, \{k_{b}\})} ∈ D.

Let γ′ be the subtree dominated by K_{n}, k_{min} minimal in d(γ′) and k_{t}, k_{b} the top and bottom pair of the foot node. Then:

\overline{(d(γ′) ∧ adj(δ(k_{min})) ≈ foot ∧ aux(δ(k_{min})) ≈ no, \{k_{b}\})} ∈ D.

[figure: B_{1}; A; adj≈root; B_{i+1}; B_{i}; adj≈foot; A; B_{n}; adj≈foot]

These are all elements in D.

To show: L_{S}(G′_{A}) = L_{S}(G_{D}). First we show two lemmata for G_{D}:

Lemma 1: For all ϕ such that ϕ_{S} ⇒^{∗} ϕ: If ϕ ⊢_{s} k_{1}⊲^{∗}k_{2} and ϕ ⊢_{s} k_{3}⊲^{∗}k_{4} and ϕ ⊢ k_{1} ≈ k_{3} ∨ k_{2} ≈ k_{4}, then ϕ ⊢ k_{1} ≈ k_{3} ∧ k_{2} ≈ k_{4} holds.

For each derivation step ϕ_{1} ⇒^{\overline{(ψ,\{k_{2}\})}} ϕ_{2} apart from the first one: ψ is a description constructed for an auxiliary tree. There are k, k′ such that ϕ_{1} ⊢_{s} k ⊲^{∗} k′, and there is a k_{min} minimal in ψ such that ϕ_{2} ⊢ k ≈ k_{min} ∧ k′ ⊲^{∗} k_{2}. Furthermore there is a k_{1} such that ψ ⊢_{s} k_{1} ⊲^{∗} k_{2} and ϕ_{2} ⊢_{s} k_{1} ⊲^{∗} k′.

[figure: ϕ_{1}; k′; k; ψ; k_{2}; k_{1}; ϕ_{2}; k_{1}; k′; k]

(k_{2} is identified with a name dominated by k′.)

Proof of Lemma 1: Induction on length n of the derivation Induction start n = 1: For all \overline{(ψ, K_{ψ})} ∈ D: There is a ϕ such

that ϕ_{S} ⇒^{\overline{(ψ,K_{ψ})}} ϕ iff ψ = d(α) for an initial tree α and K_{ψ} = ∅. This follows from |node(ϕ_{S})| = 1.

Because of this and because of the construction of d(α) for initial trees α, the induction claim holds for n = 1.

Induction step: ϕ_{S} ⇒ ϕ ⇒^{∗} ϕ_{1} ⇒^{\overline{(ψ,K_{ψ})}} ϕ_{2}, induction claim holds for ϕ_{1}.

Suppose: ψ = d(γ) where all leaves in γ are labelled by terminals, K_{ψ} = ∅, and γ has more than one node.

Let k_{min} be minimal in ψ and ψ ⊢ cat(δ(k_{min})) ≈ X. There are (def. 14) k_{1}, k_{2} such that ϕ_{1} ⊢_{s} k_{1} ⊲^{∗} k_{2} and ϕ_{2} ⊢ k_{1} ≈ k_{min}.

(i) 1. case: There is no pair k′_{1}, k′_{2} ∈ node(ψ) of a top- and a bottomname such that there is a k′ ∈ node(ϕ_{1}) with ϕ_{2} ⊢ k′_{1} ⊲^{∗} k′ ∧ k′ ⊲^{∗} k′_{2}. ⇒ (def. 11 and 14) There is a leaf name k in ψ and a t ∈ T ∪{ϵ}, such that ϕ_{2} ⊢ k_{1} ≈ k_{min} ∧ k ⊲^{∗} k_{2} ∧ δ(k) ≈ t ∧ ¬δ(k_{2}) ≈ t. ⇒ ϕ_{2} is not satisfiable. Contradiction.

(ii) 2. case: There are k′_{1}, k′_{2} in ψ as top and bottom of a node with adjunction possible, and there is a k′ ∈ node(ϕ_{1}) with ϕ_{2} ⊢ k′_{1} ⊲^{∗} k′ ∧ k′ ⊲^{∗} k′_{2}. k′_{1}, k′_{2} are not dominated by any other pair k′′_{1}, k′′_{2} with the same properties. Then ϕ_{2} ⊢_{s} k′_{1} ⊲^{∗} k_{2} and there is a k_{3} ∈ node(ϕ_{1}) such that ϕ_{2} ⊢_{s} k_{3} ⊲^{∗} k′_{2}. If k_{3} is a leaf name, then we immediately have a contradiction as in (i). If not, then inductively we get a contradiction as in (i). This means that ψ = d(γ) was constructed for an auxiliary tree.

Then clearly the derivation step is of the form shown above.

Lemma 2: If ψ_{1}, ⋯ ψ_{n} with minimal names k_{1}, ⋯, k_{n} are the descrip-

tions constructed (in this order) from an auxiliary tree β, then: If k_{r}, k_{f} in ϕ_{1} are top and bottom of a node with adjunction

possible and if ϕ_{1} ⇒^{ψ_{1}} ϕ′ with ϕ′ ⊢ k_{r} ≈ k_{1} holds, then for all ϕ_{2}, such that ϕ′ ⇒^{∗} ϕ_{2} and ϕ_{2} has minimal trees:

ϕ′ ⇒^{∗} ⋯ ⇒^{ψ_{1}} ⋯ ⇒^{∗} ⋯ ⇒^{ψ_{n}} ⋯ ⇒^{∗} ϕ_{2}

with ϕ_{2} ⊢ k_{r} ≈ k_{1} ∧ k_{1} ⊲^{∗} k_{2} ∧ ⋯ k_{n} ⊲^{∗} k_{f}.

None of the ψ_{i} is used more often than ψ_{1} in a derivation.

Proof of Lemma2: Induction on the maximal number of top and bottom pairs k_{t}, k_{b}, such that there is a single k ∈ K with ϕ_{2} ⊢ k_{t} ⊲^{∗} k ∧ k ⊲^{∗} k_{b} for all these pairs k_{t}, k_{b}.

Induction start: n = 0 trivial (no “adjunction”).

Induction step: Let k_{r}, k_{f} in ϕ_{1} be top and bottm of a node where adjunction is possible, ϕ_{1} ⊢ cat(δ(k_{r})) ≈ A ∧ cat(δ(k_{f})) ≈ A.

Because of the attribute aux the only possibility of adding an elementary description by identifying its minimal name with k_{r} is to add the first of the descriptions of an auxiliary tree with root and foot label A.

Let ψ_{1}, ⋯ ψ_{n} (as in Lemma 2) be the descriptions of such a tree.

ϕ_{1} ⇒^{ψ_{1}} ϕ′ where ϕ′ ⊢ k_{r} ≈ k_{1} ∧ k′_{1} ⊲^{∗} k_{f} ∧ cat(δ(k′_{1})) ≈ B_{1} ∧

cat(δ(k_{f})) ≈ A, where k′_{1} is top of the adjunction node on the spine. B_{1} ≠ A (construction). ⇒ ϕ′ ⊢_{s} k′_{1} ⊲^{∗} k_{f} and ϕ′ ⊢ ¬k′_{1} ≈ k_{f} ⇒ ϕ′ has no minimal tree.

We have to add something between k′_{1} and k_{f}. This can be a description from an auxiliary tree with root and foot labelled by B_{1}. Then (induction claim) after having added all descriptions for this auxiliary tree, we arrive at a description ϕ′′, such that for a new name k: ϕ′′ ⊢_{s} k ⊲^{∗} k_{f} and ϕ′′ ⊢ k′_{1} ⊲^{∗} k ∧ cat(δ(k)) ≈ B_{1} ∧ cat(δ(k_{f})) ≈ A, ⇒ ϕ′′ still has no minimal tree.

⇒ there must be a description added with a minimal name labelled by B_{1}, that was not constructed for an auxiliary tree with root and foot label B_{1}.

⇒ (construction of G′_{A}) ψ_{2} must be added such that k_{2} must be equivalent to k′_{1}. Inductively this means that all ψ_{1}, ⋯ ψ_{n} must be added in the correct order between k_{r} and k_{f}.

We now define a new derivation mode for G_{D} where all elementary descriptions for one elementary tree are added at once: First we remove all conjuncts aux(δ(k)) ≈ no for any k from the descriptions of G_{D}. Then we define:

ϕ_{1} ↦ ϕ_{2} :if either ϕ_{1} = ϕ_{S} and ϕ_{1} ⇒ ϕ_{2} or there are descriptions ψ_{1}, ⋯ ψ_{n} corresponding (as above) to an auxiliary tree with k_{i} minimal and k_{i}^{b} marked in ψ_{i} and ψ_{i} ⊢_{s} k_{i}^{t} ⊲^{∗} k_{i}^{b} (for 1 ≤ i ≤ n) and there is a top and bottom pair k_{r}, k_{f} in ϕ_{1}, such that ϕ_{2} = ϕ_{1} ∧ ψ_{1} ∧ ⋯ ∧ ψ_{n} ∧ k_{r} ≈ k_{1} ∧ k_{1}^{b} ≈ k_{2} ∧ ⋯ ∧ k_{n}^{b} ≈ k_{f} ∧ aux(δ(k_{1}^{t})) ≈ yes ∧ ⋯ aux(δ(k_{n}^{t})) ≈ yes.

As already shown (Lemma 2) ϕ_{1} ⇒^{∗} ϕ_{2} holds and ϕ_{2} has minimal trees iff ϕ_{1} ↦^{∗} ϕ_{2} and there is no strong dominance ϕ_{2} ⊢_{s} k_{1} ⊲^{∗} k_{2}, such that ϕ_{2} ⊢ adj(δ(k_{1})) ≈ root ∧ adj(δ(k_{2})) ≈ foot.

Furthermore the following can be shown:

γ_{1} ⇒^{∗} γ_{2} in G′_{A} iff ϕ_{1} ↦^{∗} ϕ_{2} in G_{D} with ϕ_{1} = d(γ_{1}) and ϕ_{2} = d(γ_{2}) (up to

a bijection of K). If there is no OA-constraint in γ_{i}, then γ_{i} is the only minimal tree of ϕ_{i}. Proof by induction on the length n of the derivation:

(i) Induction start n = 0: Induction claim trivially holds. (ii) Induction step n → n + 1: γ_{1} = γ_{k_{1}} ⇒ γ_{k_{2}} ⋯ ⇒ γ_{k_{n}} ⇒ γ_{2}.

Consequently (induction claim) ϕ_{1} ↦ ϕ_{k_{2}} ⋯ ↦ ϕ_{k_{n}} with ϕ_{i} = d(γ_{i}), 1 ≤ i ≤ n.

Let K be a node in γ_{k_{n}}, where adjunction is possible, k_{t}, k_{b} are top and bottom of K in ϕ_{k_{n}}.

An auxiliary tree β can be adjoined to K iff the descriptions corresponding to β can be added between k_{t} and k_{b}. This follows immediately from the construction of G_{D}.

[figure: ϕ_{S}; ψ; A_{1}; A_{1}; A_{2}; A_{2}; A_{3}; A_{n−1}; A_{n}; A_{n}; ϵ; A_{1}; A_{1}; a_{1}; A_{1}; k_{1}; A_{2}; k_{2}; A_{2}; a_{2}; A_{2}; k_{3}; A_{3}; k_{4}; A_{n}; k_{2n−2}; A_{n}; a_{n}; A_{n}; k_{2n−1}; K_{ψ} = {k_{1}, k_{2}, k_{3}, ⋯ k_{2n−1}}]
Figure 5. TDG for {a_{1}^{k} ⋯ a_{n}^{k}}

Consequently γ_{k_{n}} ⇒ γ_{2} iff ϕ_{k_{n}} ↦ ϕ_{2}.
□

Proposition 9. There are TDLs, that are no TALs.

For example {a_{1}^{k}a_{2}^{k}...a_{n}^{k}; 0 ≤ k} for n ≥ 5 and {w^{n}; w ∈ T^{∗}} for n ≥ 3 are TDLs. Fig. 5 and 6 show corresponding TDGs. According to the pumping lemma for TALs (see Vijayashanker (1987)) these languages are no TALs.

5.2. Decidability. In order to deal with natural languages in a way similar to TAGs, we will now define lexicalized TDGs (for a definition of lexicalized grammars in general see Schabes (1990)).

Definition 20. (Lexicalized TDG) A TDG G is a lexicalized TDG (LTDG), if for every elementary description ψ in G there are two names k and k_{t} and there is a t ∈ T, such that ψ ⊢ k ⊲ k_{t} ∧ δ(k_{t}) ≈ t.

[figure: ϕ_{S}; S; S_{1}; S_{1}; ...; (n times); S_{1}; S_{1}; ϵ; ϵ; ψ_{a} for a ∈ T; S; S_{1}; S_{1}; ...; S_{1}; k_{1}; S_{1}; k_{n}; a; a; K_{ψ_{a}} = {k_{1}, ⋯ k_{n}}]
Figure 6. TDG for {w^{n}; w ∈ T^{∗}}

With Prop. 6 and Prop. 7 the following proposition holds for LTDGs:

Proposition 10. (Decidability) For LTDGs the word problem is decidable.

Proof: First we will show that for a given description ϕ and an elementary ψ the set of equivalence classes of descriptions ϕ′ with ϕ ⇒^{ψ} ϕ′ is finite and can be constructed in finitely many steps (i.e. is decidable). Here two descriptions ϕ′_{1} and ϕ′_{2} are called equivalent iff ϕ′_{1} ⊢ ϕ′_{2} and ϕ′_{2} ⊢ ϕ′_{1}. Let ϕ be a description and ψ an elementary decription. Construction of the descriptions ϕ′ with ϕ ⇒^{ψ} ϕ′:

1. Let Φ′ be the set of those descriptions ϕ′ where node(ϕ′) = node(ϕ) ∪ node(ψ) and ϕ′ = ϕ ∧ ψ ∧ ξ for a conjunction ξ. Each conjunct in ξ is either an elementary formula without the symbol ⊲ or it is a disjunction of equivalences of l-terms or v-terms. No conjunct and no disjunct occurs more than once in ξ. Furthermore (A1) − (A4) for derivation steps must hold for ϕ′. Φ′ is finite and decidable and it is clearly a superset of the descriptions derivable from ϕ by adding ψ.

2. For all ϕ_{i} ∈ Φ′: if there is a ϕ_{j} ∈ Φ′ such that ϕ_{j} ⊢ ϕ_{i} and ϕ_{i} ⊬ ϕ_{j}, then remove ϕ_{i} from Φ′.

Because of prop. 6 the set Φ′ contains all descriptions ϕ′ such that ϕ ⇒^{ψ} ϕ′ (more precisely: one element of each equivalence class \overline{ϕ′}). To decide for a given w = t_{1} ⋯ t_{n}, t_{i} ∈ T, whether w ∈ L_{S}(G) holds, all derivations ϕ_{S} ⇒^{∗} ϕ must be done where for each of the t_{i} exactly one elementary description ψ is used in deriving ϕ with ψ ⊢ δ(k) ≈ t_{i} for one node name k. In this way in finitely many steps we get a finite set of descriptions. After that we only have to test whether w = word(B) holds for a minimal tree B of one of the derived descriptions. According to Prop. 7 this is decidable.

□

6. Advantages of TDGs for natural language

TDGs offer all advantages of multicomponent TAGs (MC-TAGs) because one elementary description can describe several subtrees that have to be added at the same time. MC-TAGs are an extension of TAGs necessary for linguistic purposes, e.g. to deal with long-distance scrambling in German (see Becker et al. (1991)). With TDGs scrambling phenomena can be analyzed in the way proposed by Kroch and Rambow (1994).

6.1. Complement clauses. As already pointed out in the introduction, one of the deficiencies of TAGs is, that complement clauses must be treated in a different way than other arguments (see Abeillé (1988) and Rambow et al. (1995)). One of the main ideas in TAG is, that arguments should be added by substitution to the argument structure wheras adjuncts are added by adjunction. The only exception are complement clauses. The reason for this difference is the desire to describe argument structures locally. In TAGs all argument nodes for one lexical head are in one elementary tree. Even for unbounded dependencies the argument that has been moved has to be in the same elementary tree as the head of the argument structure. If one wants to preserve this in a TAG, it is not possible to add complement clauses by substitution but the argument structure must be adjoined to the complement clause.

With TDGs it is possible to have this local analysis of unbounded dependencies without treating complement clauses in a way different from other arguments (see fig. 7). Even for unbounded dependencies inside of complement clauses the derivation can start from the argument structure and the complement clause is added in one derivation step. The crucial point here is that there can be arbitrarily many marked names in elementary descriptions. This treatment of complement clauses corresponds to the subsertion operation proposed in Rambow et al. (1995).

In TDGs the elementary description for arguments and those for modifiers differ in the following way: Arguments are described by descriptions ψ TAG-analysis: γ_{1} ⇒^{β} γ_{2}

γ_{1}

β

γ_{2}

[figure: S; NP; ϵ; VP; V; V; tu; penses; S; Comp; que; S]

[figure: S; WH; S]

[figure: S; WH]

[figure: S; NP; ϵ; VP; V; V; tu; penses; S; Comp; que; S]

[figure]

TDG-analysis: ϕ_{1} ⇒^{(ψ,K_{ψ})} ϕ_{2} with ϕ_{2} = ϕ_{1} ∧ ψ ∧ k_{1} ≈ k_{10} ∧ k_{2} ≈ k_{13} ∧ k_{9} ≈

k_{14}

ϕ_{1}

ψ ϕ_{2}

[figure: S; k_{1}; S; k_{2}; NP; ϵ; VP; V; V; tu; penses; S; Comp; que; S; k_{9}] [figure: S; k_{10}; S; k_{11}; WH; S; k_{13}; S; k_{14}; S; k_{15}]

K_{ψ} = {k_{13}, k_{14}}
[figure: S; k_{1}≈k_{10}; S; k_{11}; WH] [figure: S; k_{2}≈k_{13}; NP; ϵ; VP; V; V; tu; penses; S; Comp; que; S; k_{9}≈k_{14}] [figure: S; k_{15}]

Figure 7. complement clauses with unbounded dependencies qui penses-tu que Marie aime ϵ (see Abeillé (1988))

ϕ_{1} ⇒^{(ψ,K_{ψ})} ϕ_{2} with ϕ_{2} = ϕ_{1} ∧ ψ ∧ k_{2} ≈ k_{14} ∧ k_{1} ≈ k_{11}

[figure: ϕ_{1}; ψ; ϕ_{2}; k_{8}; ancienne; k_{7}; A; k_{6}; AP; k_{9}; N; k_{5}; N; k_{2}≈k_{10}; N; k_{3}; maison; k_{1}≈k_{4}; N; k_{17}; bleue; k_{16}; A; k_{15}; AP; k_{13}; N; k_{12}; N; k_{14}; N; k_{11}; N; ancienne; A; AP; N; N; N; k_{10}≈k_{2}; k_{14}≈k_{2}; maison; N; k_{4}≈k_{1}; k_{11}≈k_{1}; bleue; A; AP; N; N]
ϕ_{1} = see ϕ_{2} in fig. 4
ψ = k_{11} ⊲^{∗} k_{12} ∧ k_{12} ⊲ k_{13} ∧ k_{12} ⊲ k_{15} ∧ k_{13} ≺ k_{15} ∧ k_{13} ⊲^{∗} k_{14}

∧k_{15} ⊲ k_{16} ∧ k_{16} ⊲ k_{17} ∧ cat(δ(k_{11})) ≈ N ∧ cat(δ(k_{12})) ≈ N ∧cat(δ(k_{13})) ≈ N ∧ cat(δ(k_{14})) ≈ N ∧ cat(δ(k_{15})) ≈ AP ∧cat(δ(k_{16})) ≈ A ∧ δ(k_{17}) ≈ bleue

K_{ψ} = {k_{14}}

The minimal trees of ϕ_{2} are those in fig. 1.

Figure 8. Nominal modifiers: ancienne maison bleue

such that no leaf name is marked. In contrast to this the elementary description of a modifier contains a marked leaf name, that can be compared to a foot node of an auxiliary tree in a TAG.

6.2. Underspecification. As already mentioned in the introduction one of the main reasons for defining TAG-like grammars in a constraint based way was the desire to have underspecified representations of trees. With TDGs it is possible to describe several readings in one tree description. Syntactic ambiguities that can be analyzed in this way are nominal modifier ambiguities as in Fig. 8 and also PP-attachment ambiguities as in Fig. 9. For scope ambiguities, for example quantifier ambiguities, it is also possible to derive underspecified representations similar to those in Muskens (1995). ϕ_{1}

[figure: k_{2}; k_{3}; Jean; NP; VP; k_{4}; S; k_{1}; k_{5}; VP; V; k_{6}; regarde; k_{7}] [figure: k_{8}; NP; k_{9}; Det; k_{11}; N; k_{10}; un; k_{12}; N; k_{13}; homme] [figure: k_{20}; avec; k_{19}; P; k_{21}; NP; k_{18}; PP; k_{16}; VP∨N; k_{15}; VP∨N; k_{17}; VP∨N; k_{14}; VP∨N] ψ

ϕ_{1} = k_{1} ⊲ k_{2} ∧ k_{1} ⊲ k_{4} ∧ k_{2} ≺ k_{4} ∧ k_{2} ⊲ k_{3} ∧ k_{4} ⊲^{∗} k_{5} ∧ k_{5} ⊲ k_{6}

∧k_{5} ⊲ k_{8} ∧ k_{6} ≺ k_{8} ∧ k_{6} ⊲ k_{7} ∧ k_{8} ⊲ k_{9} ∧ k_{8} ⊲ k_{11} ∧ k_{9} ≺ k_{11} ∧k_{9} ⊲ k_{10} ∧ k_{11} ⊲^{∗} k_{12} ∧ k_{12} ⊲ k_{13} ∧ ⋯

ψ = k_{14} ⊲^{∗} k_{15} ∧ k_{15} ⊲ k_{16} ∧ k_{15} ⊲ k_{18} ∧ k_{16} ≺ k_{18} ∧ k_{16} ⊲^{∗} k_{17}

∧k_{18} ⊲ k_{19} ∧ k_{18} ⊲ k_{21} ∧ k_{19} ≺ k_{21} ∧ k_{19} ⊲ k_{20} ∧[cat(δ(k_{14})) ≈ VP ∨ cat(δ(k_{14})) ≈ N] ∧[cat(δ(k_{15})) ≈ VP ∨ cat(δ(k_{15})) ≈ N] ∧ cat(δ(k_{15})) ≈ cat(δ(k_{16})) ∧[cat(δ(k_{17})) ≈ VP ∨ cat(δ(k_{17})) ≈ N] ∧ cat(δ(k_{18})) ≈ PP ∧cat(δ(k_{19})) ≈ P ∧ δ(k_{20}) ≈ avec ∧ cat(δ(k_{21})) ≈ NP

K_{ψ} = {k_{17}}
ϕ_{2} = ϕ_{1} ∧ ψ_{1} ∧ k_{4} ≈ k_{14} ∧ k_{12} ≈ k_{17}

[figure: ϕ_{2}; Jean; NP; VP; k_{4}≈k_{14}; S; VP; V; regarde; NP; Det; N; un; k_{12}≈k_{17}; N; homme; avec; P; NP; PP; VP∨N; VP∨N]

Figure 9. PP-attachment: Jean regarde un homme avec un télescope

7. Conclusion

In this article I have presented a constraint-based extension of Tree Adjoining Grammars. For the grammar formalism I am using a quantifier-free first order logic similar to the one proposed by Rogers (1994b). Based on inference rules in the style of those introduced by Rogers I have defined a notion of syntactic consequence that was proved to be decidable, sound and even complete.

A Tree Description Grammar consists of a set of formulas of this logic. These formulas are called descriptions and have a certain form, they describe certain subtrees and dominance relations between these subtrees. The grammar formalism is derivation based where in each derivation step a description is extended by adding another description belonging to the grammar.

Concerning their formal properties I have shown that Tree Description Languages are a true superset of Tree Adjoining Languages and that they contain the languages {a_{1}^{k}a_{2}^{k}...a_{n}^{k}; 0 ≤ k} for n ≥ 5 and {w^{n}; w ∈ T^{∗}} for n ≥ 3. Tree Description Grammars seem to be powerful enough to deal with natural languages. But it is possible that they are even too powerful. I am currently working on restricted versions of TDGs that still have all the advantages of TDGs for natural language processing but that can be shown to describe semilinear languages, i.e. languages for which the constant growth property holds.

As we have seen TDGs not only provide a constraint-based definition of TAGs. They also offer the advantages of MC-TAGs and of D-Tree Grammars because they enable us to add several subtree descriptions at the same time and to treat arguments in a uniform way. Furthermore TDGs allow the introduction of underspecification for TAGs. It seems to be quite natural to use constraint-based grammar formalisms to allow underspecification. Using TDGs, underspecified representations can be derived for structural ambiguities and for scope ambiguities. Thus with respect to natural language processing TDGs are a reasonable extension of TAGs.

References

Abeillé, A.: 1988, Parsing French with tree adjoining grammar: some

linguistic accounts, Proceedings of COLING, Budapest. Backofen, R., Rogers, J. and Vijay-Shanker, K.: 1995, A first-order ax-

iomatization of the theory of finite trees, Jounal of Logic, Language and Information 4(1), 5–39.

Becker, T., Joshi, A. K. and Rambow, O.: 1991, Long-distance scrambling

and tree adjoining grammars, Proceedings of ACL-Europe. Ebbinghaus, H.-D., Flum, J. and Thomas, W.: 1992, Einführung in

die mathematische Logik, BI-Wissenschaftsverlag, Mannheim, Leipzig, Wien, Zürich.

Joshi, A. K.: 1987, An introduction to Tree Adjoining Grammars, in A. Manaster-Ramer (ed.), Mathematics of Language, John Benjamins, Amsterdam.

Kallmeyer, L.: 1996, Tree Description Grammars, in D. Gibbon (ed.), Natural Language Processing and Speech Technology. Results of the 3rd KONVENS Conference, Mouton de Gruyter, Berlin.

Kroch, T. and Rambow, O.: 1994, The linguistic relevance of quasitrees, 3e Colloque International sur les Grammaires d’Arbres Adjoints (TAG+3), Paris.

Marcus, M. P., Hindle, D. and Fleck, M. M.: 1983, D-theory: Talking

about talking about trees, Proceedings of ACL. Muskens, R.: 1995, Order-independence and underspecification, in

J. Groenendijk (ed.), Ellipsis, Underspecification, Events and More in Dynamic Semantics, DYANA Report R2.2.C.

Poesio, M.: 1996, Semantic ambiguity and perceived ambiguity, in K. van Deemter and S. Peters (eds), Semantic Ambiguity and Underspecification, CLSI Publications Stanford.

Rambow, O.: 1994, Multiset-Valued Linear Index Grammars: Imposing

dominance constraints on derivations, Proceedings of ACL. Rambow, O., Vijay-Shanker, K. and Weir, D.: 1995, D-Tree Grammars,

Proceedings of ACL. Rogers, J.: 1994a, Capturing CFLs with Tree Adjoining Grammars, Pro-

ceedings of ACL. Rogers, J.: 1994b, Studies in the Logic of Trees with Applications to

Grammar Formalisms, PhD thesis, University of Delaware. Rogers, J. and Vijay-Shanker, K.: 1992, Reasoning with descriptions of

trees, Proceedings of ACL. Schabes, Y.: 1990, Mathematical and Computational Aspects of Lexical-

ized Grammars, PhD thesis, University of Pennsylvania.

Shieber, S. M. and Schabes, Y.: 1990, Synchronous Tree-Adjoining Gram-

mars, Proceedings of COLING. Vijay-Shanker, K.: 1992, Using descriptions of trees in a tree adjoining

grammar, Computational Linguistics 18(4), 481–517. Vijay-Shanker, K. and Joshi, A. K.: 1988, Feature structures based tree

adjoining grammar, Proceedings of COLING, Budapest. Vijay-Shanker, K. and Schabes, Y.: 1992, Structure sharing in lexicalized

tree adjoining grammars, Proceedings of COLING, Nantes. Vijay-Shanker, K., Weir, D. J. and Joshi, A. K.: 1987, Characterizing

structural descriptions produced by various grammatical formalisms, Proceedings of ACL, Stanford.

Vijayashanker, K.: 1987, A Study of Tree Adjoining Grammars, PhD thesis, University of Pennsylvania.

SfS, Universität Tübingen, Wilhelmstr. 113, D-72074 Tübingen, Germany

E-mail address: lk@sfs.nphil.uni-tuebingen.de