Labelling and completeness for categorial resource logics

Natasha Kurtonina Research Institute for Language and Speech (OTS) Trans 10, 3512 JK Utrecht

Natasha.Kurtonina@let.ruu.nl

Abstract An important theme in current categorial research is the shift of emphasis from individual type logics to communicating families of such systems. The reason for this shift is that the individual logics are not expressive enough for realistic grammar development: the grammar writer needs access to the combined inferential capacities of a family of logics. See [Morrill 94], [Moortgat 95] for discussion and motivation. In line with these developments, our objective in this paper is to develop a uniform labelling discipline for the family of resource logics NL, L, NLP and LP and the generalizations discussed in depth in [K& M 95], and to establish a completeness result for the proposed labelling regime with respect to the general frame semantics for these logics. Our approach uses a generalization of our earlier [Kurtonina 94] completeness result for the ‘dynamic’ relational semantics of L which was based on a labelled deductive presentation of the logic.

1 Introduction: labelling for categorial type systems

Let us situate our approach with respect to related work, before starting with the technicalities. The technique of labelling has been used in the categorial literature before, for various reasons. [Buszkowski 86] used labelling as an auxiliary device to obtain his completeness results for the Lambek calculus. Victor Sanchez in [Sanchez 90] relied on labelling for semantic reasons in his work on a categoriallydriven theory of natural language reasoning. [Moortgat 91] added string labelling to type formulas for syntactic reasons, viz. to overcome the expressive limitations of the standard sequent language in capturing discontinuous forms of linguistic composition. In a proof theoretic study of categorial logics, [Roorda 91] introduced labelling to enforce the well-formedness conditions on proof nets. The programmatic introduction of Labelled Deductive Systems as a general framework for the study of structure sensitive consequence relations in [Gabbay 92] made it possible to reevaluate these scattered earlier proposals. From 1991 on, labelling has been on the categorial agenda on a more systematic level. For recent studies, we refer to [Morrill 94, Morrill 95], [Oehrle 94], [Hepple 94], [Venema 94], to mention just a few.

Consider a consequence relation

A_{1}, …, A_{n} ⇒ B

representing the fact that a conclusion B can be derived from a database of assumptions A_{1}, …, A_{n}. The central idea of the labelled deductive approach is to replace the formula as the basic declarative unit by a pair x : A, consisting of a label x and a formula A. Sequents then assume the form

x_{1} : A_{1}, …, x_{n} : A_{n} ⇒ y : B

The label is to be thought of as an extra piece of information added to the formula. Rules of inference manipulate not just the formula, but the formula plus its label. We then obtain a whole scala of labelling regimes depending on how we make precise the intuitive notion of an ‘extra piece of information added to a formula’ — depending on the degree of autonomy between the formula and the label.

At the conservative end of the spectrum one can find semantic lambda term labelling in the sense of the Curry-Howard correspondence. The labels, in this application, simply record the history of the proof — they do not make an independent contribution. At the other end of the spectrum are the labelling systems where in the declarative unit x : A the label x and the formula A each make their own irreducible contribution. Such systems can best be seen as combinations of two logics: the formula logic and the logic governing the labelling algebra.

Our proposals are somewhere in between these two extremes. In the application to linguistic reasoning which is the subject of this chapter, a consequence relation represents a grammaticality judgement: the derivability of an expression of type B from a database of assumptions, i.e. expressions of type A_{1}, …, A_{n}. Derivability, in this linguistic sense, has to take into account the structure of the assumptions — for example: their linear order, and the way they are grouped into hierarchical units or constituents. We rely on the labelling algebra to make the structure of our linguistic database explicit. In [K& M 95], we have seen how one obtains the systems L, NLP, LP from the pure residuation logic NL by removing order sensitivity, constituent structure sensitivity or both. In order to develop uniform algorithmic proof theory for this family of type logics we start from the multiset sequent presentation of their common denominator, the Lambek-Van Benthem system LP, and impose the extra syntactic fine-tuning in terms of the labelling regime.

Labelling, in this sense, is not uncommon in current categorial work, see for example [Morrill 94, Morrill 95] for descriptive and computational applications. But the labelling systems in use are related to groupoid interpretation, not to the more abstract ternary frame semantics which is the ‘common ground’ for the general completeness results for the various individual systems in the categorial landscape, and for the mixed multimodal logics. From the perspective of ternary frame semantics, the groupoid models are obtained by specializing the accessibility relation Rx, yz to x = y + z, where the binary operation + imposes functionality. The groupoid models become inappropriate when one wants to consider one-sided structural postulates (for example: left-associativity without right-associativity), rather than the two-way inferences for which the groupoid equational reasoning is appropriate^{1}. In developing labelling for the abstract ternary frame semantics, we can implement the labelling discipline in such a way that we can manipulate the three components of the triples (xyz) ∈ R, rather than assuming that x is determined by y + z.

Let us finally insist here on the importance of the completeness result for the labelled calculus. Labels, just like formulas, are pieces of syntax. Even if the rules of a labelled system look very much like imitating truth conditions we will never have a guarantee that the labelling is really appropriate for the intended interpretation unless we present a completeness proof, which requires an explicit statement of the relation between the labels and the objects of the domain of interpretation. That there are real issues here is shown in the discussion of [Venema 94].

1To accommodate one-way structural postulates, one can move to ordered groupoids, cf.

[Došen 88,89, Došen 92a], but in terms of ‘abstractness’ these would be on the same level as the general frame semantics adopted here.

The paper is organized as follows. In §2 we introduce uniform labelled sequent presentation for the logics NL, NLP, L, LP. We prove completeness with respect to the ternary frame semantics for these logics in §3. Labelled sequent calculus is presented in two formats which we show to be equivalent. The first format decorates formulas with atomic labels and enriches the sequent language with an explicit book-keeping component to record the structure of the database. The second format introduces a language of tree-terms over the atomic labels, and formulates the labelling discipline as a term assignment system. In §5, we discuss a number of generalizations, showing how our results can be applied to multimodal architectures, and to logics extended with one-place multiplicative operators. §6 then moves to concrete labelling. We use the labelling algebra to add sortal refinements to the type formulas: the sort labels filter out theorems that would be derivable in an unlabelled setting.

2 Resource management in labelled sequent calculus

Let us introduce the labelled sequent presentation informally before starting with the definitions. The new declarative unit, as we said before, now is the labelled formula x : A, rather than the bare formula A. What kind of labels do we want to use, and how do we want to interpret them? In our first version of the labelled calculus the labels are all taken from some set of atomic markers. In a sense to be made precise below, the labels refer to elements of the domain of interpretation W. In order to keep track of the way the labels are configured into a structured database, we add an explicit book-keeping component to the sequent language. Labelled sequents then will be of the general form

[δ]; a_{1} : A_{1}, a_{2} : A_{2}, …, a_{n} : A_{n} ⇒ a : A,

where each label a_{i}(1 ≤ i ≤ n) is a witness of a piece of information attached to A_{i} and d fixes the configuration of the labels in a tree such that the succedent label a is its root and the antecedent labels a_{i} the leaves. Because the configuration is fixed in δ the sequent antecedent can be treated simply as a multiset of labelled formulae. Now for the definitions.

Definition 2.1. Labels and trees. Let Lab be a set of atomic labels. We define by simultaneous induction the set of trees T over Lab and functions

root: T → Lab

leaves: T → P (Lab)

nodes: T → P (Lab)

• If x ∈ Lab, then x is a tree such that

leaves(x) = {x}

root(x) = x

nodes(x) = {x}

• If ⟨a, bc⟩ ∈ Lab^{3} and a, b, c are distinct, then ⟨a, bc⟩ is a tree such that

root(⟨a, bc⟩) = a

leaves(⟨a, bc⟩) = {b, c}

nodes(⟨a, bc⟩) = {a, b, c}

• If δ_{1} and δ_{2} are trees such that

root(δ_{2}) ∈ leaves(δ_{1}) and

nodes(δ_{1}) ∩ nodes(δ_{2})={root(δ_{2})}

then ξ=(δ_{1}δ_{2}) is a tree and

root(ξ)=root(δ_{1})

leaves(ξ)=(leaves(δ_{1}) ∪ leaves(δ_{2}))-{root(δ_{2})}

nodes(ξ)=nodes(δ_{1}) ∪ nodes(δ_{2})

Example 2.2. ξ=((⟨a, bc⟩⟨c, de⟩)⟨d, kn⟩) is a tree with

root(ξ)=a

leaves(ξ)={b, k, n, e}

nodes(ξ)={a, b, c, d, e, k, n}

Thus, each tree turns out to be a bracketed string of triangles. As usual we often drop the most external pair of brackets. The size (l) of a tree can be defined as follows:

• l(a) = 0

• l(⟨a, bc⟩) = 1

• l(ξχ) = l(ξ) + l(χ)

Now we can give precise definitions of a labelled formula and a labelled sequent.

• a : A is a labelled formula if A is a formula and a ∈ Lab;

• [δ]; a_{1} : A_{1}, a_{2} : A_{2}, …, a_{n} : A_{n} ⇒ a : A is a labelled sequent if a : A, a_{i} : A_{i}(1 ≤ i ≤ n) are labelled formulas, and δ ∈ T with

– root(δ)=a

– leaves(δ)={a_{1} … a_{n}}

Note that in a labelled sequent

[δ]; a_{1} : A_{1}, a_{2} : A_{2}, …, a_{n} : A_{n} ⇒ a : A

a_{1}, …, a_{n}, a are distinct since according to the definition all nodes of δ are distinct. Moreover the presence of δ is not conservative, since the rules of the labelled Lambek calculus include not only manipulations with formulas and labels, but also with trees.

We are in a position now to define the labelled sequent presentation first of all for the pure residuation logic NL, then for the systems with structural rules.

Definition 2.3. Labelled sequent calculus: the pure residuation logic NL^{lab}. Let α be a labelled formula, X, Y, Z finite multisets of labelled formulas, and let δ_{1}, δ_{2}, be members of T. NL^{lab} has one axiom

[a]; a : A ⇒ a : A

and the following inference rules, provided that all sequents involved are welldefined:

\frac{[δ_{1}]; X ⇒ b : A [δ_{2}]; c : B, Y ⇒ α}{[(δ_{2}⟨c, ba⟩)δ_{1}]; a : A → B, X, Y ⇒ α}

\frac{[⟨c, ba⟩d]; b : A, X ⇒ c : B}{[δ]; X ⇒ a : A → B}

\frac{[δ_{1}]; X ⇒ b : A [δ_{2}]; c : B, Y ⇒ α}{[(δ_{2}⟨c, ab⟩)δ_{1}]; a : A ← B, X, Y ⇒ α}

\frac{[⟨c, ab⟩d]; X, b : A ⇒ c : B}{[δ]; X ⇒ a : B ← A}

\frac{[d⟨a, bc⟩]; b : A, c : B, X ⇒ α}{[δ]; a : A • B, X ⇒ α}

\frac{[δ_{1}]; X_{1} ⇒ b : A [δ_{2}]; X_{2} ⇒ c : B}{[(⟨a, bc⟩δ_{1})δ_{2}]; X_{1}, X_{2} ⇒ a : A • B}

Definition 2.4. Structural rules as manipulations on labels. Structural options for resource management have the general format

\frac{[δ]; X ⇒ α}{[δ′]; X ⇒ α}

where δ′ is obtained from δ via an operation matching the structural rule in question. Specifically, L^{lab} can be obtained from NL^{lab} by adding the Associativity Rule that δ′ is obtained from δ by replacing some subtree (⟨a, bc⟩⟨c, de⟩) by a tree (⟨a, te⟩⟨t, bd⟩) or vice versa provided that t (resp. c) is fresh. NLP^{lab} can be obtained from NL^{lab} by adding the Permutation Rule that δ′ is obtained from δ by replacing some subtree (⟨a, bc⟩) by a tree (⟨a, cb⟩). Finally, LP^{lab} is obtained from NL^{lab} by adding both Associativity and Permutation.

The following sequents give an example of theorems of NL^{lab}.

\begin{matrix}(i) & [\{⟨x, bc⟩, ⟨d, ax⟩\}]; a : r ← q, b : p, c : p → q ⇒ d : r \\ (ii) & [\{⟨x, bc⟩, ⟨n, ax⟩\}]; a : r ← q, b : p, c : p → q ⇒ n : r \end{matrix}

Note that the derivation of (ii) can be obtained from the derivation of (i) by renaming d for n.

Lemma 2.5. Renaming Lemma. The Lemma consists of two claims.

• Claim 1.

If a sequent [δ]; x_{1} : X_{1}, x_{2} : X_{2}, …, x_{n} : X_{n} ⇒ x : X is derivable, then [δ′]; x_{1} : X_{1}, …, y : X_{i}, …, x_{n} : X_{n} ⇒ x : X where δ′ is obtained from δ by replacing x_{i} by y is also derivable.

• Claim 2.

If a sequent [δ]; x_{1} : X_{1}, x_{2} : X_{2}, …, x_{n} : X_{n} ⇒ x : X is derivable then [δ]; x_{1} : X_{1}, x_{2} : X_{2}, …, x_{n} : X_{n} ⇒ y : X where δ′ is obtained from δ by replacing x by y is also derivable.

Both Claims can be proved by straightforward induction on the length of the derivation. □

interpreting labelled sequents. To obtain an interpretation for our labelled sequents we add to a ternary model ⟨W, R, V ⟩ a function ^{∗} which assigns exactly one element of W to each a ∈ Lab.

A sequent [δ]; a_{1} : A_{1}, a_{2} : A_{2}, …, a_{n} : A_{n} ⇒ a : A is true in M if a^{∗} ⊧ A whenever a_{i}^{∗} ⊧ A_{i}(1 ≤ i ≤ n) and for each triangle ⟨x, yz⟩ which occurs in δ, Rx*,y*z* . A sequent ϕ is semantically valid if it is true in all models.

Note that although on the syntactic level the labels on the nodes of each triangle are distinct, we do not impose such distinctness as a semantic requirement. Since ^{∗} is an arbitrary function it might very well be that in some models the same elements of the domain are assigned to distinct node labels of the syntactic tree. Thus on the semantic level the definition of a ternary frame realizes an arbitrary ternary accessibility relation as required.

As usual it is easy to prove soundness, i.e. each sequent derivable in NL^{lab} is semantically valid. Completeness is the subject of the following section.

3 Labelling and completeness

We establish completeness of the labelling regime first for NL^{lab}, then for the systems with extra resource management properties. The general idea behind the completeness proof can be expressed as follows:

1. Suppose [δ]; a_{1} : A_{1}, a_{2} : A_{2}, …, a_{n} : A_{n} ⇒ a : A is not derivable in NLlab.

2. Mark all labelled formulas on the left hand side with T and a : A with F. The resulting T-F set is

Δ_{0} = {T a_{1} : A_{1}, …, T a_{n} : A_{n}, F a : A}.

Construct a model such that each a_{i}^{∗} supports A_{i}, but a^{∗} does not support A. In other words, extend Δ_{0} to Δ and prove that x^{∗} ⊧ X iff T x : X ∈ Δ.

To realize this idea of the completeness proof we need to identify some properties of T − F sets, i.e sets of labelled formulas marked with T or F.

properties of T-F sets. Let Δ be a T − F set, V_{Δ} the set of all labels that occur in Δ, Δ_{R} the set of all triangles associated with Δ, and δ ∈ T (i.e. δ is a tree). We loosely say that δ ⊆ Δ_{R} if all triangles that occur in δ are members of Δ_{R}.

• Δ is deeply consistent (d.c.) iff whenever δ ⊆ Δ_{R} , γ_{1}, …, γ_{k} are T -members of Δ and [δ]; γ_{1}, …, γ_{k} ⇒ γ is derivable, then F γ ∉ Δ.

• Δ is h-complete (Henkin complete) iff

(i) if F a : A → B ∈ Δ, then there are x, y ∈ V_{Δ} such that ⟨y, xa⟩ ∈ Δ_{R}, T x : A ∈ Δ and F y : B ∈ Δ;

(ii) if F a : A ← B ∈ Δ, then there are x, y ∈ V_{Δ} such that ⟨y, ax⟩ ∈ Δ_{R}, T x : A ∈ Δ and F y : B ∈ Δ;

(iii) if T a : A • B ∈ Δ, then there are x, y ∈ V_{Δ} such that ⟨a, xy⟩ ∈ Δ_{R}, T x : A ∈ Δ and T y : B ∈ Δ.

• Δ is r-complete (relatively complete) iff (i) if F a : A • B ∈ Δ and ⟨a, xy⟩ ∈ Δ_{R}, then

either F x : A ∈ Δ or F y : B ∈ Δ; (ii) if T a : A → B ∈ Δ and ⟨y, xa⟩ ∈ Δ_{R}, then

either F x : A ∈ Δ or T y : B ∈ Δ; (iii) if T a : A ← B ∈ Δ and ⟨y, ax⟩ ∈ Δ_{R}, then

either F x : A ∈ Δ or T y : B ∈ Δ.

• Δ is nice iff it is d.c., h-complete, r-complete

• Let Δ be a T-F set, x ∈ V_{Δ} and A be a non-labelled formula. We say that A and x are linked in Δ iff T x : A ∈ Δ or F x : A ∈ Δ.

Henkin model. Lemma 3.1. If Δ is a nice T − F set, then there exists a model M′ = ⟨W, R,^{∗} , V ⟩ such that if x ∈ V_{Δ} and X are linked in Δ, then T x : X ∈ Δ iff x^{∗} ⊧ X in M′. proof. Define M′ as follows:

W = V_{Δ} (the set of all labels that occur in Δ); Rx, yz iff ⟨x, yz⟩ ∈ Δ_{R}. for all x ∈ V_{Δ}, x^{∗} = x V is such that T x : p ∈ Δ iff x^{∗} ⊧ p in M′.

The lemma is proved by induction on the length of X. In the atomic case the claim is a direct consequence of the definition. We have to take care of three cases when proving the inductive step.

The first case: X = A • B.

1. Suppose T a : A • B ∈ Δ.

2. Since Δ is h-complete there are x, y ∈ V_{Δ} such that ⟨a, xy⟩ ∈ Δ_{R}, T x : A ∈ Δ and T y : B ∈ Δ.

3. Therefore Ra, xy; x ⊧ A and y ⊧ B (by inductive assumption) and a ⊧ A • B 4. Thus a^{∗} ⊧ A • B

1. Suppose a^{∗} ⊧ A • B and therefore a ⊧ A • B.

2. Then there are x, y ∈ W such that Ra, xy; x ⊧ A and y ⊧ B.

3. Since a and A • B are linked in Δ, either T a : A • B ∈ Δ or F a : A • B ∈ Δ. Let us suppose that F a : A • B ∈ Δ.

4. Since Δ is r-complete, F a : A•B ∈ Δ and ⟨a, xy⟩ ∈ Δ_{R} (because Ra, xy) imply that either F x : A ∈ Δ or F y : B ∈ Δ; in both cases we get a contradiction with [2.]. Thus T a : A • B ∈ Δ.

The second case: X = A → B 1. Suppose T a : A → B ∈ Δ.

2. Suppose Rc, ba and b ⊧ A 3. Then ⟨c, ba⟩ ∈ Δ_{R} and T b : A ∈ Δ

4. Since Δ is r-complete, [1.] [2.] and [3.] imply T c : B ∈ Δ, and therefore by the inductive assumption c ⊧ B

5. Hence, a^{∗} ⊧ A → B

1. Suppose a^{∗} ⊧ A → B

2. Suppose T a : A → B ∉ Δ. Then since a and A → B are linked in Δ, F a : A → B ∈ Δ

3. By h-completeness of Δ, there are b, c ∈ V_{Δ} such that T b : A ∈ Δ, F c : B ∈ Δ and ⟨c, ba⟩ ∈ Δ_{R}

4. By inductive assumption, get a contradiction.

Therefore T a : A → B ∈ Δ

The third case can be left to the reader □

Lemma 3.1 enables one to claim that if a sequent u : A ⇒ u : B is not derivable and the corresponding T − F set {T u : A, F u : B} can be extended to a nice one, then there exists a model where u : A ⇒ u : B is falsified. Now we have to define how to make the relevant extensions of d.c. sets. We start with the definition of saturation with h-witnesses and then r-witnesses.

harmless witnesses. Formulas of the form F a : A → B, F a : A ← B, T a : A•B will be called h-formulas (Henkin formulas). Let Δ be a d.c. set. By adding hwitnesses we refer to the following procedure:

(i) if F a : A → B ∈ Δ, then add new labels b and c to V_{Δ}; ⟨c, ba⟩ to Δ_{R} and new labelled formulas T b : A and F c : B to Δ;

(ii) if F a : A ← B ∈ Δ, then add new labels b and c to V_{Δ} ; ⟨c, ab⟩ to Δ_{R} and new labelled formulas T b : A and F c : B to Δ;

(iii) if T a : A • B ∈ Δ, then add new labels b and c to V_{Δ}; ⟨a, bc⟩ to Δ_{R} and new labelled formulas T b : A and T c : B to Δ.

We say that in (i)-(iii) the point a generates points b and c. The set of successors of a point x (Σ_{x}) is defined by (iv)-(v):

(iv) if x generates y, then y ∈ Σ_{x};

(v) if u ∈ Σ_{x} and u generates w, then w ∈ Σ_{x}.

To saturate some T − F set Δ with r-witnesses perform (i)-(iii)

(i) if F a : A • B ∈ Δ and ⟨a, xy⟩ ∈ Δ_{R}, then add F x : A to Δ if it does not disturb d.c. of Δ, otherwise add F y : B

(ii) if T a : A → B ∈ Δ and ⟨y, xa⟩ ∈ Δ_{R}, then add F x : A to Δ if it does not disturb d.c. of Δ, otherwise add T y : B

(iii) if T a : A ← B ∈ Δ and ⟨y, ax⟩ ∈ Δ_{R}, then add F x : A to Δ if it does not disturb d.c. of Δ, otherwise add T y : B.

Formulas of the form F a : A•B, T a : A → B, T a : A ← B will be called r-formulas. We say that an r-formula F a : A • B (resp. T a : A → B, T a : A ← B) is active in Δ if there are b, c ∈ V_{Δ} such that ⟨a, bc⟩ ∈ Δ_{R} (resp. ⟨c, ba⟩ ∈ Δ_{R}, ⟨c, ab⟩ ∈ Δ_{R}).

Let Δ be a T − F set, V_{Δ} be a set of labels that occur in Δ and Δ_{R} be a set of triangles associated with Δ such that each member of Δ_{R} is a result of some h-decomposition. Then the following propositions hold.

Proposition 3.2. If x ∈ V_{Δ} and X is the set of all successors of x, then all members of X are distinct.

proof. Direct consequence of the definition of adding h-witnesses. □

Proposition 3.3. If δ ⊆ Δ_{R}, then δ is generated by a single point.

proof. Straightforward induction on the size of δ. Indeed, if δ = ⟨a, bc⟩, then it is generated by a single point according to the definition of adding h-witnesses.

claim If δ = ξ_{1}ξ_{2}, and x is their common point, then either ξ_{1} or ξ_{2} is generated by x proof. If in both ξ_{1} and ξ_{2} x is a generated point, then x has to be generated twice: as a daughter and as a root, which is not possible, since by the definition of adding h-witnesses every point in Δ_{R} is uniquely generated. Thus, at least in one of this trees x is a generator.

Next, suppose δ = ξ_{1}ξ_{2}, x is their common point, and ξ_{i} is generated by x, while ξ_{j} (i, j = 1, 2) is generated by y. Then either x = y or x is a successor of y or vice versa. In all this cases δ = ξ_{1}ξ_{2}, is generated by a single point. □

Proposition 3.4. Let δ_{1}, δ_{2} ⊆ Δ_{R} with root (δ_{2}) ∈ leaves (δ_{1}). Then δ_{1}δ_{2} ⊆ Δ_{R}

proof. We have to show that δ_{1}δ_{2} is a well defined tree, or in other words, that δ_{1} and δ_{2} have no other points in common besides x. Reasoning by analogy with the proof of the Proposition 3.3, conclude, that x generates δ_{1} or δ_{2} or both of them. If x generates δ_{1} and y generates δ_{2}, then no matter if x is a successor of y or vice versa, the successor would always generate fresh points , therefore δ_{1} and δ_{2} can not share any points besides x. If x generates both δ_{1} and δ_{2}, then in one case the set of successors would be generated by x as a root (and therefore, by a formula of the form T a : A • B) while the second set would be generated by x as a daughter (and therefore by formula of the form F a : A → B or F a : A ← B), thus two latter sets can not share any members. □

Lemma 3.5. Let Δ be a d.c. set, and each member of Δ_{R} is a result of some hdecomposition. If β is an active r-formula in Δ, then there always exists an r-witness of β which can be added to Δ without disturbing its deep consistency.

proof

The first case: F a : A • B ∈ Δ

Let β be F a : A • B and ⟨a, bc⟩ ∈ Δ_{R}. Suppose that neither Δ + F b : A, nor Δ + F c : B is d.c. Then clearly

(1) there exist δ_{1} ⊆ Δ_{R} and T-members of Δ γ_{1}, …, γ_{n} such that

(∗) [δ_{1}]; γ_{1}, …, γ_{n} ⇒ γ

is derivable in NLlab and γ is an F-member of Δ + F b : A. Since Δ is d.c., γ is nothing else but b : A;, and (∗) has actually the form

(∗) [δ_{1}]; γ_{1}, …, γ_{n} ⇒ b : a

Thus, b is the root of δ_{1}

(2) there exist δ_{2} ⊆ Δ_{R} and T-members of Δ α_{1}, …, α_{n} such that

(∗∗) [δ_{2}]; α_{1}, …, α_{n} ⇒ α

is derivable in NLlab and α is an F-member of Δ + F c : B. Once again, since Δ is d.c., α is nothing else but c : B; whence

(∗∗) [δ_{2}]; α_{1}, …, α_{n} ⇒ c : B

is derivable and therefore c is the root of δ_{2}

According to Proposition 3.4 (⟨a, bc⟩δ_{1})δ_{2} is a well defined tree, thus by (1) and (2)

[(⟨a, bc⟩δ_{1})δ_{2}]; γ_{1}, …, γ_{k}, α_{1}, …, α_{n} ⇒ A • B

is derivable. Since (⟨a, bc⟩δ_{1})δ_{2} ⊆ Δ_{R} and γ_{1}, …, γ_{k}, α_{1}, …, α_{n} are T-members of Δ but a : A • B is an F-member of Δ, Δ can not be d.c..

The second case: T a : A → B ∈ Δ

Let T a : A → B ∈ Δ and ⟨c, ba⟩ ∈ Δ_{R}. Suppose neither Δ + F b : A nor Δ + T c : B is d.c. Then clearly

(1) there exist δ_{1} ⊆ Δ_{R} and T-members of Δ γ_{1}, …, γ_{k} such that

[δ_{1}]; γ_{1}, …, γ_{k} ⇒ γ

is derivable in NLlab and γ is an F-member of Δ + F b : A. Since Δ is d.c., γ is obviously b : A;

(2) there exist δ_{2} ⊆ Δ_{R} and T-members of Δ + T c : B α_{1}, …, α_{n} such that

[δ_{2}]; α_{1}, …, α_{n} ⇒ α

is derivable in NLlab and α is an F-member of Δ. Since Δ is d.c., there exists an index i such that α_{i} coincides with c : B;

Clearly c is a leaf of δ_{2} and b is a root of δ_{1}. According to Proposition 3.4 (δ_{2}⟨c, ba⟩)δ_{1} is a well defined tree. Therefore the sequent

[(δ_{2}⟨c, ba⟩)δ_{1}]; α_{1}, …, α_{i−1}, γ_{1}, …, γ_{k}, a : A → B, α_{i+1}, …, α_{n} ⇒ α

turns out to be derivable and Δ can not be d.c..

The last case (α := T b : A ← B) is left to the reader. □

Lemma 3.6. Adding h-witnesses does not disturb d.c.. proof. Suppose F a : A → B belongs to a d.c. set Δ. Suppose that adding ⟨c, ba⟩ (where b and c are fresh) to Δ_{R} and adding T b : A and F c : B to Δ does disturb d.c.. Therefore, there exists a derivable sequent

(♯) [δ]; γ_{1}, …, γ_{n} ⇒ γ

such that δ ⊆ Δ_{R} ∪ {⟨c, ba⟩}; γ_{1}, …, γ_{n} are T-members of Δ + T b : A and γ is an F-member of Δ + F c : B. Note, that if ⟨c, ba⟩ does not occur in δ, then Δ is not d.c.. Thus δ = ⟨c, ba⟩δ_{1}, for some δ_{1} ⊆ Δ_{R}, moreover b and c can occur only once in a tree, generated by δ. Therefore γ coincides with c : B and γ_{1} coincides with b : A, hence the sequent (♯) has actually the form

[⟨c, ba⟩δ_{1}]; b : A, γ_{2}, …, γ_{n} ⇒ c : B

Thus

[δ_{1}]; γ_{2}, …, γ_{n} ⇒ a : A → B

is also derivable, and since δ_{1} ⊆ Δ_{R}, γ_{1}, …, γ_{n} are T-members of Δ, and a : A → B is an F-member of Δ, Δ can not be d.c.. In the case of adding h-witnesses of F a : B ← A or T a : A • B our argument would not be much different. □

completeness proof: from deeply consistent sets to nice sets. Recall our initial assumption: a : A ⇒ a : B is not derivable in NL^{lab}. Define Δ_{0}, … Δ_{n}, … (n ∈ N) as follows:

Δ_{0} = {T a : A, F a : B}.

Δ_{n+1}: add all possible h-witnesses to Δ_{n}, corresponding triangles to Δ_{R_{n}}

Δ_{n+2}: add all possible r-witnesses to Δ_{n+1}.

By Lemma 3.5 and Lemma 3.6, Δ = ∪Δ_{i}(i ∈ N) is nice. Now our Completeness Theorem becomes just a direct consequence of the previous results.

Completeness theorems for NLP^{lab}, L^{lab} and LP^{lab} require the additional proof that taking the associative or permutational closure of some d.c. set does not disturb its deep consistency. But this is guaranteed due to the presence of the corresponding structural rule in the sequent presentation of the labelled version of the Lambek Calculus. Note, that the Cut rule was not used in our completeness proof, which means that we have obtained semantical proof of Cut Elimination theorem. For the constructive procedure of Cut Elimination we refer to [Kurtonina 95].

4 Labelling with Kripke tree terms

The labelling preceding subsection decorated the formulas always with atomic labels: the structure of the database was accounted for by adding to the sequent language an explicit representation of the tree configuration of the atomic labels. The alternative labelling regime to be introduced below has a term language to build structured labels out of the atomic labels. The term language now directly captures the structure of the database, so that we can remove the book-keeping component from the sequent language.

Definition 4.1. Elementary tree terms, tree terms, proper tree terms.

(i) If x ∈ Lab, then x is an elementary tree term

(ii) If χ is an elementary tree term, then χ is a tree term;

(iii) If ξ, χ are tree terms and x ∈ Lab,, then r(x, ξ, χ) is a tree term.

A tree term t is called proper if all its elementary subterms are distinct. We define the size (l) of the tree term as follows:

(i) if x is an elementary tree term, then l(x) = 0

(ii) l(r(x, ξ, χ)) = l(ξ) + l(χ) + 1

Example r(a, r(x, r(y, bc), d)e) is a proper tree term which corresponds to the following tree: (⟨a, xe⟩⟨x, y, d⟩)⟨y, b, c⟩.

To prove that each proper tree term corresponds to some tree and vice versa, one proceeds by induction on the length of a tree term for one direction and on the length of a tree for the other one.

Definition 4.2. Labelled sequents with Kripke tree terms. Let a, b, c be elementary tree terms, and t, u, v proper tree terms. A labelled sequent is an expression of the form

a_{1} : A_{1}, a_{2} : A_{2}, …, a_{n} : A_{n} ⇒ t : A

where each a_{i}(1 ≤ i ≤ n) is an elementary tree term and t is a proper tree term.

Definition 4.3. Labelled sequent calculus. Let X, Y be finite multisets of formulas labelled with elementary tree terms. And let a, b, c be elementary tree terms, t, u, v proper tree terms as before. We write t = t′[u/v] if t is obtained from the proper tree term t′ by replacing the subterm v by u.

The labelled sequent presentation for the basic system NLlab has one axiomscheme and the following inference rules:

a : A ⇒ a : A

\frac{X ⇒ t_{1} : A  c : B, Y ⇒ t_{2} : α}{a : A → B, X, Y ⇒ t : α}  \frac{b : A, X ⇒ r(c, bt) : B}{X ⇒ t : A → B}
where t = t_{2}[r(c, t_{1}a)/c]

\frac{X ⇒ t_{1} : A  c : B, Y ⇒ t_{2} : α}{a : A ← B, X, Y ⇒ t : α}  \frac{b : A, X ⇒ r(c, bt) : B}{X ⇒ a : B ← A}
where t = t_{2}[r(c, at_{1})/c]

\frac{b : A, c : B, X ⇒ t_{1} : α}{a : A • B, X ⇒ t : α}  \frac{X_{1} ⇒ t_{1} : A  X_{2} ⇒ t_{2} : B}{X_{1}, X_{2} ⇒ r(a, t_{1}t_{2}) : A • B}
where t = t_{1}[a/r(a, bc)]

As before, one obtains labelled presentation for the systems L, NLP and LP by adding Associativity, Permutation or their combination:

\frac{X ⇒ t : A}{X ⇒ t′ : A}

where (Associativity) t′ can be obtained from t by replacing a subterm r(a, t_{1}, r(b, t_{2}t_{3})) by a tree term r(a, r(c, t_{1}t_{2})t_{3}), provided that c is fresh, or (Permutation) where t′ can be obtained from t by replacing a subterm r(a, t_{1}t_{2}) by a tree term r(a, t_{2}t_{1}).

Clearly via translation of proper tree terms into trees and vice versa one can easily prove the equivalence of the two formulations of the Lambek Calculus. A direct consequence of this fact is soundness and completeness of the Lambek Calculus with tree terms as labels with respect to ternary relation semantics.

5 Generalizations

In the preceding section we have looked at the systems NL, L, NLP, LP and presented uniform labelled sequent calculus for these logics, with completeness results for the relevant classes of ternary frames. The methods used are quite general: they can be straightforwardly applied to a number of related systems. Two generalizations seem especially relevant in view of current linguistic applications: the move from unimodal to multimodal architectures, and the introduction of unary multiplicative operators in addition to the familiar binary ones. We discuss these in turn.

5.1 Multimodal architectures

In the preceding paragraphs, we have studied the systems NL, L, NLP, LP in isolation: each of these systems characterizes a distinct resource management regime in terms of a package of structural rules — rules for the manipulation of labels in our labelled presentation. It has been argued in the linguistic literature (see for example [Moort. & Morrill 91], [Moort. & Oehrle 94], [Morrill 94] and [Moortgat 95] that for purposes of actual grammar development, one wants to have access to the combined inferential capacity of these various systems.

On the model-theoretic level, such a mixed style of inference requires a move from unimodal frames ⟨W, R⟩ to multimodal frames ⟨W, {R_{i}}_{i∈I}⟩. We now distinguish a family of accessibility relations: each of these R_{i} can have its own individual resource management properties, or if R_{i} and R_{j} have the same resource management regime they can still be kept distinct in virtue of their indexes i and j. On the syntactic level, we also index the connectives with i ∈ I, so that we can interpret each •_{i} (and its residual implications →_{i} and ←_{i}) in terms of its own accessibility relation R_{i}. Structural postulates, and the corresponding frame conditions, are relativized to the mode indexes. Apart from the standard structural options differentiating NL, L, NLP and LP, the multimodal architecture supports mixed forms, where Associativity or Commutativity apply when two modes are in construction with each other. Such mixed structural principles greatly enhance the linguistic expressivity of the framework. See [Moort. & Oehrle 94], [Morrill 94] for concrete illustrations. We will treat the labelled version of such principles in a moment.

Our framework for labelled deduction directly accommodates the multimodal categorial architecture. We sketch the necessary changes for the tree term labelling. In the definition of tree terms, we now have a family of term constructors r_{i} instead of the one r of the unimodal setting

Definition 5.1. Multimodal systems: elementary tree terms, tree terms, proper tree terms. Let Lab, be a set of atomic markers, as before, and I a set of resource management mode indices.

(i) If x ∈ Lab, then x is an elementary tree term

(ii) If χ is an elementary tree term, then χ is a tree term;

(iii) If ξ, χ are tree terms , x ∈ Lab, and i ∈ I, then r_{(}x, ξ, χ) is a tree term.

Similarly, in the definition of the multimodal labelled sequent calculus, we harmonize the mode information on the connectives and on the associated tree term labels. Below the logical rules for the connectives.

\frac{X ⇒ t_{1} : A  c : B, Y ⇒ t_{2} : α}{a : A →_{i} B, X, Y ⇒ t : α}  \frac{b : A, X ⇒ r_{i}(c, bt) : B}{X ⇒ t : A →_{i} B}
where t = t_{2}[r_{i}(c, t_{1}a)/c]

\frac{X ⇒ t_{1} : A  c : B, Y ⇒ t_{2} : α}{a : A ←_{i} B, X, Y ⇒ t : α}  \frac{b : A, X ⇒ r_{i}(c, bt) : B}{X ⇒ a : B ←_{i} A}
where t = t_{2}[r_{i}(c, at_{1})/c]

\frac{b : A, c : B, X ⇒ t_{1} : α}{a : A •_{i} B, X ⇒ t : α}  \frac{X_{1} ⇒ t_{1} : A  X_{2} ⇒ t_{2} : B}{X_{1}, X_{2} ⇒ r_{i}(a, t_{1}t_{2}) : A •_{i} B}
where t = t_{1}[a/r_{i}(a, bc)]

The structural rules, in the multimodal setting, are mode restricted: they refer to specific resource management mode labels. Our earlier versions of Associativity and Permutation would now assume the following form (for obvious mode labels).

\frac{X ⇒ t : A}{X ⇒ t′ : A} (†)

• Associativity Rule: (†) where t′ = t[r_{ass}(a, r_{ass}(c, t_{1}t_{2})t_{3})/r_{ass}(a, t_{1}, r_{ass}(b, t_{2}t_{3}))], provided that c is fresh.

• Permutation Rule: (†) where t′ = t[r_{perm}(a, t_{2}t_{1})/r_{perm}(a, t_{1}t_{2})].

Apart from these familiar unimodal structural options, our language is now expressive enough to also formulate mixed version for situations where different modes are in construction with each other. As an illustration, we present versions of Mixed Associativity and Mixed Commutativity for communication between modes i and j. The structural postulates are as follows.

Mixed Commutativity A •_{i} (B •_{j} C) ⊢ B •_{j} (A •_{i} C)
Mixed Associativity  A •_{i} (B •_{j} C) ⊢ (A •_{i} B) •_{j} C)

Translated in the labelling format, these structural postulates become rules for manipulating term labels:

• Mixed Associativity Rule: (†) where t′ = t[r_{j}(a, r_{i}(c, t_{1}t_{2})t_{3})/r_{i}(a, t_{1}, r_{j}(b, t_{2}t_{3}))] , provided that c is fresh.

• Mixed Permutation Rule: (†) where t′ = t[r_{j}(a, t_{2}r_{i}(c, t_{1}t_{3}))/r_{i}(a, t_{1}, r_{j}(b, t_{2}t_{3}))].

For a linguistic application of this type of communication principle, the reader can turn to [Moort. & Oehrle 94], who give a multimodal analysis of head-adjunction phenomena such as can be found in the Germanic Verb-Raising construction. In a sentence such as

dat Jan (een boek (wil lezen)) (that J. a book wants read) i.e. that John wants to read a book the verb ‘wil’ (want) has to be combined semantically with the combination of the main verb ‘lezen’ (read) and its direct object ‘een boek’ (a book). But on the syntactic level, ‘wil’ does not combine with the phrase ‘een boek lezen’ but just with its head, viz. ‘lezen’. Let the main verb combine with its arguments in mode i, and the modal auxiliary ‘wil’ in mode j, then the Mixed Commutativity rule makes it possible to proceed from the surface syntactic organization to the configuration required for semantic interpretation.

5.2 Unary multiplicatives

The labelling method and completeness proof of the previous sections was formulated for families of binary residuated connectives and their ternary accessibility relation. Residuation can be generalized to n-ary families of connectives interpreted with respect to n + 1-ary accessibility relations, [Dunn 91] for an excellent survey, and [Moortgat 95, K& M 95] for the categorial application. Our labelling approach can be applied straightforwardly in the generalized residuation setting.

Especially relevant for the linguistic applications is the case of unary residuated operators, interpreted with respect to a binary accessibility relation. The basic residuation pattern for the unary operators assumes the following form:

◇A ⇒ B iff A ⇒ □^{↓}B

Semantically, we have the usual truth conditions below:

\begin{matrix}x ⊧ ◇A iff ∃y(Rxy & y ⊧ A) \\ x ⊧ □^{↓}A iff ∀y(Ryx ⇒ y ⊧ A) \end{matrix}

Definition 5.2. Labelled sequent calculus: unary residuated connectives. Labelled sequent presentation for unary multiplicatives requires a generalization of the notion of a tree term to include binary tree terms built with the constructor r^{2} next to the ternary case we had before: if ξ is a tree terms, x ∈ Lab, then r^{2}(x, ξ) is a tree term. The logical rules for the new connectives ◇, □^{↓} then assume the following form.

\frac{b : A, X ⇒ t_{1} : B}{a : □^{↓}A, X ⇒ t : B}  \frac{X ⇒ r^{2}(a, t) : A}{X ⇒ t : □^{↓}A}
where t = t_{1}[r^{2}(b, a)/b]

\frac{b : A, X ⇒ t_{1} : B}{a : ◇A, X ⇒ t : B}  \frac{X ⇒ t : A}{X ⇒ r^{2}(a, t) : ◇A}
where t = t_{1}[a/r^{2}(a, b)]

6 Concrete uses of labelling: sortal refinement

The use of labelling in the previous sections is still on the conservative side: we have given a uniform presentation for a family of categorial type logics with different resource management properties by introducing a division of labour between the sequent language and the labelling discipline: the sequent language is kept uniform, and the syntactic fine-tuning is taken care of by the labels.

In this section we want to give a very simple illustration of a form of labelling where the label has acquired a greater degree of independence from the formula, i.e. where the label allows one to incorporate additional information relevant to the process of linguistic inference. We show how one can decorate simple type assignment with labels capturing morphophonological sortal information. The sortal decoration makes it possible to rule out derivations that would go through if we restricted the attention to unlabelled type assignments.

Compare the adjective modifier very and the prefix un-. On the syntactic level, they are both functors taking adjectives into adjectives. We could assign them the type a ← a and type a to happy. But given this type assignment both the grammatical very unhappy and the ungrammatical un-very happy are derivable according to the scheme

a ← a, a ← a, a ⇒ a

Can we refine the type assignment in such a way as to take into account the different combinatory possibilities of affix, words, and phrases? To block the undesired derivation and to keep the desired one we decorate the type formulas with sort labels, characterizing very and happy as syntactic words and un- as an affix. Our assignments in labelling format could take the form

very  word : a ← a
un-  affix : a ← a
happy  word : a

Moreover, we have to impose constraints on the composition relation in order to characterize the well-formed combinations on the morphophonological sort level:

(i) ⟨word, affix word⟩ (ii) ⟨phrase, word phrase⟩ (iii) ⟨phrase, word word⟩

Next, to express the fact that a syntactic word can do the duty as a phrasal expression (but not vice versa, of course) we adopt the following rule:

Let Ψ be a set of constraints and a triangle δ ∈ Ψ has a root –word, then there exists δ′ ∈ Ψ with the same leaves as δ and with the root–phrase.

In our case that means that (i) adds one more triangle to the set of constraints:

(i′) ⟨word, affix word⟩

Now using suitable abbreviations and marks to distinguish tree points we can present a derivation of very unhappy:

\frac{\underline{ph_{1} : a ⇒ ph_{1} : a  ph_{2} : a ⇒ ph_{2} : a} ; w_{1} : a ⇒ w_{1} : a  [⟨ph_{2}, w_{2}ph_{1}⟩]w_{2} : a ← a, ph_{1} : a ⇒ ph_{2} : a}{[⟨ph_{2}, w_{2}ph_{1}⟩⟨ph_{1}, afw_{1}⟩]; w_{2} : a ← a, af : a ← a, w_{1} : a ⇒ ph_{2} : a}

On the other hand un- very unhappy turns out to be underivable since our constraints on composition relation do not allow to combine affix with phrase.

Formally passing from the abstract style of labelling to the concrete style exemplified here we have to specify the definition of a model ⟨W, R, V ⟩ of interpretation by taking W as a set of sorts and imposing frame constraints on R which are indicated above.

Thus on the level of interpretation, filtering out derivations that would be valid in the non-labelled setting is realized by restricting the class of all ternary models to those satisfying the constraints formulated above.

As we remarked at the beginning of this paragraph, our objective here was just to provide a simple illustration of ‘autonomous’ forms of labelling. For an elaboration of this style of labelling on a much more fundamental and wide-ranging level, we can refer to Ruth Kempson’s work on combining syntactic and semantic inference [Kempson 95].

7 Conclusion

Our main objective in this paper has been to develop a uniform labelling regime for the landscape of categorial resource logics, and to establish completeness of the labelling discipline with respect to the general frame semantics. As remarked at the beginning of this paper, in computational studies of categorial grammar, labelling is often introduced as a tool to obtain efficient parsing strategies. We leave it as a topic for further research how the general labelling method developed in this paper can be combined with the compilation techniques of [Morrill 95] that allow for efficient checking of subproblems of the general labelling problem in terms of optimal data-structures.

References

[Buszkowski 86] W. Buszkowski (1986), ‘Completeness Results for Lambek Syntactic Calculus’, Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 32, 13-28

[Došen 88,89] K. Došen (1988,1989) “Sequent systems and groupoid models”. Studia Logica 47, 353-385, 48, 41-65.

[Došen 92a] K. Došen (1992), “A brief survey of frames for the Lambek calculus”. Zeitschr. f. math. Logik und Grundlagen d. Mathematik 38,179-187

[Došen 92b] K. Došen (1992) “Modal translations in substructural logics”. Journal of Philosophical Logic 21, 283-336.

[Dunn 91] J. M. Dunn (1991), “Gaggle theory: an abstraction of Galois connections and residuation, with applications to negation, implication, and various logical operators’. In Van Eijck (ed.) Logics in AI. JELIA Proceedings. Springer, Berlin.

[Gabbay 92] D. Gabbay (1992), Labelled Deductive Systems. Summer School of Logic, Language and Information. Essex 1992.

[Hepple 90] M. Hepple (1990) The Grammar and Processing of Order and Dependency: A Categorial Approach. PhD Dissertation, University of Edinburgh.

[Hepple 94] M. Hepple (1994) Labelled Deduction and Discontinuous Constituency. In ‘Linear Logic and Lambek Calculus”, Proceedings 1993 Rome Workshop

[Kempson 95] R. Kempson (1995), “Ellipsis: a natural deduction perspective”. In Kempson (ed) Language and Deduction, IGPL Bulletin, Vol 3 (2,3).

[Kurtonina 94] N. Kurtonina (1994), The Lambek Calculus, Relational Semantics and the Method of Labelling. To appear in Studia Logica.

[Kurtonina 95] N. Kurtonina (1995), ‘Talking about explicit databases in Categorial Grammar’. Bulletin of the IGPL, Vol 3 (2,3), pp 357–370.

[K& M 95] N. Kurtonina and M. Moortgat (1995), “Structural Control”. This volume. To appear in Blackburn & de Rijke (eds) Logic, Structure and Syntax. Kluwer, Dordrecht.

[Moortgat 91] M. Moortgat (1991), Generalized quantifiers and discontinuous type constructors. Report, OTS, Utrecht University

[Moortgat 88] M. Moortgat (1988), Categorial Investigations. Logical and Linguistic Aspects of the Lambek Calculus. Foris, Dordrecht.

[Moortgat 95] M. Moortgat (1995), “Multimodal linguistic inference”, IGPL Bulletin, Vol 3 (2,3), p 371–421. Special issue Deduction and Language (guest editor: Ruth Kempson). (Revised version to appear in JoLLI).

[Moort. & Morrill 91] M. Moortgat and G. Morill (1991), “Heads and phrases. Type calculus for dependency and constituent structure” . Manuscript, OTS Utrecht.

[Moort. & Oehrle 93] M. Moortgat and R.T. Oehrle (1993) Logical Parameters and Linguistic Variations. Lecture Notes on Categorial Grammar. 5th European Summer School in Logic, Language and Information, Lisbon.

[Moort. & Oehrle 94] M. Moortgat and R.T. Oehrle (1994), “Adjacency, dependency and order’. Proceedings 9th Amsterdam Colloquium, pp 447-466.

[Morrill 94] G. Morrill (1994), Type Logical Grammar. Categorial Logic of Signs. Kluwer Academic Publishers

[Morrill 95] G. Morrill (1995), ‘Higher-order Linear Logic Programming of Categorial Deduction’. Proceedings EACL95, Dublin.

[Oehrle 94] R. T. Oehrle (1995), “Term-labeled categorial type systems”, Linguistics and Philosophy, 17.633–678.

[Sanchez 89] V. Sanchez (1989), Natural Logic, Generalized Quantifiers and Categorial Grammar. PhD Dissertation, ILLC, University of Amsterdam

[Venema 94] Y. Venema, (1994) Tree Models and labelled Categorial Grammar. Report, OTS, University of Utrecht. To appear in JoLLI.