Apakah kombinator Y bertentangan dengan korespondensi Curry-Howard?

Combinator Y memiliki tipe . Oleh Korespondensi Curry-Howard, karena jenis ( a → a ) → a dihuni, maka harus sesuai dengan teorema yang benar. Namun a → a selalu benar, jadi sepertinya tipe kombinator Y sesuai dengan teorema a , yang tidak selalu benar. Bagaimana ini bisa terjadi?$(a \rightarrow a) \rightarrow a$$(a \rightarrow a) \rightarrow a$$a \rightarrow a$$a$

Korespondensi Curry-Howard yang asli adalah isomorfisme antara logika proposisional intuitionistic dan kalkulus lambda yang diketik sederhana.

Tentu saja ada isomorfisme mirip Curry-Howard; Phil Wadler dengan terkenal menunjukkan bahwa nama laras ganda "Curry-Howard" memprediksi nama laras ganda lainnya seperti "Hindley-Milner" dan "Girard-Reynolds". Akan lucu jika "Martin-Löf" adalah salah satunya, tetapi ternyata tidak. Tapi saya ngelantur.

Penggabung Y tidak bertentangan dengan ini, karena satu alasan utama: itu tidak dapat diungkapkan dalam kalkulus lambda yang diketik sederhana.

Sebenarnya, itulah intinya. Haskell Curry menemukan kombinator fixpoint dalam kalkulus lambda yang tidak diketik, dan menggunakannya untuk membuktikan bahwa kalkulus lambda yang tidak diketik bukanlah sistem pengurangan suara.

Menariknya, tipe Y sesuai dengan paradoks logis yang tidak seterkenal yang seharusnya, disebut paradoks Curry. Pertimbangkan kalimat ini:

Jika kalimat ini benar, maka Santa Claus ada.

Misalkan kalimat itu benar. Maka, jelas, Santa Claus akan ada. Tapi inilah tepatnya yang dikatakan kalimat itu, jadi kalimat itu benar. Karena itu, Santa Claus ada. QED

Curry-Howard mengaitkan sistem tipe dengan sistem deduksi logis. Antara lain, memetakan:

• program untuk pembuktian
• evaluasi program untuk transformasi pada bukti
• jenis dihuni untuk proposisi yang benar
• ketik sistem ke sistem deduksi logis

$a \to b$$a$$b$$Y (\lambda x. x) \to Y (\lambda x.M)$ . Aturan pemotongan yang sesuai memungkinkan proposisi apa pun diperoleh dari proposisi lainnya. Dengan demikian sistem logisnya tidak konsisten.

Korespondensi Curry-Howard hanya itu: korespondensi. Dalam dirinya sendiri, itu tidak mengatakan bahwa teorema tertentu itu benar. Dikatakan bahwa tipabilitas / provabilitas membawa dari satu sisi ke sisi lain.

Korespondensi Curry-Howard berguna sebagai alat bukti dengan banyak jenis sistem: cukup ketik lambda kalkulus, sistem F, kalkulus konstruksi, dll. Semua sistem jenis ini memiliki properti yang sesuai dengan logika konsisten (jika matematika biasanya konsisten ). Mereka juga memiliki sifat tidak mengizinkan rekursi sewenang-wenang. Korespondensi Curry-Howard menunjukkan bahwa kedua sifat ini terkait.

Curry-Howard masih berlaku untuk kalkulus yang diketik dan sistem deduksi yang tidak konsisten. Hanya saja tidak terlalu berguna di sana.