Logics of Structured Resources

Michael Moortgat (editor)

DYANA-2

Dynamic Interpretation of Natural Language

esprit Basic Research Project 6852 Deliverable R1.1.C September 1995

Logics of Structured Resources

Michael Moortgat Universiteit Utrecht

(editor)

authors:

Natasha Kurtonina and Michael Moortgat

Natasha Kurtonina Martin Emms

DYANA-2

Dynamic Interpretation of Natural Language

esprit Basic Research Project 6852 Deliverable R1.1.C September 1995

esprit Basic Research Project 6852 dyana-2

Dynamic Interpretation of Natural Language

Universiteit van Amsterdam Institute for Logic, Language and Computation (ILLC)

University of Edinburgh Centre for Cognitive Science (ECCS)

Universität München Centrum für Informations- und Sprachforschung (CIS)

Universitetet i Oslo Department of Linguistics and Philosophy (ILF)

Universität Stuttgart Institut für Maschinelle Sprachverarbeitung (IMS)

Universität Tübingen Seminar für Sprachwissenschaft (SfS)

Universiteit Utrecht Research Institute for Language and Speech (OTS)

For copies of reports, updates on project activities and other dyana-related information, contact:

The dyana-2 Project Administrator ILLC/Department of Philosophy University of Amsterdam Nieuwe Doelenstraat 15 NL-1012 CP Amsterdam

http://www.fwi.uva.nl/research/illc/dyana/Home.html

\begin{matrix}c \\ ◯ \end{matrix} 1995, The Individual Authors

No part of this document may be reproduced or transmitted in any form, or by any means, electronic or mechanical, including photocopy, recording, or any information storage and retrieval system, without permission from the copyright owner.

Contents

Introduction by the editor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . v

Task 1.1, subtask 2: Logics of Structured Resources Structural Control Natasha Kurtonina and Michael Moortgat . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

Task 1.1, subtask 2: Logics of Structured Resources Labelling and Completeness for Categorial Resource Logics Natasha Kurtonina . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

Additional Contribution An Undecidability Result for Polymorphic Lambek Calculus Martin Emms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

Introduction

This deliverable contains three contributions addressing logical foundations of the multimodal and polymorphic categorial architectures.

structural controlThe paper by Kurtonina and Moortgat develops the earlier work in [1] into a full theory of communication between categorial resource logics. Substructural communication is obtained in terms of the extension of the categorial vocabulary with a pair of unary residuated modal operators , proposed in [2, 3]. A general result is established showing that the unary modal operators, in interaction with the standard binary vocabulary, provide full control over the grammatical dimensions of precedence, dominance and dependency. The control allows both for the imposition of structural constraints in regimes with a flexible resource management, and for licensing structural relaxation in regimes with a more stringent structure sensitivity. Technically the theory of structural control is implemented via two-way embeddings, with a stronger system as target logic and a weaker neighbour as the source logic, and vice versa. The embeddings differ interestingly from the Linear Logic embedding on the basis of a ‘!’ modality in their bidirectionality, and in the fact that the more delicate resource control for the categorial logics does not presuppose S4 properties for the modal operators.

The results in the paper by Kurtonina and Moortgat throw a new light on a number of issues that have come up in the course of the dyana project.

Structural composition versus meaning composition With respect to the syntax-semantics interface, different dyana contributions have drawn attention to the tension between semantic expressivity and syntactic discrimination. Viewing categorial types from a semantic perspective, there is a natural correlation between proofs/derivations and the construction of ‘meaning recipes’ in terms of (a Linear Logic refinement of) the Curry-Howard correspondence. Moving to the syntactic perspective, one can refine the categorial vocabulary to take into account the structural factors of grammatical composition. But the price one pays for structural refinement is the loss of readings (LP theorems).

The embedding results in the present contribution suggest a division of labour between ‘syntax’ and ‘semantics’ which may help in resolving the tension at the syntax-semantics interface. The system LP can play the role of the default semantic composition language — it provides the natural locus for the statement of the Curry-Howard correspondence. Similarly, the pure residuation logic NL can serve as the default language of structural composition: moving beyond the NL notion of derivability requires the introduction of structural postulates and the corresponding frame constraints — structural postulates, in other words, have their ‘meaning’ in the general models that provide the structural semantics of the grammatical resources. The embedding results then guarantee that the intermediate space between these two extremes can be navigated by means of the modal control operators.

Controlling the proliferation of modesThe move from simple Lambek systems to the multimodal architecture of Deliverable R1.1.B94 was originally motivated by the introduction of different forms of grammatical composition with ‘observable’ properties to discriminate between them, e.g. the distinction between regular phrasal composition and the form of composition that realizes clitic-head adjunction, cf. [4]. But many multimodal accounts have moved beyond this ‘realistic’ interpretation of the modes of grammatical composition — they have introduced interaction principles on the basis of ‘phantom’ modes that play a crucial role in the process of grammatical reasoning, but that will never surface in the end-sequents representing the structural configuration of the grammatical resources. Examples of this more abstract treatment of modes can be found in Moortgat and Oehrle’s [5] account of verb raising, or Morrill’s [6] wrapping proposals. The multimodal architecture, because of its essential open-endedness, does not give sharp theoretical limitations on the varieties of grammatical composition. Still, in general, one would like to have strategies for restricting the unconstrained proliferation of modes.

The enrichment of the categorial vocabulary with unary modalities , provides precisely such a tool: from a given default •, one can obtain a scala of variants with different resource management properties by definition in terms of modal decoration. A simple illustration would be the dependency logics of [7]. The distinction between left and right headed products does not really require a move from a unimodal • to a bimodal •_{l}, •_{r} setting: the left and right headed products are definable from the default • as (−) • − and − • (−), respectively.

Type logic versus feature-logicIn [8] one finds a further result along these lines which is included here in the Appendix. There it is shown that the binary categorial operators themselves can be expressed in terms of unary modal operators and the standard Boolean vocabulary. Technically, the result takes the form of a faithful embedding of the non-associative Lambek Calculus into minimal bimodal tense logic K_{1,2}^{t} on the basis of the following translation.

\begin{aligned}p^{♯} & = & p \\ (A • B)^{♯} & = & ◇_{1}(◇_{1}A^{♯} & ◇_{2}B^{♯}) \\ (AB)^{♯} & = & □_{2}^{↓}(◇_{1}A^{♯} ⊃ □_{1}^{↓}B^{♯}) \\ (B/A)^{♯} & = & □_{1}^{↓}(◇_{2}A^{♯} ⊃ □_{1}^{↓}B^{♯}) \end{aligned}

This decomposition suggests a homogeneous mixture of the type-logical and the feature-logical languages. From the perspective of frame semantics, the language of feature logic is simply a multimodal language with binary feature transitions R_{f} interpreting the attributes as existential modal operators ⟨f⟩. The tense modalities _{1},_{2} (and their universal duals) which provide the decomposition of the categorial /, •, operators, could be added straightforwardly to the attribute vocabulary. This strategy for combining type and feature logic, and its relation with the fibering approach of [9] must be left here as a topic for further research.

labelling and completenessThe contribution of Kurtonina develops a general labelled deductive perspective on the landscape of categorial resource logics. In line with Gabbay’s [10] concept of ‘simulation’, the sequent calculus for LP (i.e. the multiplicative fragment of Linear Logic) is taken as the basis for the labelled presentations. The LP calculus captures the resource sensitivity of categorial deduction which is shared by all the ‘sublinear’ logics. Adding a labelling discipline to the LP proof theoretic core engine, one recaptures the finer notions of structural discrimination that characterize the logics weaker than LP. The labelling discipline thus makes it possible to simulate the more delicate notions of categorial deduction from the perspective of (labelled) LP.

Two important design properties of the labelling discipline proposed in this contribution are uniformity and completeness. Uniformity is obtained by grounding the labelling regime in the pure residuation logic NL. As we have seen in [11], from the pure residuation logic one unfolds the categorial landscape via the addition of structural postulates for resource management. The structural postulates correspond in a systematic fashion with operations in the labelling algebra. In order to show that the simulation of structure sensitive notions of categorial inference through labelling is indeed faithful, Kurtonina establishes a completeness result for the labelling discipline with respect to the general frame semantics for the logics under consideration. It is shown that the proposed labelling regime supports the generalized categorial architecture of [11] with mixed styles of inference, and n-ary families of type constructors, specifically, unary control modalities in combination with the standard binary vocabulary.

Kurtonina’s paper develops a logical perspective on labelled categorial deduction. In computational studies of categorial grammar, labelling is introduced as a tool to obtain efficient parsing strategies. A topic for further research would be to see how the general labelling method developed in this paper can be combined with the compilation techniques of [12, 13] that allow for efficient checking of subproblems of the general labelling problem in terms of optimized data-structures.

undecidability of second order lambek calculusIn the final contribution to this deliverable, Martin Emms establishes the undecidability of second order Lambek calculus. The result is based on recent work of [14] who show that second order intuitionistic propositional logic (LJ2) — which is known to be undecidable — can be embedded into the multiplicative fragment of second order intuitionistic Linear Logic (IMLL2). The key idea of the embedding is to reintroduce the structural rules of Contraction and Weakening that differentiate between LJ2 and IMLL2 in the shape of second order IMLL2 formulae ∀X.X−∘(X ⊗ X) and ∀X.X−∘I. Emms extends the strategy to the structural rule that differentiates between IMLL2 (i.e. LP) and L — the rule of Permutation, which is reintroduced via the second order formula ∀X∀Y.((X •Y)/X)/Y.

The undecidability result for polymorphic L provides extra motivation for the search for restricted forms of categorial polymorphism with pleasant decidability properties, cf. [15] for exploration of this issue. Also, the undecidability result suggests an interesting general question in relation to the embeddings in the first contribution to this deliverable: could one design a general embedding strategy based on second-order encoding of structural postulates such that the undecidability of IMLL2 would carry over to the full sublinear landscape? A positive answer is conjectured at the end of Emms’ contribution. The question remains open for the time being — again, a fruitful area for further investigation.

References

[1] Kurtonina, N. and M. Moortgat (1994) ‘Controlling resource management’. In Moortgat (ed.) Deliverable R1.1.B.

[2] Moortgat, M. (1994) ‘Residuation in mixed Lambek systems’. In Moortgat (ed.) Deliverable R1.1.B.

[3] Moortgat, M. (1995) ‘Multimodal linguistic inference’. IGPL Bulletin Vol 3 (2,3), pp 371–402. (To appear in JoLLI.)

[4] Kraak, E. (1995) ‘French object clitics: a multimodal analysis’. In Leiss (ed.) Deliverable R1.3.C.

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

[6] Morrill, G. (1994) Type Logical Grammar. Kluwer, Dordrecht.

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

[8] Kurtonina, N. (1995) Frames and Labels. A Modal Analysis of Categorial Inference. PhD Dissertation, OTS Utrecht, ILLC Amsterdam.

[9] Dörre, J., D. Gabbay and E. König (1994) ‘Fibred semantics for featurebased grammar logic’. In Dörre (ed.) Deliverable R1.2.B.

[10] Gabbay, D. (1994) Labelled Deductive Systems. Volume 1 — Foundations. Report MPI–I–94–223, Max-Planck Institut für Informatik, Saarbr˘”cken.

[11] Kurtonina, N. and M. Moortgat (1995) ‘Structural Control’. This volume.

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

[13] Morrill, G. (1995) ‘CATLOG. A compiler and parser for type-logical grammar’. Dyana-2 Prototype P3.5.

[14] Lincoln, P. et al. (1995) ‘Decision problems for second-order Linear Logic’. Proceedings LICS’95.

[15] Emms, M. (1993) ‘Parsing with polymorphism’. Proceedings EACL, OTS

Utrecht.

Utrecht, September 1995 Michael Moortgat

Task 1.1, subtask 2 Logics of Structured Resources

Structural Control

Natasha Kurtonina and Michael Moortgat

(Universiteit Utrecht)

Labelling and Completeness for Categorial Resource Logics

Natasha Kurtonina

(Universiteit Utrecht)

Additional Contribution

An Undecidability Result for Polymorphic Lambek Calculus

Martin Emms

(Universität München)