ラムダ計算の本

言語 数学

twitterで「ラムダ計算が分かっているとはどういうことか、言語学者はほぼ分かっていない」という発言を（気軽に）したら、「もう一歩踏み込んで書いて欲しい」というご要望を頂きました。

僕自身、型理論の専門家と議論をしていると勉強不足を感じることが多い段階なのですが、専門家に笑われるのを厭わずに、「もし自分が今の段階でラムダ計算の本を書くとしたら、こんな内容になるのではないか」という目次を書いてみました。

  1. Untyped Lambda Calculus
    1. Motivation
    2. Syntax
    3. Reduction
    4. Fixedpoint Operator
    5. Turing Completeness
    6. Church-Rosser Theorem
  2. Simply-Typed Lambda Calculus
    1. Judgments
    2. Products and Sums
    3. Weak Normalization
    4. Strong Normalization
  3. Curry-Howard Isomorphisms
    1. Type = Proposition
    2. Term = Proof
    3. Cut elimination
  4. Continuations
    1. Lambda-mu Calculus and Classical Logic
    2. Shift and Reset Operators
  5. Combinatory Logic
    1. Combinators
    2. Hilbert-style Proof
  6. Higher-order Theories
    1. Polymorphic Type Theory
    2. Dependent Type Theory
    3. Lambda Cube
  7. Substructural Lambda Calculus
    1. Linear Lambda Calculus
    2. Full Lambek Lambda Calculus (FL)
    3. Non-associative Lambek Calculus (NL)
    4. Combinatory Categorial Grammar (CCG)
  8. Categorical Semantics
    1. Basic Category Theory
    2. Cartesian Closed Category (CCC)
    3. Monoidal Close Category
    4. Monad

問題は、このうちどこまでが「言語学者にとって最低限必要な内容」なのか、ということなのですが、おそらく上記の内容はすべて言語学と深い関係があると思われます。どの段階も、言語学的議論の宝庫といえるのではないでしょうか。