Controlling resource management

Natasha Kurtonina and Michael Moortgat Research Institute for Language and Speech (OTS) Trans 10, 3512 JK Utrecht {kurtonina,moortgat}@let.ruu.nl

Abstract The structural parameters of precedence, dominance and dependency generate a cube of resource-sensitive type inference systems. From the pure logic of residuation NL, one obtains L, NLP and LP in terms of Associativity, Commutativity, and their combination. Each of these systems has a dependency variant, where the product is split up into a left-headed and a right-headed version. For all the logics in this family, completeness holds with respect to an interpretation in the power set algebra of ternary relational frame structures, suitably constrained with respect to the relevant structural parameter. In this paper we study the extension of these systems with unary residuated operators ◇, □^{↓}, interpreted with respect to binary relational structures. The completeness results carry over to the situation of mixed (2,3) frames. In the extended systems we can present embeddings in terms of ◇, □^{↓} that fully recover control over resource management in the dimensions of linear order, dominance and dependency in logics where such control is lacking at the level of the product/implication fragments.

1 Logics of structured resources

This paper is concerned with the issue of communication between categorial type logics of the Lambek family. Lambek calculi occupy a lively corner in the broader landscape of resource-sensitive systems of inference. In the application envisaged here, the resources we are talking about are linguistic expressions — signs. These resources are structured in dimensions of linear order, hierarchical grouping (constituency) and dependency. The structure of the resources determines well-formedness — the key concept in grammatical analysis, which we present here in logical terms, i.e. in terms of derivability.

Fig 1 charts the eight logics that result from the interplay of the structural parameters of precedence, dominance and dependency. The systems lower in the cube exhibit a more fine-grained sense of structure-sensitivity; their neighbours higher up loose discrimination for one of the structural parameters we distinguish here. In presenting the grammar for a language, we will in general not be in a position to restrict ourselves to one particular type logic — we want to have access to the combined inferential capacities of the different logics. For this to be possible we need a theory of systematic communication between type systems.

Following the logical tradition, the issue of communication has already been addressed in the categorial literature in terms of embeddings of stronger (less discriminating) logics within weaker ones. Embedding theorems of this type show that it is possible to gain full access to the flexibility of a logic with a more liberal resource management regime from within a system with a more constrained form of resource management. Systematic treatment of embeddings in this direction can be found in [13] and [5].

Here we are interested in the complementary question, which is at least as relevant from the linguistic point of view: can one systematically recover full control over structural discrimination (with respect to the parameters of order, dominance, dependency) from within a coarser logic where such discrimination is lacking? A positive answer to this question would entail we have a general logic of constraints in the dimensions of order, dominance and dependency. A conjecture for one particular embedding ([12]) was proved to be correct in [5]. We exploit the proof strategy here to obtain embeddings for the full landscape.

Before embarking on this enterprise, we present the bare essentials (syntactically and semantically) of the framework we are assuming. For a fuller treatment, see [8, 11, 9, 10].

[figure: NLP; LP; L; NL; DNLP; DLP; DL; DNL]

Figure 1: Resource-sensitive logics: precedence, dominance, dependency

Consider first the standard language of categorial type formulae F freely generated from a set of atomic formulae A: F ::= A | F/F | F • F | F\F. The most general interpretation for such a language can be given in terms of Kripke style relational structures — ternary relational structures ⟨W, R^{3}⟩ in the case of the binary connectives ([1]), with W to be understood as the set of linguistic resources (signs) and the accessibility relation R as representing linguistic composition. From a ternary frame we obtain a model by adding a valuation V sending prime formulae to subsets of W and satisfying the clauses below for compound formulae.

\begin{aligned}V (A • B) & = & \{z |∃x∃y[Rzxy & x ∈ V (A) & y ∈ V (B)]\} \\ V (C/B) & = & \{x |∀y∀z[(Rzxy & y ∈ V (B)) ⇒ z ∈ V (C)]\} \\ V (A\C) & = & \{y |∀x∀z[(Rzxy & x ∈ V (A)) ⇒ z ∈ V (C)]\} \end{aligned}

With no restrictions on R, we obtain the pure logic of residuation known as NL.

residuation A → C/B ⟺ A • B → C ⟺ B → A\C

And with restrictions on the interpretation of R, and corresponding structural postulates, we obtain the systems NLP, L and LP. Notice that the structural discrimination gets coarser as we impose more constraints on the interpretation of R.

structural postulate  frame condition
ass  A • (B • C) ⟷ (A • B) • C ∃t.Rxyt & Rtzu ⟺ ∃v.Rvyz & Rxvu
comm  A • B → B • A  Rzxy ⟺ Rzyx

What we have said so far concerns the upper face of the cube of Fig 1. To obtain the systems at the lower face, we split the connective • in left-headed •_{l} and rightheaded •_{r}, taking into account the asymmetry between heads and dependents. See [9]. Semantically, the lower plane of logics is obtained by moving from unimodal to multimodal (in this case: bimodal) frames ⟨W, R_{l}^{3}, R_{r}^{3}⟩, with a distinct accessibility relation for each product. Again, we have the pure (bimodal) logic of residuation DNL, with arbitrary interpretation for R_{l}^{3}, R_{r}^{3}, and its relatives DNLP, DL, DLP, obtained by imposing associativity or (head-preserving!) commutativity constraints on the interpretation of R_{l}^{3}, R_{r}^{3}.

In Moortgat [8], we propose an enrichment of the type language of these systems with unary residuated operators, interpreted in terms of a binary relation of accessibility. These operators will be the key devices in our strategy for recovering control over resource management.

◇A → B ⟺ A → □^{↓}B
V (◇A) = {x | ∃y(R^{2}xy ∧ y ∈ V (A)}
V (□^{↓}A) = {x | ∀y(R^{2}yx ⇒ y ∈ V (A)}

Completeness

An essential building-block of the embedding theorems to be presented in the following sections is the completeness of the logics compared. For ternary frame semantics for the F(/, •, \) fragment, Došen [1] obtains completeness on the basis of a canonical model construction: ⊢ A → B iff for all frames (or: for all ass, comm, ass+comm frames) V (A) ⊆ V (B). The canonical model construction directly accomodates the bimodal systems with F(/_{i}, •_{i}, \_{i}) (i ∈ {l, r}). And it is shown in Moortgat [8] that the construction also extends unproblematically to the ◇, □^{↓} extended language. We now consider mixed frames ⟨W, R^{2}, R_{i}^{3}⟩ with W the set of linguistic resources as before, R^{2} an arbitrary binary and relation on W, and the R_{i}^{3} ternary relations (arbitrary, associative, commutative, associative plus commutative, as the case may be). The canonical model construction is extended to the mixed (2,3) frames as follows. For the canonical frame, let W be the formulae of F(/_{i}, •_{i}, \_{i}, ◇, □^{↓}). In the canonical frame, we define the accessibility relations R^{2} and R_{i}^{3} as follows:

R_{i}^{3}(A, B, C) ⟺ ⊢ A → B •_{i} C R^{2}(A, B) ⟺ ⊢ A → ◇B

Define the canonical valuation as V (A) = {B | ⊢ B → A}. Now suppose V (A) ⊆ V (B) but ⊬ A → B. If ⊬ A → B with the canonical valuation on the canonical frame, A ∈ V (A) but A ∉ V (B) so V (A) ⊈ V (B). Contradiction.

We close this introductory section with a Gentzen presentation of the logics under discussion. For our illustrations later on we use Gentzen style derivations.

Definition 1.1 Gentzen presentation. Sequents Γ ⇒ A with Γ a structured database of linguistic resources, A a formula. Structured databases are inductively defined as terms T ::= F | (T , T )^{i} | (T )^{⋄}, with binary (·, ·)^{i} or unary (·)^{⋄} structural connectives corresponding to the (binary, unary) logical connectives.

[Ax] \overline{A ⇒ A}  \frac{Γ ⇒ A Δ[A] ⇒ C}{Δ[Γ] ⇒ C} [Cut]

[R◇] \frac{Γ ⇒ A}{(Γ)^{⋄} ⇒ ◇A}  \frac{Γ[(A)^{⋄}] ⇒ B}{Γ[◇A] ⇒ B} [L◇]

[R□^{↓}] \frac{(Γ)^{⋄} ⇒ A}{Γ ⇒ □^{↓}A}  \frac{Γ[A] ⇒ B}{Γ[(□^{↓}A)^{⋄}] ⇒ B} [L□^{↓}]

[R/_{i}] \frac{(Γ, B)^{i} ⇒ A}{Γ ⇒ A/_{i}B}  \frac{Γ ⇒ B  Δ[A] ⇒ C}{Δ[(A/_{i}B, Γ)^{i}] ⇒ C} [L/_{i}]

[R\_{i}] \frac{(B, Γ)^{i} ⇒ A}{Γ ⇒ B\_{i}A}  \frac{Γ ⇒ B  Δ[A] ⇒ C}{Δ[(Γ, B\_{i}A)^{i}] ⇒ C} [L\_{i}]

[L•_{i}] \frac{Γ[(A, B)^{i}] ⇒ C}{Γ[A •_{i} B] ⇒ C}  \frac{Γ ⇒ A  Δ ⇒ B}{(Γ, Δ)^{i} ⇒ A •_{i} B} [R•_{i}]

Structural rules (relativized to the appropriate resource management modes):

\frac{Γ[(Δ_{2}, Δ_{1})^{k}] ⇒ A}{Γ[(Δ_{1}, Δ_{2})^{k}] ⇒ A} [P]  Γ[((Δ_{1}, Δ_{2})^{m}, Δ_{3})^{m}] ⇒ A Γ[(Δ_{1}, (Δ_{2}, Δ_{3})^{m})^{m}] ⇒ A [A]

2 Recovering control

In the sections that follow, we consider pairs of logics L, L′ where L is a ‘southern’ neighbour of L′. For the 12 edges of the cube of Fig 1, we define embedding translations (·)^{♯} : F(L) ↦ F(L′◇) which fully recover the structural discrimination of L in L′ with its more liberal resource management. The embedding theorems have the format

L ⊢ A → B iff L′◇ ⊢ A^{♯} → B^{♯}

One can prove the (⇒) part by an easy induction on the length of derivations in L which we’ll leave to the reader. For the proofs of the (⇐) part, we rely on the completeness of the logics compared. We present the proof recipe here in general terms, and supply the particular ingredients in the following sections.

To show that ⊢ A^{♯} → B^{♯} in L′◇ implies ⊢ A → B in L we proceed by contraposition. Suppose L ⊬ A → B. By completeness, there is an L model M = ⟨F, V ⟩ falsifying A → B, i.e. there is a point a such that M, a ⊧ A but M, a |̸= B. From M, we construct an L′ model M′ = ⟨F′, V′⟩: for the construction of F′, we put a in the domain of F′ and we take into account the difference in structure between F and F′; for the valuation, we set V′(p) = V (p). We prove that the construction of M′ is truth preserving, i.e. that for any a ∈ W ∩ W′, M, a ⊧ A iff M′, a ⊧ A^{♯}. Then, if M is a countermodel for A → B, so is M′ for A^{♯} → B^{♯}. By completeness again, we may conclude that L′◇ ⊬ A^{♯} → B^{♯}.

The paper is organised as follows. In §3, we discuss a representative case for each of the structural dimensions of precedence, dominance and dependency. This covers the edges connected to the pure logic of residuation, NL. In §4, we show how with minor adaptions the embedding translations of §3 can be extended to the remaining edges, with the exception of the four associative logics at the right back face of the cube. These are treated in §5. Our strategy here is to use the composition of simple embedding translations plus modal associativity postulates.

3 Simple embeddings

Prop 3.4: Commutativity NLP

L

[figure] [figure]

Prop 3.6: Associativity

NL

Prop 3.2: Dependency

DNL

Figure 2: Simple embeddings: precedence, dominance, dependency

3.1 Dependency

For the most straightforward application of the method, we consider the dependecy calculus DNL of [9] and show how it can be emdedded in NL. Recall that DNL is the pure logic of residuation for a bimodal system with asymmetric products •_{l}, •_{r} for left-headed and right-headed composition respectively. The distinction between left- and right-headed products is expressible within NL◇, where we have the unary residuated pair ◇, □^{↓} next to a symmetric product • and its implications.

Definition 3.1 The embedding translation ·^{♯} : F(DNL) ↦ F(NL◇) is defined as follows.

p^{♯} = p
(A •_{l} B)^{♯} = ◇A^{♯} • B^{♯} (A •_{r} B)^{♯} = A^{♯} • ◇B^{♯}
(A/_{l}B)^{♯} = □^{↓}(A^{♯}/B^{♯}) (A/_{r}B)^{♯} = A^{♯}/◇B^{♯}
(B\_{l}A)^{♯} = ◇B^{♯}\A^{♯}  (B\_{r}A)^{♯} = □^{↓}(B^{♯}\A^{♯})

We now have the following proposition.

Proposition 3.2

DNL ⊢ A → B iff NL◇ ⊢ A^{♯} → B^{♯}

The (⇒) half is easily proved by induction on the length of the derivation of A → B in DNL and we will in general not bother to go through the induction. Below one of the residuation inferences as an illustration.

\begin{matrix}A •_{l} B → C \\ A → C/_{l}B \end{matrix}  \begin{matrix}(A •_{l} B)^{♯} → C^{♯} \\ A^{♯} → (C/_{l}B)^{♯} \end{matrix}  \begin{matrix}◇A^{♯} • B^{♯} → C^{♯} \\ ◇A^{♯} → C^{♯}/B^{♯} \\ A^{♯} → □^{↓}(C^{♯}/B^{♯}) \end{matrix}

For the (⇐) direction, let us apply the general method outlined above. Suppose DNL ⊬ A → B. By completeness, there is a model M = ⟨W, R_{l}^{3}, R_{r}^{3}, V ⟩ falsifying A → B. From M, we want to construct a model M′ = ⟨W′, R_{•}^{3}, R_{⋄}^{2}, V′⟩ which falsifies A^{♯} → B^{♯}. Then, by completeness again, we will be able to conclude NL◇ ⊬ A^{♯} → B^{♯}.

Consider the frames. For every triple (abc) ∈ R_{l}^{3}, we introduce a fresh b′ and put the worlds a, b, b′, c ∈ W′, (b′b) ∈ R_{⋄}^{2} and (ab′c) ∈ R_{•}^{3}. Similarly, for every triple (abc) ∈ R_{r}^{3}, we introduce a fresh c′ and put the worlds a, b, c, c′ ∈ W′, (c′c) ∈ R_{⋄}^{2} and (abc′) ∈ R_{•}^{3}. For the valuation, we set V′(p) = V (p). In a picture (with dotted lines for the dependent daughter for R_{l}, R_{r}):

\begin{matrix}M  [figure: a; b; c] & ⇝ & [figure: a; b′ b; c]  M′ \\ M  [figure: a; b; c] & ⇝ & [figure: a; b; c′ c]  M′ \end{matrix}

We have to prove that the construction of M′ is truth preserving. By induction on the complexity of A, we can show that for any a ∈ W ∩ W′, M, a ⊧ A iff M′, a ⊧ A^{♯}. We prove the biconditional for the left-headed product. The other connectives are handled in a similar way.

(⇒). Suppose M, a ⊧ A•_{l}B. By the truth conditions for •_{l}, there exist b, c such that (i) R_{l}abc and (ii) M, b ⊧ A, (iii) M, c ⊧ B. By the construction of M′, we conclude from (i) that there is a fresh b′ ∈ W′ such that (iv) R_{⋄}^{2}b′b and (v) R_{•}^{3}ab′c. By inductive hypothesis, from (ii) and (iii) we have M′, b ⊧ A^{♯} and M′, c ⊧ B^{♯}. Then, from (iv) we have M′, b′ ⊧_{⋄} A^{♯} and from (v), M′, a ⊧ ◇A^{♯} • B^{♯}.

(⇐). Suppose M′, a ⊧ ◇A^{♯} • B^{♯}. From the truth conditions for •, ◇, we know there are d′, d, e ∈ W′ such that (i) R_{⋄}^{2}d′d, (ii) R_{•}^{3}ad′e and (iii) M′, d ⊧ A^{♯} and M′, e ⊧ B^{♯}. From the construction of M′, we may conclude that d′ = b′, d = b, e = c, since every triple (abc) ∈ R_{l}^{3} is keyed to a fresh world b′ ∈ W′. So we actually have (i’) R_{⋄}^{2}b′b, (ii’) R_{•}^{3}ab′c and (iii’) M′, b ⊧ A^{♯} and M′, c ⊧ B^{♯}. (i’) and (ii’) imply R_{l}^{3}abc. By inductive hypothesis, we have from (iii’) M, b ⊧ A, and M, c ⊧ B. But then M, a ⊧ A •_{l} B.

Illustration

Below two instances of lifting in DNL. The left one is derivable, the right one is not.

\begin{matrix}\begin{matrix}\begin{matrix}A^{♯} ⇒ A^{♯} \\ (A^{♯})^{⋄} ⇒ ◇A^{♯} \end{matrix} ◇R & B^{♯} ⇒ B^{♯} \\ ((A^{♯})^{⋄}, ◇A^{♯}\B^{♯})^{•} ⇒ B^{♯} \end{matrix} & \L \\ (A^{♯})^{⋄} ⇒ B^{♯}/(◇A^{♯}\B^{♯}) \end{matrix} ; /R ; A^{♯} ⇒ □^{↓}(B^{♯}/(◇A^{♯}\B^{♯})) ; □^{↓}R ; A ⇒ B/_{l}(A\_{l}B) ; ·^{♯}  \begin{matrix}\begin{matrix}? \\ ((A^{♯})^{⋄}, □^{↓}(A^{♯}\B^{♯}))^{•} ⇒ B^{♯} \end{matrix} ; (A^{♯})^{⋄} ⇒ B^{♯}/□^{↓}(A^{♯}\B^{♯}) & /R \\ A^{♯} ⇒ □^{↓}(B^{♯}/□^{↓}(A^{♯}\B^{♯})) \end{matrix} ; □^{↓}R ; A ⇒ B/_{l}(A\_{r}B) ; ·^{♯}

3.2 Commutativity

We can exploit the modal embedding of the dependency calculus to recover control over Permutation. Here we look at the embedding of NL into NLP◇. In §4 we generalize the result. For the embedding, choose one of the (asymmetric) dependency product translations for • in NL. Permutation in NLP spoils the asymmetry of the product.

Definition 3.3 The embedding translation ·^{♯} : F(NL) ↦ F(NLP◇) is defined as follows.

p^{♯} = p
(A • B)^{♯} = ◇A^{♯} ⊗ B^{♯}
(A/B)^{♯} = □^{↓}(A^{♯}∘−B^{♯})
(B\A)^{♯} = ◇B^{♯}−∘A^{♯}

Proposition 3.4

NL ⊢ A → B iff NLP◇ ⊢ A^{♯} → B^{♯}

The (⇒) part again is proved straightforwardly by induction on the length of the derivation of A → B in NL. For the (⇐) direction, suppose NL ⊬ A → B. By completeness, there is a model M = ⟨W, R_{•}^{3}, V ⟩ falsifying A → B. From M, we now have to construct a commutative model M′ = ⟨W′, R_{⊗}^{3}, R_{⋄}^{2}, V′⟩ which falsifies A^{♯} → B^{♯}. Then, by completeness again, we will conclude that NLP◇ ⊬ A^{♯} → B^{♯}.

The construction of the frame for M′ in this case proceeds as follows. For every triple (abc) ∈ R_{•}^{3}, we introduce a fresh b′ and put the worlds a, b, b′, c ∈ W′, (b′b) ∈ R_{⋄}^{2} and both (ab′c), (acb′) ∈ R_{⊗}^{3}. The construction makes the frame for M′ commutative. But because every commutative triple (ab′c) depends on a fresh b′ ∈ W′ − W, the commutativity of M′ has no influence on M. For the valuation, we set V′(p) = V (p).

Now for any a ∈ W ∩W′, we can show by induction on the complexity of A that M, a ⊧ A iff M′, a ⊧ A^{♯}.

Illustration

Below first a theorem of NL, followed by a non-theorem. We compare their image under ·^{♯} in NLP◇. And we notice that the second example is derivable in NLP.

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}B^{♯} ⇒ B^{♯} & A^{♯} ⇒ A^{♯} \\ (A^{♯}∘−B^{♯}, B^{♯})^{⊗} ⇒ A^{♯} \end{matrix} & ∘−L \\ ((□^{↓}(A^{♯}∘−B^{♯}))^{⋄}, B^{♯})^{⊗} ⇒ A^{♯} \end{matrix} ; □^{↓}L ; (□^{↓}(A^{♯}∘−B^{♯}))^{⋄} ⇒ A^{♯}∘−B^{♯} ; ∘−R ; □^{↓}(A^{♯}∘−B^{♯}) ⇒ □^{↓}(A^{♯}∘−B^{♯}) ; □^{↓}R ; (□^{↓}(A^{♯}∘−B^{♯}))^{⋄} ⇒ ◇□^{↓}(A^{♯}∘−B^{♯}) ; ◇R & A^{♯} ⇒ A^{♯} \\ ((□^{↓}(A^{♯}∘−B^{♯}))^{⋄}, ◇□^{↓}(A^{♯}∘−B^{♯})−∘A^{♯})^{⊗} ⇒ A^{♯} \end{matrix} & −∘L \\ (□^{↓}(A^{♯}∘−B^{♯}))^{⋄} ⇒ A^{♯}∘−(◇□^{↓}(A^{♯}∘−B^{♯})−∘A^{♯}) \end{matrix} ; ∘−R ; □^{↓}(A^{♯}∘−B^{♯}) ⇒ □^{↓}(A^{♯}∘−(◇□^{↓}(A^{♯}∘−B^{♯})−∘A^{♯})) ; □^{↓}R ; NL ⊢ A/B ⇒ A/((A/B)\A) ; ·^{♯}

\begin{matrix}\begin{matrix}? \\ ((□^{↓}(A^{♯}∘−B^{♯}))^{⋄}, □^{↓}(A^{♯}∘−(◇B^{♯}−∘A^{♯})))^{⊗} ⇒ A^{♯} \end{matrix} ; (□^{↓}(A^{♯}∘−B^{♯}))^{⋄} ⇒ A^{♯}∘−(□^{↓}(A^{♯}∘−(◇B^{♯}−∘A^{♯})) & ∘−R \\ □^{↓}(A^{♯}∘−B^{♯}) ⇒ □^{↓}(A^{♯}∘−(□^{↓}(A^{♯}∘−(◇B^{♯}−∘A^{♯}))) \end{matrix} ; □^{↓}R ; NL ⊬ A/B ⇒ A/(A/(B\A)) ; ·^{♯}

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}B ⇒ B & A ⇒ A \\ (A∘−B, B)^{⊗} ⇒ A \end{matrix} & ∘−L \\ (B, A∘−B)^{⊗} ⇒ A \end{matrix} ; P ; A∘−B ⇒ B−∘A ; −∘R & A ⇒ A \\ (A∘−(B−∘A), A∘−B)^{⊗} ⇒ A \end{matrix} & ∘−L \\ (A∘−B, A∘−(B−∘A))^{⊗} ⇒ A \end{matrix} ; P ; NLP ⊢ A∘−B ⇒ A∘−(A∘−(B−∘A)) ; ∘−R

3.3 Associativity

For the pair NL versus L◇, Morrill ([12]) conjectures an embedding based on the following translation. (We use the same symbols for the connectives in NL and L: note carefully that in the latter /, •, \ have an associative interpretation.)

Definition 3.5 Translation ·^{♯} : F(NL) ↦ F(L◇) as below.

p^{♯} = p
(A • B)^{♯} = ◇(A^{♯} • B^{♯})
(A/B)^{♯} = □^{↓}A^{♯}/B^{♯}
(B\A)^{♯} = B^{♯}\□^{↓}A^{♯}

Proposition 3.6

NL ⊢ A → B iff L◇ ⊢ A^{♯} → B^{♯}

Consider again falsifying models M = ⟨W, R_{•}^{3}, V ⟩ and M′ = ⟨W′, R_{a}^{3}, R_{⋄}^{2}, V′⟩ for A → B in NL and A^{♯} → B^{♯} in L◇, respectively. The construction of the frame for M′ proceeds as follows. For every triple (abc) ∈ R_{•}^{3}, we introduce a fresh a′ and put the worlds a, a′, b, c ∈ W′, (aa′) ∈ R_{⋄}^{2} and (a′bc) ∈ R_{a}^{3}.

M [figure: a; b; c] ⇝ a [figure: a′; b; c] M′

The frame for M′ has to satisfy the frame condition for associativity:

(⋆) ∀xyzw ∈ W′(∃t(R_{a}wxt ∧ R_{a}tyz) ⟺ ∃t′(R_{a}wt′z ∧ R_{a}t′xy))

(⋆) is satisfied automatically because, by the construction of M′, there are no x, y, z, w ∈ W′ that fulfill the requirements: for every triple (xyz) ∈ R_{a}^{3}, the point x is chosen fresh, which implies that no point of W′ can be both the root of one triangle and a leaf in another one. Now, M, a ⊧ A iff M′, a ⊧ A^{♯} is shown as before.

4 Generalisations

The results of the previous section can be extended with minor modifications to the five edges that remain when we keep the Associativity face for §5.

What we have done in Prop 3.2 for the pair DNL versus NL◇ can be adapted straightforwardly to the commutative pair DNLP versus NLP◇. Recall that in DNLP, the dependency products satisfy head-preserving commutativity (DP), whereas in NLP we have simple commutativity (P).

\begin{matrix}DP : A ⊗_{l} B ⟷ B ⊗_{r} A \\ P : A ⊗ B → B ⊗ A \end{matrix}

Accomodating the commutative products, the embedding translation is that of Prop 3.2: ◇ marks the head subtype.

Definition 4.1 Translation ·^{♯} : F(DNLP) ↦ F(NLP◇):

p^{♯} = p
(A ⊗_{l} B)^{♯} = ◇A^{♯} ⊗ B^{♯}  (A ⊗_{r} B)^{♯} = A^{♯} ⊗ ◇B^{♯}
(A∘−_{l}B)^{♯} = □^{↓}(A^{♯}∘−B^{♯}) (A∘−_{r}B)^{♯} = A^{♯}∘−◇B^{♯}
(B−∘_{l}A)^{♯} = ◇B^{♯}−∘A^{♯}  (B−∘_{r}A)^{♯} = □^{↓}(B^{♯}−∘A^{♯})

Proposition 4.2

DNLP ⊢ A → B iff NLP◇ ⊢ A^{♯} → B^{♯}

For the proof of the (⇐) direction, we combine the method of construction of Prop 3.2 with that of Prop 3.4. For a configuration R_{l}^{⊗}abc in M, we take fresh b′ and put the configurations R_{⋄}b′b, R_{⊗}ab′c, R_{⊗}acb′ in M′. Similarly, for a configuration R_{r}^{⊗}abc in M, we take fresh c′ and put the configurations R_{⋄}c′c, R_{⊗}abc′, R_{⊗}ac′b in M′. The commutativity property of ⊗ is thus realized by the construction.

\begin{matrix}M [figure: a; b; c] ⇝ [figure: a; b′ b; c] + [figure: a; c; b′ b] M′ \\ M [figure: a; b; c] ⇝ [figure: a; b; c′ c] + [figure: a; c′ c; b] M′ \end{matrix}

Let us check the truth preservation lemma. This time a configuration (⋆) in M′ does not have a unique pre-image: it can come from R_{l}^{⊗}xyz or R_{r}^{⊗}xzy. But because of head-preserving commutativity (DP), these are both in M.

(⋆) [figure: x; z; y′ y]

Similarly, the embedding construction presented in Prop 3.4 for the pair NL versus NLP◇ can be generalized directly to the related pair DNL versus DNLP◇. This time, we want the embedding translation to block the structural postulate of head-preserving commutativity in DNLP. The translation below invalidates the postulate by uniformly decorating with ◇, say, the left subtype of a product.

Definition 4.3 Define ·^{♯} : F(DNL) ↦ F(DNLP◇) as follows.

p^{♯} = p

(A •_{l} B)^{♯} = ◇A^{♯} ⊗_{l} B^{♯} (A •_{r} B)^{♯} = ◇A^{♯} ⊗_{r} B^{♯}
(A/_{l}B)^{♯} = □^{↓}(A^{♯}∘−_{l}B^{♯}) (A/_{r}B)^{♯} = □^{↓}(A^{♯}∘−_{r}B^{♯})
(B\_{l}A)^{♯} = ◇B^{♯}−∘_{l}A^{♯} (B\_{r}A)^{♯} = ◇B^{♯}−∘_{r}A^{♯}

We then have the following proposition. The proof is entirely parallel to that of Prop 3.4 before.

Proposition 4.4

DNL ⊢ A → B iff DNLP◇ ⊢ A^{♯} → B^{♯}

The method of Prop 3.6 generalizes to the following cases with some simple changes.

Definition 4.5 Translation ·^{♯} : F(NLP) ↦ F(LP◇) as below.

p^{♯} = p
(A ⊗ B)^{♯} = ◇(A^{♯} ⊗ B^{♯})
(A∘−B)^{♯} = □^{↓}A^{♯}∘−B^{♯}
(B−∘A)^{♯} = B^{♯}−∘□^{↓}A^{♯}

Proposition 4.6

NLP ⊢ A → B iff LP◇ ⊢ A^{♯} → B^{♯}

The only difference with Prop 3.6 is that the product in input and target logic are commutative. Commutativity is realized automatically by the construction of M′.

Proposition 4.7

DNL ⊢ A → B iff DL◇ ⊢ A^{♯} → B^{♯}

Proposition 4.8

DNLP ⊢ A → B iff DLP◇ ⊢ A^{♯} → B^{♯}

5 Composed translations

The remaining cases concern the right back face of the cube, where we find the associative systems DL, L, LP, DLP. For the embeddings we use compositions of translations defined individually before. Our strategy is to neutralize direct appeal to the Associativity of the target logic, installing modal versions of the Associativity postulates instead.

5.1 Associative dependency calculus

Consider first the pair DL versus L. In DNL we have no restrictions on the interpretation of •_{l}, •_{r}. In DL we assume •_{l}, •_{r} are interpreted on (bimodal) associative frames, and we have structural associativity postulates A(l), A(r) on top of the pure logic of residuation for •_{l}, •_{r}.

\begin{matrix}A(l) : (A •_{l} B) •_{l} C ⟷ A •_{l} (B •_{l} C) \\ A(r) : A •_{r} (B •_{r} C) ⟷ (A •_{r} B) •_{r} C \end{matrix}

[figure: LP; L; DLP; DL]

Figure 3: Embedding translations: the Associative face

Our general proof method for the embedding does not work if we add a straightforward modal translation of A(l, r) such as given below: the associativity for • in the target logic L would spoil the truth preservation lemma.

\begin{matrix}◇A • (◇B • C) ⟷ ◇(◇A • B) • C (cf.A(l)) \\ (A • ◇B) • ◇C ⟷ A • ◇(B • ◇C) (cf.A(r)) \end{matrix}

To avoid this problem, we develop a slightly more involved construction. For the embedding translation, we compose the mappings DNL-NL and NL-L.

Definition 5.1

p^{♯} = p
(A •_{l} B)^{♯} = ◇(◇A^{♯} • B^{♯}) (A •_{r} B)^{♯} = ◇(A^{♯} • ◇B^{♯})
(A/_{l}B)^{♯} = □^{↓}(□^{↓}A^{♯}/B^{♯}) (A/_{r}B)^{♯} = □^{↓}A^{♯}/◇B^{♯}
(B\_{l}A)^{♯} = ◇B^{♯}\□^{↓}A^{♯} (B\_{r}A)^{♯} = □^{↓}(B^{♯}\□^{↓}A^{♯})

From the proof of the embedding NL-L we know that ◇ neutralizes the influence of the associativity of • in the target logic L. We reinstall modal versions of the associativity postulates.

\begin{matrix}A(l)^{⋄} : ◇(◇◇(◇A • B) • C ⟷ ◇(◇A • ◇(◇B • C)) \\ A(r)^{⋄} : ◇(A • ◇◇(B • ◇C)) ⟷ ◇(◇(A • ◇B) • ◇C) \end{matrix}

Consider first the question of completeness with respect to the A(l)^{⋄}, A(r)^{⋄} structural postulates, cf Fig 5.1. We check completeness for A(l)^{⋄} — the situation for A(r)^{⋄} is entirely similar.

The models for L◇ are structures ⟨W, R_{⋄}^{2}, R_{•}^{3}, V ⟩. Now consider (⇒) in Figure 5.1 below. By the definition of R_{⋄}^{2}, R_{•}^{3} in the canonical model the following are derivable:

\begin{matrix}a → ◇b, & e → ◇f, \\ b → c • d, & f → g • h, \\ c → ◇e, & g → ◇i. \end{matrix}

From these we can conclude ⊢ a → ◇(◇◇(◇i • h) • d)), i.e. a ∈ V (◇(◇◇(◇i • h) • d))), given the definition of the canonical valuation (⋆). For (‡) we have to find b′, c′, d′, e′, f′ such that

\begin{matrix}a → ◇b′, & d′ → ◇e′, \\ b′ → c′ • d′, & e′ → f′ • d, \\ c′ → ◇i, & f′ → ◇h. \end{matrix}

Let us put

f′ = ◇h,
e′ = f′ • d = ◇h • d,
d′ = ◇e′ = ◇(◇h • d),
c′ = ◇i,
b′ = c′ • d′ = ◇i • ◇(◇h • d).

Together they imply ⊢ a → ◇(◇i • ◇(◇h • d)), i.e. a ∈ V (◇(◇i • ◇(◇h • d))) can be shown to follow from (⋆). Similarly for the other direction.

(†)  a [figure: b; c; e; f; gi; h; d] ⟺  a [figure: b′; c′i; d′; e′; f′ h; d]  (‡)

∃bcefg(R_{⋄}ab ∧ R_{•}bcd ∧ R_{⋄}ce ∧ R_{⋄}ef ∧ R_{•}fgh ∧ R_{⋄}gi) ⟺
∃b′c′d′e′f′(R_{⋄}ab′ ∧ R_{•}b′c′d′ ∧ R_{⋄}c′i ∧ R_{⋄}d′e′ ∧ R_{•}e′f′d ∧ R_{⋄}f′h)

Figure 4: A(l): modal version

Now for the embedding theorem.

Proposition 5.2

DL ⊢ A → B iff L◇ + A(l, r)^{⋄} ⊢ A^{♯} → B^{♯}

Suppose DL ⊬ A → B. Then there is a model M = ⟨W, R_{l}, R_{r}, V ⟩ where A → B fails. From M we construct M′ as follows. For every triple (abc) ∈ R_{l} we take fresh a′, b′ and put (aa′) ∈ R_{⋄}, (a′b′c) ∈ R_{•}, (b′b) ∈ R_{⋄}. Similarly, for every triple (abc) ∈ R_{r} we take fresh a′, c′ and put (aa′) ∈ R_{⋄}, (a′bc′) ∈ R_{•}, (c′c) ∈ R_{⋄}.

Now suppose (‡) holds, and let us check whether (†). Note that a configuration R_{⋄}ab′, R_{•}b′c′d′, R_{⋄}c′i can only hold if in M we had R_{l}aid′ (⋆). And a configuration R_{⋄}d′e′, R_{•}e′f′d, R_{⋄}f′h can be in M′ only if in M we had R_{l}d′hd (⋆⋆). The frame for M is associative. Therefore, from (⋆, ⋆⋆) we can conclude M also contains a configuration R_{l}aed, R_{l}eih for some e ∈ W. Applying the M′ construction to that configuration we obtain (†). Similarly for the other direction.

5.2 Generalisation

The method of composed translations can be generalized to the remaining edges. Below we give the relevant translations and embedding theorems. We give the essential ingredients for the construction of M′, leaving the elaboration as an exercise to the reader.

Definition 5.3 Embedding translation ·^{♯} : F(L) ↦ F(LP◇).

p^{♯} = p
(A • B)^{♯} = ◇(◇A^{♯} ⊗ B^{♯})
(A/B)^{♯} = □^{↓}(□^{↓}A^{♯}∘−B^{♯})
(B\A)^{♯} = ◇B^{♯}−∘□^{↓}A^{♯}

Proposition 5.4

L ⊢ A → B iff LP◇ + A(l, r)^{⋄} ⊢ A^{♯} → B^{♯}

We compose the translations of Def 4.5 and Def 3.3. We realize the commutativity of R_{⊗} via the construction of M′, as in the case of Prop 3.4:

M [figure: a; b; c] ⇝  a [figure: a′; b′ b; c] +  a [figure: a′; c; b′ b] M′

For the pair DL versus DLP, we compose the translations of Def ?? and Def 4.3.

Definition 5.5 Embedding translation ·^{♯} : F(DL) ↦ F(DLP◇).

p^{♯} = p
(A •_{l} B)^{♯} = ◇(◇A^{♯} ⊗_{l} B^{♯}) (A •_{r} B)^{♯} = ◇(◇A^{♯} ⊗_{r} B^{♯})
(A/_{l}B)^{♯} = □^{↓}(□^{↓}A^{♯}∘−_{l}B^{♯}) (A/_{r}B)^{♯} = □^{↓}(□^{↓}A^{♯}∘−_{r}B^{♯})
(B\_{l}A)^{♯} = ◇B^{♯}−∘_{l}□^{↓}A^{♯} (B\_{r}A)^{♯} = ◇B^{♯}−∘_{r}□^{↓}A^{♯}

Proposition 5.6

DL ⊢ A → B iff DLP◇ + A(l, r)^{⋄} ⊢ A^{♯} → B^{♯}

Finally, for the pair DLP versus LP, we compose the translations of Def 4.1 and Def 4.5.

Definition 5.7 Embedding translation ·^{♯} : F(DLP) ↦ F(LP◇).

p^{♯} = p
(A ⊗_{l} B)^{♯} = ◇(◇A^{♯} ⊗ B^{♯}) (A ⊗_{r} B)^{♯} = ◇(A^{♯} ⊗ ◇B^{♯})
(A∘−_{l}B)^{♯} = □^{↓}(□^{↓}A^{♯}∘−B^{♯}) (A∘−_{r}B)^{♯} = □^{↓}A^{♯}∘−◇B^{♯}
(B−∘_{l}A)^{♯} = ◇B^{♯}−∘□^{↓}A^{♯}  (B−∘_{r}A)^{♯} = □^{↓}(B^{♯}−∘□^{↓}A^{♯})

Proposition 5.8

DLP ⊢ A → B iff LP◇ + A(l, r)^{⋄} ⊢ A^{♯} → B^{♯}

6 Conclusion

We have completed the tour of the landscape. In Fig 5 we label the edges of the cube with the numbers of the embedding theorems. Some comments and directions for future research. First, notice that the embeddings of less discriminating logics into more discriminating ones as given in [5] use an S4 (KT 4) universal modality □. For the complementary direction of embedding discussed in this paper, we use a residuated pair of modalities ◇, □^{↓} with minimal resource management — the pure logic of residuation for R^{2}. Secondly, observe that the modal associativity postulates of §5 suggest a similar ‘minimal’ alternative to the S4 □ strategy for licensing relaxation of resource management.

[figure: 4.2; NLP; 4.6; LP; 5.4; L; 3.2; 3.6; 5.6; 3.4; 4.8; NL; 4.4; DNLP; 5.8; DLP; 5.2; 4.7; DL; DNL]

Figure 5: Embedding translations: recovering resource control

References

[1] Došen, K. (1992) ‘A brief survey of frames for the Lambek calculus’. Zeitschr. f. math. Logik und Grundlagen d. Mathematik 38, 179–187.

[2] Došen, K. (1988,1989) ‘Sequent systems and groupoid models’. Studia Logica 47, 353–385, 48, 41–65.

[3] Dunn, J.M. (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.

[4] Dunn, M. (1993) ‘Partial Gaggles Applied to Logics With Restricted Structural Rules’. In Došen and Schröder-Heister (eds) Substructural Logics. Oxford.

[5] Kurtonina, N. (1994) ‘On some modal extensions of the Lambek Calculus’. In [?].

[6] Lambek, J. (1958) ‘The Mathematics of Sentence Structure’, American Mathematical Monthly 65, 154–170.

[7] Lambek, J. (1988) ‘Categorial and categorical grammar’. In Oehrle, Bach and Wheeler (eds) Categorial Grammars and Natural Language Structures. Dordrecht.

[8] Moortgat, M. (1994) ‘Residuation in mixed Lambek systems’. This volume. (To appear in the IGPL Bulletin.)

[9] Moortgat, M. and G. Morrill (1991) ‘Heads and phrases. Type calculus for dependency and constituent structure’. Ms OTS Utrecht.

[10] Moortgat, M. and R. Oehrle (1993) Logical parameters and linguistic variation. Lecture notes on categorial grammar. 5th European Summer School in Logic, Language and Information. Lisbon.

[11] Moortgat, M. and R.T. Oehrle (1994) ‘Adjacency, dependency and order’. Proceedings 9th Amsterdam Colloquium, pp 447–466.

[12] Morrill, G. (1992) ‘Categorial formalisation of relativisation: pied-piping, islands and extraction sites’. Report LSI–92–23–R, Universitat Politècnica de Catalunya.

[13] Venema, Y. (1993) ‘Meeting strength in substructural logics’. UU Logic Preprint. To appear in Studia Logica.