カリー／ハワード／ランベック対応

カリー／ハワード／ランベック対応(Curry-Howard-Lambek correspondence)

型理論、論理、圏論の対応について

カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論（ラムダ計算を含む）」「論理」「圏論」の三分野の概念のあいだの精密・詳細な対応を与えてくれます。しかし、言葉はうまく対応してくれません。異なる分野の言語・文化・習慣にはギャップがあるからです。