Modal embeddings, residuation, and composition

Dick Oehrle Department of Linguistics, University of Arizona Tucson, AZ 85721, U.S.A.

May 19, 1998

Modal operators were introduced into categorial grammar by Morrill and his colleagues at Edinburgh. Inspired by the exponential operators of linear logic [9], they realized that modal operators could be exploited to gain increased forms of resourcesensitivity in the course of grammatical deduction. In particular, in just the same way as the exponential operators of linear logic can be used to license such resourcesensitive operations as contraction and weakening in an environment in which these operations are not generally valid, so can comparable operators be used to license other forms of structural sensitivity—such as permutation or associativity—in an environment in which such operations are not generally available. Because there are various forms of resource sensitivity, a number of different modals might be called for—one modality governing each structural property. An ambitious attack along these lines can be found in volume 5 of the Edinburgh Working Papers in Cognitive Science, entitled Studies in Categorial Grammar, edited by Morrill and Barry, and containing a number of path-breaking papers, explaining the many interesting linguistic applications of this line of research and setting forth a proof theory and a model theory relative to which the logical properties of the various systems could be explored.

This work prompted more probing questions. One question that arose involves the completeness of the envisioned modal extensions with respect to the intended semantics. Versmissen [10] showed that completeness does not always hold. Another question was prompted by the observation that modalities could be used both to allow certain behavior or to block certain behavior. For example, in Morrill’s paper [6], modal operators are used to indicate the possibility of extraction from a given domain. But they can just as well be used, as noted in lecture notes of mine [8] and independently, with much more thoroughness, by Morrill [7], to indicate the impossibility of extraction from a given domain.

The situation is reminiscent of attempts to control the applicability of transformational operations, as the question arose in Generative Grammar in the 1960’s. If one attempts to recast transformational grammar in the language of sequents, transformations take the form of structural rules. But many transformations were formulated in ways that did not allow them, on empirical grounds, to apply with complete generality. This led to the introduction of ‘rule features’ which could be associated with critical elements in such a way that a given transformation, ordinarily optional, might be required to apply or might be prevented from applying. In the terminology of Lakoff [3], such cases were ‘absolute positive exceptions’ and ‘absolute negative exceptions’. The analogy that is of interest here involves the fact that modalities and rule features both provide a mechanism for increasing control over inference. But there is this important difference: in the case of rule features, the control mechanism is an ad hoc device introduced from outside the system of categories; in the case of exponentials and modalities, the control system is integrated into the underlying logic. In fact, this difference is critical for the results that Kurtonina & Moortgat present, which depend fundamentally on the fact that □^{↓} is the residual of ◇.

1 Residuated modalities

Kurtonina & Moortgat express the fact that ◇ is residuated with residual □^{↓} in terms of the biconditional:

◇A → B ⇔ A → □^{↓}B

An alternative way of seeing this, following Blyth & Janowitz (see [1], [4]), is to note that ◇ and □^{↓} are both isotone and we have ◇ ∘ □^{↓} ≤ 1 ≤ □^{↓} ∘ ◇. Isotonicity here means that the following derived rules both hold:

\begin{matrix}A → B & A → B \\ \overline{◇A → ◇B} & \overline{□^{↓}A → □^{↓}B} \end{matrix}

The required compositions mean that we have:

◇□^{↓}A → A and A → □^{↓}◇A

These properties are immediate consequences of the sequent rules below:

[R◇] Γ → A ; \overline{(Γ)^{⋄} → ◇A}  Γ[(A)^{⋄}] → B ; \overline{Γ[◇A] → B} [L◇]

[R□^{↓}] (Γ)^{⋄} → A ; \overline{Γ → □^{↓}A}  Γ[A] → B ; \overline{Γ[(□^{↓}A)^{⋄}] → B} [L□^{↓}]

For example, we have

A → B ; \overline{(A)^{⋄} → ◇B} ; \overline{◇A → ◇B} and A → A ; \overline{(□^{↓}A)^{⋄} → A} ; \overline{◇□^{↓}A → A}

The importance of the fact that ◇ and □^{↓} form a residuated pair stems from a simple property: if f : A → B and g : B → C are residuated functions, with residuals f^{+} : B → A and g^{+} : C → B, respectively, then g ∘ f : A → C is a residuated function with residual (g ∘ f)^{+} = f^{+} ∘ g^{+}. (This is Theorem 2.8 of Blyth & Janowitz [1].) Since f, f^{+}, g, g^{+} are all isotone and the composition of any two isotone functions is again isotone, then the compositions g ∘ f and f^{+} ∘ g^{+} are isotone. Moreover, to see that the required inequalities hold, note:

\begin{matrix}g ∘ f ∘ f^{+} ∘ g^{+} ≤ g ∘ 1_{B} ∘ g^{+} = g ∘ g^{+} ≤ 1_{C} \\ 1_{A} ≤ f^{+} ∘ f = f^{+} ∘ 1_{B} ∘ f ≤ f^{+} ∘ g^{+} ∘ g ∘ f \end{matrix}

Given this result, we now turn to the question of what we can express using composition of residuated functions by adding ◇ and its residual □^{↓} to a logic based on a binary product.

2 Composition of residuated mappings

The simplest compositions of ◇ and • are the following:

(◇−) • −, − • (◇−), ◇(− • −)

Note that the first two are asymmetric and each is non-commutative. Moreover, it is obvious that the last gives us a product that we can easily distinguish from (− • −). Kurtonina & Moortgat exploit these properties in their embedding functions. Let us examine the compositions a little more closely.

For any type X, we write λ_{X} for the left translation function with action Y ↦ X • Y and ρ_{X} for the right translation function with action Y ↦ Y • X. The residual λ_{X}^{+} of λ_{X} is the function with action Z ↦ X\Z. And the residual ρ_{X}^{+} of ρ_{X} is the function with action Z ↦ Z/X.

Now, examine the compositions of left and right translations with ◇ below, paying attention to the fact that the residual (f ∘ g)^{+} of two residuated functions f and g is g^{+} ∘ f^{+} and to the very critical assumption that ◇^{+} = □^{↓}:

\begin{matrix}λ_{X} ∘ ◇ : & Y ↦ X • ◇Y \\ (λ_{X} ∘ ◇)^{+} = ◇+ ∘ λ_{X}^{+} : & Z ↦ □^{↓}(X\Z) \\ ρ_{X} ∘ ◇ : & Y ↦ ◇Y • X \\ (ρ_{X} ∘ ◇)^{+} = ◇^{+} ∘ ρ_{X}^{+} : & Z ↦ □^{↓}(Z/X) \\ ◇ ∘ λ_{X} : & Y ↦ ◇(X • Y) \\ (◇ ∘ λ_{X})^{+} = λ_{X}^{+} ∘ ◇+ : & Z ↦ X\□^{↓}Z \\ ◇ ∘ ρ_{X} : & Y ↦ ◇(Y • X) \\ (◇ ∘ ρ_{X})^{+} = ρ_{X}^{+} ∘ ◇+ : & Z ↦ □^{↓}Z/X \end{matrix}

These compositions give some insight into the embedding translations that Kurtonina & Moortgat propose. Because: first, any embedding translation must respect residuated functions and their associated residuals; and second, the left and right translations are determined by how the mapping acts on products.

Consider first the embedding translation ♯ : F(DNL) → F(NL◇) of Definition 3.1 of Kurtonina & Moortgat’s paper. DNL is a logic with two asymmetric structure-building operations and two corresponding product type-constructors •_{l} and •_{r}. Thus, we have the following residuated left- and right-translations in DNL:

\begin{matrix}λ_{X}•_{l} : & Y ↦ X •_{l} Y \\ ρ_{X}•_{l} : & Y ↦ Y •_{l} X \\ λ_{X}•_{r} : & Y ↦ X •_{r} Y \\ ρ_{X}•_{r} : & Y ↦ Y •_{r} X \end{matrix}

For atomic types p, we have p^{♯} = p: that is, ♯ restricted to the set of atomic types A is 1_{A}. Now, for the two products •_{l} and •_{r}, we have

(A •_{l} B)^{♯} = ◇A^{♯} • B^{♯} and (A •_{r} B)^{♯} = A^{♯} • ◇B^{♯}

These rules determine the other properties of ♯ completely. In particular, if we think of ♯ as acting on both objects and maps (as in category theory), the information about products above can be construed as a succinct statement of the following actions of ♯ on basic maps:

♯ : λ_{A}•_{l} ↦ λ_{◇A^{♯}}
♯ : ρ_{B}•_{l} ↦ ρ_{B^{♯}} ∘ ◇
♯ : λ_{A}•_{r} ↦ λ_{A^{♯}} ∘ ◇
♯ : ρ_{B}•_{r} ↦ ρ_{◇B^{♯}}

From these facts, and the fact that any embedding is a morphism of residuated mappings and their residuals, the action of ♯ on the residuals /_{l}, \_{l}, /_{r}, \_{r} is completely determined:

\begin{aligned}(A/_{l}B)^{♯} & = (ρ_{B}^{+} •_{l} (A))^{♯} \\ & = (ρ_{B}^{+}•_{l})^{♯}(A^{♯}) \\ & = ((ρ_{B}•_{l})^{♯})^{+}(A^{♯}) \\ & = (ρ_{B^{♯}} ∘ ◇)^{+}(A^{♯}) \\ & = (◇^{+} ∘ ρ_{B^{♯}}^{+})(A^{♯}) \\ & = □^{↓}(ρ_{B^{♯}}(A^{♯})) \\ & = □^{↓}(A^{♯}/B^{♯}) \end{aligned}  \begin{aligned}(B\_{l}A)^{♯} & = (λ_{B}^{+} •_{l} (A))^{♯} \\ & = (λ_{B}^{+}•_{l})^{♯}(A^{♯}) \\ & = ((λ_{B}•_{l})^{♯})^{+}(A^{♯}) \\ & = λ_{◇B^{♯}}^{+} (A^{♯}) \\ & = ◇B^{♯}\A^{♯} \end{aligned}

Symmetrically, we have:

\begin{matrix}(A •_{r} B)^{♯} = ((ρ_{B}•_{r}^{+})(A))^{♯} = A^{♯}/◇B^{♯} \\ (B\_{r}A)^{♯} = ((λ_{B}•_{r}^{+})(B))^{♯} = □^{↓}(B^{♯}\A^{♯}) \end{matrix}

The embedding transformation ♯ : F(NL) → F(NLP◇) of Definition 3.3 is determined in a similar way by the combination of the action 1_{A} on atomic types and the action ♯ : A • B ↦ ◇A^{♯} ⊗ B^{♯}. This forces the action of ♯ on the residuals / and \ in just the way Kurtonina & Moortgat observe.

In the case of the embedding transformation ♯ : F(NL) → F(L◇) of Definition 3.5, we have the information

(A • B)^{♯} = ◇(A^{♯} • B^{♯})

We interpret this as a way of stating the data:

\begin{matrix}♯ : λ_{A} ↦ ◇ ∘ λ_{A^{♯}} \\ ♯ : ρ_{B} ↦ ◇ ∘ ρ_{B^{♯}} \end{matrix}

Then, since (A/B) = ρ_{B}^{+}(A), its image under ♯ will be the application of the residual of ρ_{B}^{♯} to A^{♯}. Since (◇ ∘ ρ_{B^{♯}})^{+} = ρ_{B^{♯}}^{+} ∘ ◇^{+}, we have ♯ : A/B ↦ □^{↓}A^{♯}/B^{♯}, just as required.

The same reasoning applies to the composition of embeddings that Kurtonina & Moortgat use to extend their preliminary results to the full cube of logics they consider.

3 Embeddings and composite modes

In the previous section, we saw how the properties of embedding translations are determined by the action on atomic types—always taken to be 1_{A}—and by the action on product types. Since a product type •_{i} is simply an expression in the type language of the corresponding structure-building operation (−, −)^{i}, we can transfer our discussion directly to the level of structures. This provides an alternative approach to the study of embeddings which may perhaps be seen as a syntactic complement to the elegant semantic methods of Kurtonina & Moortgat, which depend on judicious access to completeness properties in two directions in a beautiful, symmetrical way.

Consider again the translation of Definition 3.1 which embeds F(DNL) into F(NL◇), in a way determined by the identity on atomic types and the rules:

(A •_{l} B) ↦^{♯} ◇A^{♯} • B^{♯} and (A •_{r} B) ↦^{♯} A^{♯} • ◇B^{♯}

Implicitly, this defines an embedding of both DNL and NL into NL◇, as diagrammed below with i the obvious insertion function mapping each (modal-free) NL-structure to itself (as an element of NL◇):

NL

↘^{i}

NL◇

↗^{♯}

DNL

This picture can be refined in the following way. We begin with the structure language of NL◇, which contains two structure-building operations: the binary (−, −) and the unary (−)^{⋄}. We define two new structure building operations^{⋄}(−, −) and (−, −)^{⋄} as the respective compositions:

((−)^{⋄}, −) and (−, (−)^{⋄})

We now consider the logic (call it NL+2) built up from the structural operations in the absence of structural rules. That is, starting with a set A of atomic types, we have formulas F, structures T , and sequents S according to the specifications:

F ::= A | F • F | F_{◇} • F | F •_{◇} F | [cases for _{◇} /,_{◇} \, /_{◇} , \_{◇} ]
T ::= F | (T , T ) | ^{⋄}(T , T ) | (T , T )^{⋄}
S ::= T → F

The postulates of NL+2 take the standard form and there are no structural rules (except for Cut, if we like).

Consider now the obvious embeddings determined by the correspondences between structures:

\begin{aligned}♮ : & NL → NL+2 \\ & (−, −) ↦ (−, −) \end{aligned}  \begin{aligned}♭ : & DNL → NL+2 \\ & (−, −)^{l} ↦^{⋄} (−, −) \\ & (−, −)^{r} ↦ (−, −)^{⋄} \end{aligned}

This yields the diagram:

NL

↘^{♮}

NL+2

↗^{♭}

DNL

We now unpack the composite structure-building operations by associating them with their definitions by the rule ♠ determined by the action (defined on (−, −)):

♠ : ^{⋄}(−, −) ↦ ((−)^{⋄}, −)
(−, −)^{⋄} ↦ (−, (−)^{⋄})
(−, −) ↦ (−, −)

This yields the embedding diagram:

NL

↘^{♮}

NL+2 →^{♠} NL◇

↗^{♭}

DNL

And, for the embedding translation ♯ of Definition 3.1, we have:

♯ = ♠ ∘ ♭

4 Conclusion

A by-product of the above discussion is the fundamental question: which structurebuilding operations can be defined as compositions of modalities with other operations. A case in point can be found in the contrasting interpretations of the commutative type-constructor ⊗ in Hepple’s interesting approach to hybrid categorial grammars [2] and the approach advocated by Moortgat and me in [4, 5].

Both viewpoints wish to have a symmetrical product, so that, writing A ⊗ B to represent the application of this product to types A and B, we have:

A ⊗ B ↔ B ⊗ A

Hepple wishes to have the additional valid arrows below, where we have decorated the product operator with a superscript ^{H} to indicate that it represents Hepple’s product, and where • is non-commutative, so that in general we have neither A•B → B • A nor its converse:

A ⊗^{H} B → A • B and B ⊗^{H} A → B • A

This all makes sense if we regard A ⊗^{H} B as defined by the modal composition ♣(A, B) (where the underlying structure-building operation (−, −) is noncommutative), accompanied by the structural rule:

\underline{Θ[♣(Γ, Δ)] → C} ; Θ[♣(Δ, Γ)] → C

On this view, A ⊗^{H} B and B ⊗^{H} A represent different logical objects. They still carry information about relative order, even though we allow either type to be transformed to the other. This means that the following structural postulate is motivated:

Θ[(Γ, Δ)] → C ; \overline{Θ[♣(Γ, Δ)] → C}

On the view advocated by Moortgat and me, A ⊗^{M/O} B and B ⊗^{M/O} A are different representations of a single logical object—namely, the type corresponding to the structure-building operation of unordered pairing. It is also possible to think of this in terms of a modalization ♡(A, B) of an ordered structure (A, B), as long as we are willing to regard the modality ♡ as a function mapping both (A, B) and (B, A) to the unordered pair [A, B], so that we have ♡(A, B) = ♡(B, A). But the natural interpretation of the modal ♡ here is simply the forgetful functor mapping ordered pairs to their less structured, unordered counterparts.

From this point of view, then, there are really two logical systems which share a common notation. The relation between the two systems would be considerably clarified by a study of the possibility of embedding one system into the other, in just the same way that the modal embeddings studied by Kurtonina & Moortgat have illuminated the relations among even such basic and well-studied systems as NL and L.

Acknowledgment. The comments of this paper draw extensively on joint work with Michael Moortgat, particularly on parts of a paper on compositions of structurebuilding operations which is currently in preparation.

References

[1] T. S. Blyth and M. F. Janowitz. 1972. Residuation theory. Pergamon Press. Oxford.

[2] M. Hepple. 1993. A general framework for hybrid substructural categorial logics. Ms. IRCS, University of Pennsylvania.

[3] G. Lakoff. 1970. Irregularity in syntax. Holt, Rinehart, and Winston. New York.

[4] M. Moortgat & R. T. Oehrle. 1993. Lecture Notes on Categorial Grammar. European Summer School in Logic, Language, and Information. Faculdade de Letras, Universidade de Lisboa, Portugal.

[5] M. Moortgat & R. T. Oehrle. 1994. Adjacency, dependency and order. In P. Dekker & M. Stokhof, eds., Proceedings of the Ninth Amsterdam Colloquium. illc/Department of Philosophy. Universiteit van Amsterdam.

[6] G. Morrill. 1990. Intensionality and boundedness. Linguistics & Philosophy 13, 699-725.

[7] G. Morrill. 1992. Categorial formalisation of relativisation: pied piping, islands, and extraction sites. Report LSI-92-93-R. Departament de Llenguatges i sistemes informàtics. Universitat Politècnica de Catalunya.

[8] R. T. Oehrle. 1992. Lecture notes for Linguistics 505: Categorial Grammar. Ms. Department of Linguistics, University of Arizona, Tucson.

[9] A. S. Troelstra. 1992. Lectures on linear logic. CSLI Lecture Notes No. 29. CSLI. Stanford.

[10] K. Versmissen. 1993. Categorial grammar, modalities and algebraic semantics. Proceedings EACL93, Utrecht, pp 377–383.