Display Calculi Meet Categorial Type Logics
Display CalculimeetCategorial Type LogicsRajeev P. GoréAutomated Reasoning GroupComputer Sciences LaboratoryResearch School of Information Sciences and EngineeringAustralian National UniversityCanberra, ACT, 0200, AustraliaANU CRICOS Provider Number - 00120CRajeev.Gore@anu.edu.auandRaffaella BernardiKRDB, Faculty of Computer ScienceFree University of Bolzano-BozenP.zza Domenicani 339100 Bolzano-Bozen, Italybernardi@inf.unibz.itThe authors thank the Free University of Bolzano-Bozen for the travel and accommodationsubsidizes provided to the second teacher and for the financial support given to the first teacherwhile visiting the KRDB group in the preparatory phase of this course. Furthermore, a specialthank goes to the ESSLLI local organizers for their financial and technical support.
ContentsAbstractvI1Introduction to DC and CTL1 Where do we stand?1.1 Formal Grammars . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1.2 Logic and NLP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2 Introduction to DC2.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2.1 Residuation and Galois Connected Logical Connectives . .2.2.2 Unary Modalities . . . . . . . . . . . . . . . . . . . . . . .2.2.3 Unary Negations . . . . . . . . . . . . . . . . . . . . . . .2.2.4 Binary Connectives . . . . . . . . . . . . . . . . . . . . . .2.2.5 Resource Sensitivity . . . . . . . . . . . . . . . . . . . . .2.3 Proof Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.3.1 Axiomatic Presentation . . . . . . . . . . . . . . . . . . . .2.3.2 Sequent Calculi . . . . . . . . . . . . . . . . . . . . . . . .2.3.3 Cut And Its Elimination . . . . . . . . . . . . . . . . . . .2.3.4 Why Move To Other Proof Systems? . . . . . . . . . . . .2.4 Display Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.4.1 Formulae and Structures . . . . . . . . . . . . . . . . . . .2.4.2 Sequents and Sequent Rules . . . . . . . . . . . . . . . . .2.4.3 Structural Rules . . . . . . . . . . . . . . . . . . . . . . . .2.4.4 Logical Rules . . . . . . . . . . . . . . . . . . . . . . . . .2.4.5 Display Postulates, Antecedent Parts and Succedent Parts2.4.6 Display Theorem . . . . . . . . . . . . . . . . . . . . . . .2.4.7 Soundness and Completeness . . . . . . . . . . . . . . . .2.4.8 Cut Elimination . . . . . . . . . . . . . . . . . . . . . . . 28
2.4.9 Gentzen Overloading . . . . . . . . . . . . . . . . . . . . . . . . .2.4.10 Encoding Axioms Via Structural Rules . . . . . . . . . . . . . . .3 Displaying CTL3.1 Capturing Residuation . . . . . . . . . . . . . .3.2 The Logic of Residuation NL . . . . . . . . . . .3.2.1 The Residuated Unary Operators NL(3)3.2.2 Kripke Models . . . . . . . . . . . . . . .3.2.3 Structural Constraints . . . . . . . . . .3.3 Displaying Residuation and Galois Connection .3.3.1 Residuation . . . . . . . . . . . . . . . .3.3.2 Galois Connected Operations . . . . . .3.3.3 Axiomatic Presentation of NL(3,·0 ) . . .3.4 Derivability Patterns . . . . . . . . . . . . . . .3.5 Key Concepts . . . . . . . . . . . . . . . . . . .II.Linguistic Analyses3030333333353637383842424950514 The Logical Approach in Linguistics4.1 Rule-Based Categorial Grammars . . . . . . . . . . .4.1.1 Classical Categorial Grammar . . . . . . . . .4.1.2 Combinatory Categorial Grammar . . . . . .4.2 A Logic of Types . . . . . . . . . . . . . . . . . . . .4.2.1 Parsing as Deduction . . . . . . . . . . . . . .4.2.2 Logical Rules and Structural Rules . . . . . .4.3 The Composition of Meaning . . . . . . . . . . . . .4.3.1 Semantic Types and Typed Lambda Terms . .4.3.2 Interpretations for the Sample Grammar . . .4.4 Putting Things Together . . . . . . . . . . . . . . . .4.4.1 Rule-Based Approach vs. Deductive Approach4.4.2 Curry-Howard Correspondence . . . . . . . .4.5 Key Concepts . . . . . . . . . . . . . . . . . . . . . .5 Modalities for Partial Orderings5.1 Zooming in on the Semantic Domains . . . . .5.2 QP Classification . . . . . . . . . . . . . . . .5.2.1 Feature Checking Theory for QP Scope5.2.2 Controlling Scope Distribution in CTL5.3 Classification of Polarity Items . . . . . . . . .5.3.1 Licensing Relations in CTL . . . . . . .5.3.2 Cross-linguistic differences . . . . . . .5.3.3 Antilicensing Relations in CTL . . . . .5.4 Key Concepts . . . . . . . . . . . . . . . . . .79. 79. 81. 83. 85. 94. 96. 98. 106. 109Bibliography.5353545658596168697173737478111iv
AbstractContent The work presented in this course follows the parsing as deduction approachto Linguistics. We use the tools of Categorial Type Logic (CTL) to study the interfaceof natural language syntax and semantics. Our aim is to investigate the mathematicalstructure of CTL and explore its expressivity for analyzing natural language structures.Standard presentations of CTL using Gentzen’s Sequent Calculus or Proofnets areprototypical examples of a logical account of natural language analysis. Nevertheless, thelimitations of these proof systems surface when one tries to fully explore the ’theoreticalspace’ for type-logical connectives. We show how the generalized sequent framework ofDisplay Calculi (DC) improves upon the traditional accounts, and in particular, how itopens new perspectives on the treatment of negative structure.Such expressivity is required if one wants to enrich the type-logical vocabulary withantitone connectives, in addition to the more familiar isotone operations. Phenomenaof polarity sensitivity, pervasive in natural languages, suggest that such extensions aredesirable.Structure The course consists of two main components: The proof theoretical &model theoretical background of CTL and the modeling of linguistic phenomena. Throughthe course these two components will be mixed after a first separate introduction to eachof them providing the technical background and the motivations of the approach.Pre-requisite The course is addressed to any student interested in logic, languageand their connections, and only basic background on propositional logic is required.Students with knowledge of categorial grammar and proof theory will, of course, obtainfurther profit.ESSLLI’s related courses The course can be seen as a continuation of the foundational course on ”Substructural Logics” given by Greg Restall at ESSLLI 01 (Helsinki).In particular, we will show substructural logics at work by focusing on a specific one(CTL) and by zooming in on the linguistic applications only mentioned by Restall.Three closely related courses given at ESSLLI 04 are the introductory courses on“Type logical grammar” and “Proof automation for type-logical grammars” (by Glynv
Morrill and Pierre Casteran & Richard Moot, respectively.) and the advanced courseon “Multi-modal combinatory categorial grammar” (by Geert-Jan Kruijff).References The course notes have been mostly extracted from [Ber02] and [Gor98c,Gor97]. In the course, at the end of each lecture we will provide further reading materialthat can be downloaded from the CoLogNET portal of the “Logic and Natural LanguageProcessing Area”: http://colognet.let.uu.nl.Exercises For the linguistic applications, we will propose some exercises to check yourunderstanding of the presented material. You will be able to check them your selves,via the on-line version of Grail at: http://grail.let.uu.nl.vi
Part IIntroduction to DC and CTLIn this part of the notes, we introduce the formal background behind the GrammarLogic we will put at work in the second part of the notes. In particular, we focusattention on the type-forming operations of Categorial Type Logic (CTL), which buildstructured complex categories out of a small set of basic types. We show how theanalytical force of these type-forming operations derives from the fact that they comein pairs of opposites —residuated or Galois connected pairs, to be more precise. Wehave all become acquainted with these notions in our elementary math classes, whenwe learned how to solve algebraic equations like 3 x 5 by ‘isolating’ the unknown xusing the laws connecting ( , ), producing the solution x 35 . In categorial grammar,such pair of opposites is used to put together and take apart linguistic expressions, bothsyntactically and semantically.In Chapter 1, we try to set CTL within the “Language & Logic” big ombrella, brieflypointing to its main pecularities.In Chapter 2, we provide the algebraic notions of residuation and Galois that governthe behavior of the type-forming operations of CTL and introduce Display Calculi (DC)as a unified framework for presenting resource and structure sensitive reasoning.In Chapter 3, we introduce CTL by means of DC sheding lights on the proof theoretical beahvior of CTL operators. Moreover, we study the derivability relations we willsee at work in Part II.
Chapter 1Where do we stand?This course is part of the “Logic & Language” Session of ESSLLI’04. As such, wewould like to start in this preliminary and informal chapter from the very broad areaand zoom into the framework we will be introducing in the course. In this way wehope to help the reader grasping the main properties of the framework and spottingsimilarities and differences with what he/she labels as “Logic & Language”. We willstart from Computational Linguistics, move to Formal Grammars and end with LogicalGrammars.1.1Formal GrammarsFormal Grammars are an area of investigation of Computational Linguistics. The fieldis as diverse as linguistics itself, in general it could been seen as the study of formaldevices which can be used to distinguish grammatical and ungrammatical strings of agiven language [CCCSS00] and build their semantic interpretation. These formal devicescan be automata, which are abstract computing machines, and formal grammars, whichare string (or structure) rewriting systems. Formal Grammars are used by parsers todetermine the “syntactic structure” of string of words. See [Mit03] for an overview ofthe field.The object of this course is a formal grammar. Here we point out the major tasks offormal grammars and the devices that are used to carry them out by briefly comparingContext-Free Phrase Structure Grammars with the framework object of our studying,Categorial Grammars (CG)1 .Phrase Structure Grammars. In formal language theory a language is defined asa set of strings, i.e. a set of finite sequences of vocabulary items. A grammar for alanguage then is a formal device that defines which strings belong to that language.One particular kind of formal system that is used to define a language is commonlyknown as a context-free phrase structure grammar. Besides deciding whether a string1This section is extracted (and adapted) from [Hey99] with the author’s permission. We thank Dirkfor this.3
4Chapter 1. Where do we stand?belongs to a given language, this grammar deals with phrase structures represented astrees.An important difference between strings and phrase structures is that whereas stringconcatenation is assumed to be associative, trees are bracketed structures. The latterthus preserve aspects of the compositional (constituent) structure or derivation which islost in the string representations. We illustrate the behavior of this grammar by meansof the example below.Example 1.1. [Grammars and Languages]We consider a small fragment of English defined by the following grammar G ( hLEX, RULESi), with vocabulary Σ and categoriesCAT.Σ {Sara, dress, wears, the, new},CAT {det, n, np, s, v, vp, adj},LEX {hSara, npi, hthe, deti, hdress, ni, hnew, adji, hwears, vi}RULES {s np vp, np det n, vp v np, n adj n}Among the elements of the language recognized by the grammar, L(G), are hthe, detibecause this is in the lexicon, and hSara wears the new dress, si which is in the languageby the repeated application rules.(1) hnew dress, ni L(G) becausen adj n RULES,hnew, adji L(G) (LEX), andhdress, ni L(G) (LEX)(2) hthe new dress, npi L(G) becausenp det n RULES,hthe, deti L(G) (LEX), andhnew dress, ni L(G) (1)(3) hwears the new dress, vpi L(G) becausevp v np RULES,hwears, vi L(G) (LEX), andhthe new dress, npi L(G) (2)(4) hSara wears the new dress, si L(G) becauses np vp RULES,hSara, npi L(G) (LEX), andhwears the new dress, vpi L(G) (3)In a similar way we can show that the set of phrase structure trees (T (G)) contains thefollowing tree which we also depict in the usual graphical way.hhSara, npi, hhwears, vi, hhthe, deti, hhnew, adji, hdress, ni, ni, npi, vpi, si
1.1. Formal Grammars5snpSaravpvwearsnpdetthenadjnnew dressAs the following table shows, we can also derive that the sentence is in the languageby means of a rewriting procedure. The left column represents the sequence of categoriesand words that is arrived at by replacing one of the categories (c) (identical to the lefthand side of the rule in the second column) on the line above by the right-hand side ofthe rule or by a word that is assigned the category c by the lexicon.snp vpnp v npnp v det nnp v det adj nSara v det adj nSara wears det adj nSara wears the det adj nSara wears the new nSara wears the new dresss np vpvp v npnp det nn adj nhSara, npihwears, vihthe, detihnew, adjihdress, niThis example recapitulates the basic definitions of grammar and language isolatingsome of the functions a grammar is required to serve. In particular, it shows that theprincipal tasks of a grammar are the definition of several sets of objects: (i) a set ofexpressions (the string set), (ii) a set of pairs of expressions and categories (language),(iii) a set of phrase structures. More abstractly, we can say that a grammar is a devicethat is concerned with two aspects.(1) Defining the membership of elements to some (sub)set: classification or categorisation.(2) Specifying the compositional structure of complex elements.The grammars that we introduced categorise expressions in two steps. The lexiconcomponent LEX of a grammar deals with the categorisation of the atomic expressions(the words), whereas the RULES determine the category of complex expressions. Therules also take care of the definition of compositional structure. They define which partscan combine to form larger structures. Categories play an important role in definingthe compositional structure because they group together the set of expressions thatbehave similarly with respect to compositional structure. In other words, the rulesmake reference to the categories, not to the individual expressions.
6Chapter 1. Where do we stand?Besides classification, another important function of a grammar is to define structure. Analysing this aspect, we can say that the context-free grammar fixes the order of(sub)expressions (precedence) and a part-whole structure (dominance). Phrase structure trees make this compositional structure and the categorisation of wholes and partsexplicit. We will now turn to another type of grammar that performs the same tasks ina different way and which is the ancestor of the logical grammar presented in the course.Categorial Grammars. The formal grammar we work with, Categorial Grammars(CG), adopts an alternative way to define classification and composition. In this type ofgrammar the lexical component takes over the role of the rule component in fixing thecompositional structure of a language. It is important to notice how in order to effectthis, the notion of category is modified.CG have a richer notion of category than Phrase Structure Grammars. Besidesatomic categories, they also use complex categories of the form A/B and (B\A) (whereA and B are again categories, possibly complex themselves.) A language is definedsolely by a lexicon that assigns categories to words. There are no phrase structure rules.Instead, a pair of general combination operations is used: (1) an expression in A/Bconcatenated with an expression of category B gives an expression in A (see (a) below);(2) an expression in B concatenated with an expression in B\A gives an expressionin A (the schema is symmetric to (a)). Notice that these schemata do not mentionspecific categories, but use variables over arbitrary categories A, B. The informationabout precisely which expressions combine with others is provided by the lexicon. Forinstance, an adjective, such as new, might be assigned the category n/n, which, by thegeneral schema, means that it combines with expressions in n to form expressions in n.Representing this composition in a tree we have (a’) that plays the role of the phrasestructure in (b).(a)(a’)(b)AnA/BBwordiwordjn/nnnnew dressadjnnew dressNote that CG categories could be seen as trees themselves and therefore are closeto the elementary trees of Tree Adjoining Grammar (TAG). The reader is referred tothe foundational course given by B. Gaiffe and G. Perrier “Basic Parsing Techniquesfor natural language” (ESSLLI 04) for an introductory comparison of CG and TAG andto [Moo02] for a formal embedding of (a version of) the former into the latter.From this elementary summary, it should be clear how classification and composition are defined in this alternative framework. One thing that is important to underlineis that the classification of expressions by the categories directly expresses their combination properties. These aspects will be spelled out in precise terms in Chapter 4where it is also shown how moving from Classical CG to Categorial Type Logic (CTL)corresponds to move from a formal grammar to a logic grammar where categories are
1.2. Logic and NLP7logical formula and rules are logical rules. Here we try to briefly explain the place CTLoccupies within the “Logic and Natural Language Processing” (LNLP) area.1.2Logic and NLPIn several fields Logic is used to grasp the global features of reality abstracting awayfrom the empirical details and providing a model of the observed objects. In our case,the object is natural language. Logic has been recognized to be an important tool forunderstanding the structure of language (both its syntax and semantics) since [Fre87].Moreover, inference tools are a crucial component of Natural Language Processing (NLP)systems that require deep analysis which integrate semantic analysis of natural languageutterances to their general cognitive processing. Valuable references for foundational andadvanced introductions to the field are [PMW90, vBtM97].Since 1995 an European Conference on Logical Aspects of Computational Linguistics(LACL) is organized every two years. In the introduction of LACL’96 proceedings thefield is classified in (i) logical semantics of natural language, (ii) grammar and logic, (iii)mathematics with linguistic motivations, and (iv) computational perspectives. Followingthis division, if we have to chose one label, we can say that the framework presentedin the course follows under the “grammar and logic” one. As before, we would like tohighlight the main aspects in which CTL differs from other logical views on grammars.Logic Based Grammars. One known example of a family of logics used to accomplish NLP tasks are Feature Logics [Rou97]. They are known to be especially usefulin classifying and constraining the linguistic objects known as feature structures. Here,the logic is used to formalize linguistic theories. For instance, the feature co-occurrencerestriction used in Generalized Phrase Structure Grammar (GPSG) to say that anyc
formal grammars and the devices that are used to carry them out by briefly comparing Context-Free Phrase Structure Grammars with the framework object of our studying, Categorial Grammars (CG)1. Phrase Structure Grammars. In formal language theory a language is defined as a set of st
1 IntroductionOn categorial grammars and learnabilityLogical Information Systems (LIS)Categorial grammars and/as LISAnnex Plan 1 Introduction 2 On categorial grammars and learnability 3 Logical Information Systems (LIS) 4 Categorial grammars and/as LIS 5 Annex Annie Foret IRISA & Univ. Ren
context free grammars, have already been applied to music genera-tion [6]. Categorial grammars are another linguistic formalism that have proved useful to the study of music. 3 Categorial Grammars in Language In 1935, semanticist Kazimierz Ajdukiewicz introduced the concept of categorial gr
Categorial Grammar (CG) is a lexicalized formal grammar well known for its tied connection between syntax and semantics. ariantsV of it (Combinatory Categorial Grammar, CCG, and Categorial ypeT Logic, CTL) have been used to reach wide coverage grammars for Engli
Categorial Grammar The term Categorial Grammar names a group of theories of natural language syntax and semantics in which the main responsibility for defining syntactic form is borne by the lexicon. (M. Steedman) Categorial Grammars (CGs) developed as an alternati
Towards Abstract Categorial Grammars Ph. de Groote, 2001 We introduce a new categorial formalism based on intuitionistic linear logic. This formalism, which derives from current type-logical grammars, is abstract in the sense that both syntax
From CFG to AB grammars Proposition 2 Every "-free Context-Free Grammar in Greibach normal form is strongly equivalent to an AB categorial grammar. Thus every "-free Context-Free grammar is weakly equivalent to an AB categorial grammar. PROOF:Let us consider the following AB grammar: IIts words are the terminals of the CF
general Abstract Categorial Grammars can be reduced to the provability problem for Multi-plicative Exponential Linear Logic. It follows essentially a similar reduction by Kanazawa, who has shown how the parsing problem for second-order Abstract Categorial Grammars reduces to datalog querie
API RP 505, Recommended Practice for Classification of Locations for Electrical Installations at Petroleum Facilities Classified as Class I, Zone 0, Zone 1, and Zone 2, 2002, reaffirmed 2013. 2.3.2 ASHRAE Publications. American Society of Heating, Refrigeration and Air-Conditioning EngineersASHRAE, Inc., 1791 Tullie Circle NE, Atlanta, GA 30329-2305. ASHRAE 15ASHRAE STD 15, Safety Standard for .
