国立情報学研究所准教授金沢誠先生、ペンシルバニア大学数学科及び計算機科学科教授Andre Scedrov先生、リヨン大学哲学科教授Jean-Baptiste Joinet先生をお招きして、Lambek Calculus 及び線形論理に関する次のようなミニ・シンポジウム形式集会を開催いたします。
タイトルをクリックするとアブストラクトを参照できます。 Click for the abstract.
Proof theory generally defines proofs as texts respecting specific norms. From the dialectical point of view, however, a proof is a text able to resist to any argumentative attacks. After having stressed in what respects those two approaches deeply differ, I will investigate how recents approaches from Proof theory and Computing theory permit to unify them.
The Lambek calculus (1958, 1961) is a well-known logical formalism for modelling natural language syntax. The calculus can also be considered as a version of non-commutative intuitionistic linear logic. The Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. The original calculus covered a substantial number of intricate natural language phenomena. In order to address more subtle linguistic issues, the Lambek calculus has been extended in various ways.
For instance, an extension with so-called bracket modalities introduced by Morrill (1992) and Moortgat (1995) is capable of representing controlled non-associativity and is suitable for the modeling of islands. The syntax is more involved than the syntax of a standard sequent calculus. Derivable objects are sequents of the form Gamma --> A , where the antecedent Gamma is a structure called meta-formula and the succedent A is a formula. Meta-formulae are built from formulae (types) using two metasyntactic operators: comma and brackets. In joint work with Max I. Kanovich, Stepan L. Kuznetsov, and Glyn Morrill we give an algorithm for provability in the Lambek calculus with bracket modalities allowing empty antecedents. Pentus (2010) gave a polynomial-time algorithm for determining provability of bounded depth formulas in the original Lambek calculus with empty antecedents allowed. Pentus' algorithm is based on tabularisation of proof nets. Our algorithm for the extension with bracket modalities runs in polynomial time when both the formula depth and the bracket nesting depth are bounded. The algorithm combines a Pentus-style tabularisation of proof nets with an automata-theoretic treatment of bracketing.
Morrill and Valentin (2015) introduce a further extension with so-called exponential modality, suitable for the modeling of medial and parasitic extraction. Their extension is based on a non-standard contraction rule for the exponential, which interacts with the bracket structure in an intricate way. The standard contraction rule for exponentials is not admissible in this calculus. In joint work with Max I. Kanovich and Stepan L. Kuznetsov we show that provability in this calculus is undecidable and we investigate restricted decidable fragments considered by Morrill and Valentin. We show that these fragments belong to NP.
Every language recognized by the Lambek calculus with brackets is context-free. This is shown by combining an observation by J\"ager with an entirely straightforward adaptation of the method Pentus used for the original Lambek calculus. The case of the variant of the calculus allowing sequents with empty antecedents is slightly more complicated, requiring a restricted use of the multiplicative unit.