Curry-Howard同型対応
命題は型に対応し、証明はプログラムに対応するというもの
ゲンツェンの自然演繹(NK)と型付きラムダ計算は記法が異なるだけでやっていることは同じ
1958年
めっちゃ古いんやなmrsekut.icon
The formulae-as-types notion of construction
William Alvin Howard
table:大まかな対応
論理 プログラミング
証明 プログラム
論理式 型
命題 P⊃Q 型P→Q
命題 P∧Q 型P×Q 直積型
Pの証明 型Pの項t
命題Pが証明可能 型Pを持つ項が存在する
証明の簡約化 プログラムの評価
または bool, if..then..else
∀ 多相型
含意 関数
連言 レコード
選言 バリアント
二階直観主義論理 System F
直観主義論理 Calculus of Constructions
table:推論規則の対応の例
ゲンツェンの自然演繹(NK) 型付きラムダ計算
Modus Ponens 関数適用の規則T-App
→導入規則 ラムダ抽象の型付け規則T-Abs
直観主義論理周辺の話
table:継続
論理 プログラミング
パースの法則 call/cc
否定翻訳 名前呼びCPS変換
黒田成勝の否定翻訳 値呼びCPS変換
と、wikiに書いているが、特に黒田の方はわからんmrsekut.icon
http://www.kmonos.net/wlog/61.html#_1826060509
http://www.kmonos.net/wlog/61.html#_0538060508
直観主義論理のCurry-Howard同型対応
https://lemniscus.hatenablog.com/entry/20100209/1265723109
https://lemniscus.hatenablog.com/entry/20100210/1265802932
https://lemniscus.hatenablog.com/entry/20100211/1265888337
https://lemniscus.hatenablog.com/entry/20100214/1266163713
Timothy G. GriffinがA Formulae-as-Types Notion of Control(PDF)という論文で
ラムダ計算にcall/ccを加えることが、
直観主義論理に背理法を加えることに
対応する、と言ったらしい
参考
『論理の哲学』 p.206
CPS変換は、二重否定による古典論理の直観主義論理への埋め込みにあたる。また、古典論理そのものは、Schemeの call-with-current-continuation 制御演算子のように、継続を直に扱うことができるプログラミング言語に対応する ref
https://www.kurims.kyoto-u.ac.jp/~terui/summer2013.pdf
関連
一階述語論理系
Martin-Löfの型理論
依存型算譜言語
https://www.youtube.com/watch?v=uVW6Iwgw6tY
参考
『論理の哲学』 7章
林「数理論理学」
https://www.academia.edu/35826510/カリー_ハワード対応と直観主義論理の意味論入門
pdf本
コレを読み進めていけばいい？
カリー・ハワード同型対応 : tnomuraのブログ
https://xtech.nikkei.com/it/article/COLUMN/20070909/281498/?ST=develop&P=1
いろんな記事で頻繁に引用されている
https://lemniscus.hatenablog.com/entry/20100227/1267256086
https://m-hiyama-memo.hatenablog.jp/entry/20181102/1541152416
https://www.nii.ac.jp/hrd/HTML/OpenHouse/h16/archive/PDF/111.pdf
https://twitter.com/hyuki/status/1035743391655518208
http://return0.dyndns.org/log/2009/03/20#s_2
https://m-hiyama.hatenablog.com/entry/20090321/1237627082
http://www.kmonos.net/wlog/61.html#_0538060508
https://ja.wikipedia.org/wiki/カリー＝ハワード同型対応
https://wiki.haskell.org/Curry-Howard-Lambek_correspondence
https://tarao.hatenablog.com/entry/type-first
http://bitterharvest.hatenablog.com/entry/2017/05/15/153933
https://nowokay.hatenablog.com/entry/20130807/1375879662
https://www.jstage.jst.go.jp/article/jpssj1968/36/2/36_2_103/_pdf/-char/ja
https://youzicha.tumblr.com/post/624180258328002560/generalized-church-is-the-curry-howard-of
https://qiita.com/SekiT/items/855b49ad8b18f332dd5c
https://m-hiyama.hatenablog.com/entry/2021/01/07/131516
https://m-hiyama.hatenablog.com/entry/2021/01/10/185409
https://m-hiyama.hatenablog.com/entry/2021/01/07/131516
記法、図法
https://gist.github.com/kom-bu/2d43bf1f0b940deccfdddb28557ea75c
typescript
Propositions as Types
https://techblog.asahi-net.co.jp/entry/2019/10/31/125852
めっちゃおもろmrsekut.icon
@lotz84_: "Lecture Notes on the Lambda Calculus"
2001, 2007, 2013年に大学で行われた講義を元に作られた120頁に渡るレクチャーノート
内容はラムダ計算、チャーチロッサーの定理、コンビネータ代数、単純型付ラムダ計算、カリーハワード同型対応、弱/強正規化など多岐に渡っている
https://t.co/pZyixk7j48
https://pbs.twimg.com/media/FjIe72DaEAAFXxF.jpg