“Lambek Calculus and Linear Logic” 研究集会

国立情報学研究所准教授金沢誠先生、ペンシルバニア大学数学科及び計算機科学科教授Andre Scedrov先生、リヨン大学哲学科教授Jean-Baptiste Joinet先生をお招きして、Lambek Calculus 及び線形論理に関する次のようなミニ・シンポジウム形式集会を開催いたします。


日時・会場
日時:
Jan. 25th, Thurs. 2018 / 2018年1月25日(木) 15:30 - 18:30
場所:
8F, East Building, Mita Campus of Keio University / 慶應義塾大学三田キャンパス東館8階ホール
Building #3 on this map. / キャンパスマップ3番の建物です。
招待講演者 / Speakers
  • Jean-Baptiste Joinet教授 (リヨン第3大学哲学科・パリ高等師範学校カバイエス研究センター)
  • Makoto Kanazawa准教授 (国立情報学研究所NII)
  • Andre Scedrov教授 (ペンシルバニア大学数学科および計算機科学科)
プログラム・アブストラクト / Program and Abstracts

タイトルをクリックするとアブストラクトを参照できます。 Click for the abstract.

  • 15:20 Registration
  • 15:30-16:30 Jean-Baptiste Joinet (リヨン第3大学哲学科・パリ高等師範学校カバイエス研究所)
    “Logic and Dialectical Time”

    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.

  • 16:30-17:30 Andre Scedrov (ペンシルバニア大学数学科および計算機科学科)
    “Lambek Calculus Extended with Bracket and Subexponential Modalities”

    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.

  • 17:30-18:30 Makoto Kanazawa (国立情報学研究所NII)
    “On the Recognizing Power of the Lambek Calculus with Brackets”

    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.

ローカルオーガナイザー / Local Organizers
  • 岡田 光弘 (慶應義塾大学文学部哲学専攻)
  • 西牟田 祐樹 (慶應義塾大学後期博士課程)
共催
  • 慶應義塾大学 論理と感性のグローバル研究センター
  • 次世代研究推進プロジェクト
  • CNRS(フランス)
連絡先
慶應義塾大学文学部 岡田光弘研究室
東京都港区三田2−15−45
Email: logic@abelard.flet.keio.ac.jp