Apa persamaan paling menarik yang muncul dari Curry-Howard Isomorphism?

Saya menemukan Curry-Howard Isomorphism relatif terlambat dalam kehidupan pemrograman saya, dan mungkin ini berkontribusi pada saya yang benar-benar terpesona olehnya. Ini menyiratkan bahwa untuk setiap konsep pemrograman terdapat analog yang tepat dalam logika formal, dan sebaliknya. Berikut adalah daftar "dasar" dari analogi semacam itu, di luar kepala saya:

program/definition        | proof
type/declaration          | proposition
inhabited type            | theorem/lemma
function                  | implication
function argument         | hypothesis/antecedent
function result           | conclusion/consequent
function application      | modus ponens
recursion                 | induction
identity function         | tautology
non-terminating function  | absurdity/contradiction
tuple                     | conjunction (and)
disjoint union            | disjunction (or)          -- corrected by Antal S-Z
parametric polymorphism   | universal quantification

Jadi, untuk pertanyaan saya: apa saja implikasi yang lebih menarik / tidak jelas dari isomorfisme ini? Saya bukan ahli logika jadi saya yakin saya hanya menggores permukaannya dengan daftar ini.

Sebagai contoh, berikut adalah beberapa pengertian pemrograman yang saya tidak tahu nama-nama bernas dalam logikanya:

currying                  | "((a & b) => c) iff (a => (b => c))"
scope                     | "known theory + hypotheses"

Dan berikut adalah beberapa konsep logis yang belum saya jelaskan dalam istilah pemrograman:

primitive type?           | axiom
set of valid programs?    | theory

Edit:

Berikut adalah beberapa persamaan lagi yang dikumpulkan dari tanggapan:

function composition      | syllogism                -- from Apocalisp
continuation-passing      | double negation          -- from camccann

Karena Anda secara eksplisit meminta yang paling menarik dan tidak jelas:

Anda dapat memperluas CH ke banyak logika dan formulasi logika yang menarik untuk mendapatkan variasi korespondensi yang sangat luas. Di sini saya mencoba untuk fokus pada beberapa yang lebih menarik daripada yang tidak jelas, ditambah beberapa yang mendasar yang belum muncul.

evaluation             | proof normalisation/cut-elimination
variable               | assumption
S K combinators        | axiomatic formulation of logic   
pattern matching       | left-sequent rules 
subtyping              | implicit entailment (not reflected in expressions)
intersection types     | implicit conjunction
union types            | implicit disjunction
open code              | temporal next
closed code            | necessity
effects                | possibility
reachable state        | possible world
monadic metalanguage   | lax logic
non-termination        | truth in an unobservable possible world
distributed programs   | modal logic S5/Hybrid logic
meta variables         | modal assumptions
explicit substitutions | contextual modal necessity
pi-calculus            | linear logic

EDIT: Referensi yang saya rekomendasikan kepada siapa pun yang tertarik untuk mempelajari lebih lanjut tentang ekstensi CH:

"Rekonstruksi Penghakiman dari Modal Logika" http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - ini adalah tempat yang bagus untuk memulai karena dimulai dari prinsip pertama dan sebagian besar ditujukan untuk dapat diakses oleh ahli teori non-logika / bahasa. (Saya penulis kedua, jadi saya bias.)

Anda sedikit mengotori hal-hal tentang nonterminasi. Kepalsuan diwakili oleh jenis yang tidak berpenghuni , yang menurut definisi tidak dapat bersifat non-terminating karena tidak ada jenis yang perlu dievaluasi sejak awal.

Non-termination merepresentasikan kontradiksi - sebuah logika yang tidak konsisten. Logika yang tidak konsisten tentu saja memungkinkan Anda membuktikan apa pun , termasuk kepalsuan.

Mengabaikan ketidakkonsistenan, sistem tipe biasanya sesuai dengan logika intuitionistik , dan oleh konstruktivis kebutuhan , yang berarti potongan tertentu dari logika klasik tidak dapat diekspresikan secara langsung, jika sama sekali. Di sisi lain, ini berguna, karena jika suatu tipe adalah bukti konstruktif yang valid, maka istilah jenis itu adalah sarana untuk membangun apa pun yang telah Anda buktikan keberadaannya .

Ciri utama dari rasa konstruktivis adalah bahwa negasi ganda tidak setara dengan non-negasi. Faktanya, negasi jarang menjadi primitif dalam sistem tipe, jadi sebaliknya kita dapat merepresentasikannya sebagai kepalsuan yang menyiratkan, misalnya not Pmenjadi P -> Falsity. Negasi ganda dengan demikian akan menjadi fungsi dengan tipe (P -> Falsity) -> Falsity, yang jelas tidak setara dengan sesuatu yang hanya tipe P.

Namun, ada twist menarik tentang ini! Dalam bahasa dengan polimorfisme parametrik, variabel jenis berkisar pada semua jenis yang mungkin, termasuk yang tidak berpenghuni, jadi jenis polimorfik sepenuhnya seperti ∀a. a, dalam arti tertentu, hampir salah. Jadi bagaimana jika kita menulis hampir negasi ganda dengan menggunakan polimorfisme? Kami mendapatkan jenis yang terlihat seperti ini: ∀a. (P -> a) -> a. Apakah itu setara dengan sesuatu yang sejenis P? Memang benar , hanya menerapkannya pada fungsi identitas.

Tapi apa gunanya? Mengapa menulis tipe seperti itu? Apakah itu ada artinya dalam istilah pemrograman? Nah, Anda bisa menganggapnya sebagai fungsi yang sudah memiliki tipe di Psuatu tempat, dan Anda perlu memberikan fungsi yang mengambil Pargumen, dengan semuanya menjadi polimorfik di tipe hasil akhir. Dalam arti tertentu, ini mewakili perhitungan yang ditangguhkan , menunggu sisanya disediakan. Dalam pengertian ini, perhitungan yang ditangguhkan ini dapat disusun bersama, diedarkan, dipanggil, apa pun. Ini seharusnya mulai terdengar familier bagi penggemar beberapa bahasa, seperti Scheme atau Ruby - karena artinya negasi ganda sesuai dengan gaya penerusan lanjutan, dan sebenarnya tipe yang saya berikan di atas persis seperti monad lanjutan di Haskell.

Bagan Anda kurang tepat; dalam banyak kasus Anda bingung jenis dengan istilah.

function type              implication
function                   proof of implication
function argument          proof of hypothesis
function result            proof of conclusion
function application RULE  modus ponens
recursion                  n/a [1]
structural induction       fold (foldr for lists)
mathematical induction     fold for naturals (data N = Z | S N)
identity function          proof of A -> A, for all A
non-terminating function   n/a [2]
tuple                      normal proof of conjunction
sum                        disjunction
n/a [3]                    first-order universal quantification
parametric polymorphism    second-order universal quantification
currying                   (A,B) -> C -||- A -> (B -> C), for all A,B,C
primitive type             axiom
types of typeable terms    theory
function composition       syllogism
substitution               cut rule
value                      normal proof

[1] Logika untuk bahasa fungsional lengkap Turing tidak konsisten. Rekursi tidak memiliki korespondensi dalam teori yang konsisten. Dalam logika yang tidak konsisten / teori bukti yang tidak benar, Anda dapat menyebutnya sebagai aturan yang menyebabkan ketidakkonsistenan / ketidakseimbangan.

[2] Sekali lagi, ini adalah konsekuensi dari kelengkapan. Ini akan menjadi bukti anti-teorema jika logikanya konsisten - jadi, tidak mungkin ada.

[3] Tidak ada dalam bahasa fungsional, karena mereka elide fitur logis urutan pertama: semua kuantifikasi dan parametrization dilakukan di atas rumus. Jika Anda memiliki fitur orde pertama, akan ada lain jenis dari *, * -> *, dll .; jenis elemen dari domain wacana. Misalnya, dalam Father(X,Y) :- Parent(X,Y), Male(X), Xdan Yjangkauan di atas domain wacana (sebut saja Dom), dan Male :: Dom -> *.

function composition      | syllogism

Saya sangat suka pertanyaan ini. Saya tidak tahu banyak, tapi saya punya beberapa hal (dibantu oleh artikel Wikipedia , yang memiliki beberapa tabel rapi dan semacamnya):

1. Saya berpikir bahwa jenis penjumlahan / jenis gabungan ( misalnya data Either a b = Left a | Right b ) setara dengan disjungsi inklusif . Dan, meskipun saya tidak terlalu mengenal Curry-Howard, saya pikir ini menunjukkannya. Pertimbangkan fungsi berikut:

   andImpliesOr :: (a,b) -> Either a b
   andImpliesOr (a,_) = Left a
   

   Jika saya memahami sesuatu dengan benar, tipe mengatakan bahwa ( a  ∧  b ) → ( a  ★  b ) dan definisi mengatakan bahwa ini benar, di mana ★ bersifat inklusif atau eksklusif atau, mana saja yang Eithermewakili. Anda telah Eithermewakili eksklusif atau, ⊕; Namun, ( a  ∧  b ) ↛ ( a  ⊕  b ). Misalnya, ⊤ ∧ ⊤ ≡ ⊤, tapi ⊤ ⊕ ⊥ ≡ ⊥, dan ⊤ ↛ ⊥. Dengan kata lain, jika a dan b benar, maka hipotesisnya benar tetapi kesimpulannya salah, sehingga implikasi ini pasti salah. Namun, jelas, ( a  ∧  b ) → ( a  ∨ b ), karena jika a dan b benar, maka setidaknya satu benar. Jadi, jika serikat pekerja yang terdiskriminasi adalah suatu bentuk pemisahan, mereka haruslah keragaman yang inklusif. Saya pikir ini berlaku sebagai bukti, tetapi merasa lebih dari bebas untuk melecehkan saya tentang gagasan ini.

2. Demikian pula, definisi Anda untuk tautologi dan absurditas sebagai fungsi identitas dan fungsi non-terminating, masing-masing sedikit salah. Rumus sebenarnya diwakili oleh tipe unit , yaitu tipe yang hanya memiliki satu elemen ( data ⊤ = ⊤; sering dieja ()dan / atau Unitdalam bahasa pemrograman fungsional). Ini masuk akal: karena tipe itu dijamin akan dihuni, dan karena hanya ada satu kemungkinan penghuninya, itu pasti benar. Fungsi identitas hanya mewakili tautologi tertentu yang a  →  a .

   Komentar Anda tentang fungsi non-terminating, tergantung pada apa yang Anda maksudkan, lebih tidak tepat. Fungsi Curry-Howard pada sistem tipe, tetapi non-terminasi tidak dikodekan di sana. Menurut Wikipedia , berurusan dengan non-termination adalah sebuah masalah, karena menambahkannya menghasilkan logika yang tidak konsisten ( misalnya , saya dapat mendefinisikan wrong :: a -> bdengan wrong x = wrong x, dan dengan demikian “membuktikan” bahwa a  →  b untuk a dan b ). Jika ini yang Anda maksud dengan "absurditas", maka Anda benar. Jika sebaliknya yang Anda maksud pernyataan palsu, maka yang Anda inginkan adalah tipe yang tidak berpenghuni, misalnya sesuatu yang didefinisikan olehdata ⊥—Yaitu, tipe data tanpa cara untuk membangunnya. Ini memastikan bahwa itu tidak memiliki nilai sama sekali, dan karenanya harus tidak berpenghuni, yang setara dengan false. Saya pikir Anda mungkin juga bisa menggunakan a -> b, karena jika kami melarang fungsi non-terminating, maka ini juga tidak berpenghuni, tapi saya tidak 100% yakin.

3. Wikipedia mengatakan bahwa aksioma dikodekan dalam dua cara berbeda, bergantung pada bagaimana Anda menafsirkan Curry-Howard: baik dalam kombinator atau variabel. Saya pikir tampilan kombinator berarti bahwa fungsi primitif yang kita berikan menyandikan hal-hal yang dapat kita katakan secara default (mirip dengan cara modus ponens adalah aksioma karena aplikasi fungsi primitif). Dan menurut saya tampilan variabel sebenarnya memiliki arti yang sama — bagaimanapun juga, kombinator hanyalah variabel global yang merupakan fungsi tertentu. Adapun tipe primitif: jika saya memikirkan hal ini dengan benar, maka saya pikir tipe primitif adalah entitas — objek primitif yang kami coba buktikan.

4. Menurut kelas logika dan semantik saya, fakta bahwa ( a  ∧  b ) →  c  ≡  a  → ( b  →  c ) (dan juga bahwa b  → ( a  →  c )) disebut hukum ekivalensi ekspor, setidaknya dalam deduksi natural bukti. Saya tidak memperhatikan pada saat itu bahwa itu hanya kari — saya harap saya punya, karena itu keren!

5. Meskipun sekarang kami memiliki cara untuk merepresentasikan disjungsi inklusif , kami tidak memiliki cara untuk merepresentasikan variasi eksklusif. Kita harus bisa menggunakan definisi disjungsi eksklusif untuk merepresentasikannya: a  ⊕  b  ≡ ( a  ∨  b ) ∧ ¬ ( a  ∧  b ). Saya tidak tahu bagaimana menulis negasi, tapi saya tahu bahwa ¬ p  ≡  p  → ⊥, dan baik implikasi maupun kepalsuan itu mudah. Dengan demikian, kita harus dapat merepresentasikan disjungsi eksklusif dengan:

   data ⊥
   data Xor a b = Xor (Either a b) ((a,b) -> ⊥)
   

   Ini didefinisikan ⊥sebagai tipe kosong tanpa nilai, yang sesuai dengan kepalsuan; Xorkemudian didefinisikan mengandung ( dan ) Eithersebuah a atau b ( atau ) dan fungsi ( implikasi ) dari (a, b) ( dan ) dengan jenis bawah ( palsu ). Namun, saya tidak tahu apa artinya ini . ( Sunting 1: Sekarang saya lakukan, lihat paragraf berikutnya!) Karena tidak ada nilai tipe (a,b) -> ⊥(apakah ada?), Saya tidak dapat memahami apa artinya ini dalam program. Adakah yang tahu cara yang lebih baik untuk memikirkan definisi ini atau yang lain? ( Edit 1: Ya, camccann .)

   Sunting 1: Terima kasih untuk jawaban camccann (lebih khusus lagi, komentar yang dia tinggalkan untuk membantu saya), saya rasa saya mengerti apa yang terjadi di sini. Untuk membuat nilai tipe Xor a b, Anda perlu menyediakan dua hal. Pertama, saksi keberadaan salah satu elemen aatau bsebagai argumen pertama; yaitu, a Left aatau a Right b. Dan kedua, bukti bahwa tidak ada unsur dari kedua jenis tersebut adan b— dengan kata lain, bukti yang (a,b)tidak berpenghuni — sebagai argumen kedua. Karena Anda hanya akan dapat menulis fungsi dari (a,b) -> ⊥jika (a,b)tidak berpenghuni, apa artinya itu terjadi? Itu berarti bahwa beberapa bagian dari suatu objek bertipe(a,b)tidak bisa dibangun; dengan kata lain, bahwa setidaknya satu, dan mungkin keduanya, dari adan bjuga tidak berpenghuni! Dalam hal ini, jika kita berpikir tentang pencocokan pola, Anda tidak mungkin mencocokkan pola pada tupel seperti itu: seandainya itu btidak berpenghuni, apa yang akan kita tulis yang bisa cocok dengan bagian kedua dari tupel itu? Jadi, kami tidak dapat mencocokkan pola dengannya, yang dapat membantu Anda melihat mengapa hal ini membuatnya tidak berpenghuni. Sekarang, satu-satunya cara untuk memiliki fungsi total yang tidak membutuhkan argumen (seperti yang harus dilakukan, karena (a,b)tidak berpenghuni) adalah untuk hasilnya menjadi tipe yang tidak berpenghuni juga — jika kita memikirkan hal ini dari perspektif pencocokan pola, Artinya, meskipun fungsinya tidak memiliki case, tidak ada body yang memungkinkan bisa juga, jadi semuanya baik-baik saja.

Banyak dari ini adalah saya berpikir keras / membuktikan (mudah-mudahan) banyak hal dengan cepat, tetapi saya harap ini berguna. Saya sangat merekomendasikan artikel Wikipedia ; Saya belum membacanya dengan detail apa pun, tetapi tabelnya adalah ringkasan yang sangat bagus, dan sangat menyeluruh.

Berikut adalah salah satu yang agak kabur yang saya terkejut tidak dibicarakan sebelumnya: Pemrograman reaktif fungsional "klasik" sesuai dengan logika temporal.

Tentu saja, kecuali Anda seorang filsuf, matematikawan, atau programmer fungsional obsesif, ini mungkin menimbulkan beberapa pertanyaan lagi.

Jadi, pertama: apa itu pemrograman reaktif fungsional? Ini adalah cara deklaratif untuk bekerja dengan nilai yang berubah-ubah waktu . Ini berguna untuk menulis hal-hal seperti antarmuka pengguna karena masukan dari pengguna adalah nilai yang bervariasi dari waktu ke waktu. FRP "Klasik" memiliki dua tipe data dasar: peristiwa dan perilaku.

Peristiwa mewakili nilai yang hanya ada pada waktu yang berbeda. Penekanan tombol adalah contoh yang bagus: Anda dapat menganggap masukan dari keyboard sebagai karakter pada waktu tertentu. Setiap tombol ditekan hanya berupa pasangan dengan karakter tombol dan waktu penekanannya.

Perilaku adalah nilai-nilai yang ada secara konstan tetapi dapat berubah terus menerus. Posisi mouse adalah contoh yang bagus: ini hanyalah perilaku koordinat x, y. Bagaimanapun, mouse selalu memiliki posisi dan, secara konseptual, posisi ini terus berubah saat Anda menggerakkan mouse. Lagi pula, menggerakkan mouse adalah satu tindakan berlarut-larut, bukan serangkaian langkah terpisah.

Dan apakah logika temporal? Cukup tepat, ini adalah seperangkat aturan logis untuk menangani proposisi yang dikuantifikasi dari waktu ke waktu. Pada dasarnya, ini memperluas logika orde pertama normal dengan dua bilangan: □ dan ◇. Yang pertama berarti "selalu": ​​baca □ φ sebagai "φ selalu memegang". Yang kedua adalah "akhirnya": ◇ φ berarti "φ pada akhirnya akan bertahan". Ini adalah jenis logika modal tertentu . Dua hukum berikut berhubungan dengan bilangan:

□φ ⇔ ¬◇¬φ
◇φ ⇔ ¬□¬φ

Jadi □ dan ◇ adalah ganda satu sama lain dengan cara yang sama seperti ∀ dan ∃.

Kedua bilangan ini sesuai dengan dua jenis di FRP. Secara khusus, □ berhubungan dengan perilaku dan ◇ berhubungan dengan kejadian. Jika kita berpikir tentang bagaimana jenis ini dihuni, ini seharusnya masuk akal: suatu perilaku dihuni setiap saat, sementara suatu peristiwa hanya terjadi satu kali.

Terkait hubungan antara kelanjutan dan negasi ganda, jenis panggilan / cc adalah hukum Peirce http://en.wikipedia.org/wiki/Call-with-current-continuation

CH biasanya dinyatakan sebagai korespondensi antara logika intuitionistic dan program. Namun jika kita menambahkan operator call-with-current-continuation (callCC) (yang tipenya sesuai dengan hukum Peirce), kita mendapatkan korespondensi antara logika klasik dan program dengan callCC.

Meskipun ini bukan isomorfisme sederhana, pembahasan LEM konstruktif ini adalah hasil yang sangat menarik. Secara khusus, di bagian kesimpulan, Oleg Kledgeov membahas bagaimana penggunaan monad untuk mendapatkan eliminasi negasi ganda dalam logika konstruktif adalah analog dengan membedakan proposisi yang dapat ditentukan secara komputasi (yang LEM valid dalam pengaturan konstruktif) dari semua proposisi. Gagasan bahwa monad menangkap efek komputasi adalah gagasan lama, tetapi contoh isomorfisme Curry - Howard ini membantu meletakkannya dalam perspektif dan membantu memahami apa yang sebenarnya "berarti" negasi ganda.

Dukungan lanjutan kelas satu memungkinkan Anda mengekspresikan $ P \ lor \ neg P $. Trik ini didasarkan pada fakta bahwa tidak memanggil lanjutan dan keluar dengan beberapa ekspresi sama dengan memanggil lanjutan dengan ekspresi yang sama.

Untuk tampilan lebih detail silakan lihat: http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf

2-continuation           | Sheffer stoke
n-continuation language  | Existential graph
Recursion                | Mathematical Induction

Satu hal yang penting, tetapi belum diteliti adalah hubungan 2-lanjutan (kelanjutan yang membutuhkan 2 parameter) dan stroke Sheffer . Dalam logika klasik, goresan Sheffer dapat membentuk sistem logika lengkap dengan sendirinya (ditambah beberapa konsep non-operator). Yang berarti akrab and, or, notdapat diimplementasikan hanya menggunakan stoke Sheffer atau nand.

Ini adalah fakta penting dari korespondensi jenis pemogramannya karena meminta agar satu jenis kombinator dapat digunakan untuk membentuk semua jenis lainnya.

Jenis tanda tangan dari 2-lanjutan adalah (a,b) -> Void. Dengan implementasi ini kita dapat mendefinisikan 1-continuation (kelanjutan normal) sebagai (a,a)-> Void, product type as ((a,b)->Void,(a,b)->Void)->Void, sum type as ((a,a)->Void,(b,b)->Void)->Void. Ini memberi kita kekuatan ekspresif yang mengesankan.

Jika kita menggali lebih jauh, kita akan menemukan bahwa grafik eksistensial Piece setara dengan bahasa dengan satu-satunya tipe datanya adalah n-lanjutan, tetapi saya tidak melihat ada bahasa yang ada dalam formulir ini. Jadi, menurut saya, menemukan seseorang bisa menarik.