Curry-Howard同型対応
命題は型に対応し、証明はプログラムに対応するというもの
ゲンツェンの自然演繹(NK)と型付きラムダ計算は記法が異なるだけでやっていることは同じ
1958年
めっちゃ古いんやな
直観主義論理周辺の話
と、wikiに書いているが、特に黒田の方はわからん
対応する、と言ったらしい
参考
『論理の哲学』 p.206
>CPS変換は、二重否定による古典論理の直観主義論理への埋め込みにあたる。また、古典論理そのものは、Schemeの call-with-current-continuation 制御演算子のように、継続を直に扱うことができるプログラミング言語に対応する ref
関連
参考
『論理の哲学』 7章
pdf本
コレを読み進めていけばいい？
いろんな記事で頻繁に引用されている
記法、図法
typescript
めっちゃおもろ
>@lotz84_: "Lecture Notes on the Lambda Calculus"
>2001, 2007, 2013年に大学で行われた講義を元に作られた120頁に渡るレクチャーノート
>内容はラムダ計算、チャーチロッサーの定理、コンビネータ代数、単純型付ラムダ計算、カリーハワード同型対応、弱/強正規化など多岐に渡っている
>
