Curry - Howard - Lambek -De Bruijn iliskisi kisaca sunu demektedir: Her sezgisel mantikta her ispatlanabilir onermeye karsilik, tipli-lambda kalkulde (simply typed lambda calculus) bir tip vardir (sanirim Lambek bunun kartezyen kapali kategorilerle bir baglantisini kuruyor ama emin degilim )
asagida bazi ornekler verdim
| Manitksal ifade |
Programlama karsiligi |
Aciklama |
| $A \land B$ |
$A \times B$ carpma tipi |
$A \land B$ yi ispatlamak icin bir tane $A$ tipinde obje ve bir tane de $B$ tipinde obje gosterebilmeliyim. Fonksyonel dilllerde iki tipi yada ifadeyi carpma tipi ile birbirini baglayabilirsiniz. sag ve sol projeksyonlarla orjinal objeleri geri kazanabilirsiniz |
| $A \lor B$ |
$A + B$ toplama tipi |
$A \lor B$ yi ispatlamak icin bir tane $A$ tipinde obje veya bir tane de $B$ tipinde obje gosterebilmeliyim. Bunu Programlama dillerinde toplama tipleri ile yapiyoruz. C biliyorsaniz tagged union lari dusunebilirsiniz.
|
| $A \rightarrow B$ |
$A\rightarrow B$ tipinde total bir fonksiyon |
$A\rightarrow B$ yi ispatlamak icin, Her $A$ tipindeki objeyi $B$ tipindeki objeye donusturen bir sey lazim. Fonksiyon tipleri! |
| $\neg A$ |
$A \rightarrow \epsilon$ $epsilon$ burada bos tipi ifade ediyor |
Programiniz coktu , yada sonsuz donguye girdi ve bir sey uretmiyor :( |
| |
| $\forall _{ a \in A} X(a)$ |
$\prod_{a:A}X(a)$ tipinde bir fonksiyon |
bagimli tipler ile alakali (dependent types) |
| $\exists _ { a \in A} : X(a)$ |
$\sum_{a:A}X(a)$ tipinde bir fonskiyon |
bagimli tipler ile alakali (dependent types) |
Evet ispat denetleyecileri/arayacilari/asistanlari bu iliski sayesinde varolabiliyorlar. Bir iki tane ispat asistani ornek vermek gerekirse: Agda Coq Lean Idris Mizar Isabelle
Bildigim kadari ile Lean kullanilarak Ingilterede bir universitede undergrad calculusun cogunu formalize ettiler ve kontrol ettiler. Internette aradim ama bulamadim fakat Project Xena adinda bir proje buldum. Ogrenmek icin ilginc olabilir.
Bundan sonrasi tarih (ne kadar dogru ne kadar yanlis bilemiyorum referans vermeden hatirladiklarimi yazacagim isimler mekanlar ve olarlar karisik olabilir):
Hilbert matematigi otomatize etmek istiyor ve tutarliligini gostermek istiyor bir de mumkunse matematikcileri isinden etmek istiyor. Tabii ogrencilerine bunu odev olarak veriyor. Ogrencilerinden biri, Gentzen (ogrencisi olmayabilir ama o siralarda Gottingende [azicik dedikodu olacak ama nazi maalesef Gentzen]) bir tumdengelim semasi buluyor. Bu daha sonra onemli olacak. Bir digeri ise amerikali Haskell Curry. Curry kombinatorik mantik uzerine calisiyor.
Godel Hilbertin girisiminin mumkun olmadigini gosteriyor. Eger matematigi otomatize edecek kadar guclu bir dilimiz varsa o dilin paradoksal ifadelere yolacagini soyluyor.
Bu sirada Ingilterede hesaplamayi modellemek icin buyuk bir ugras var. Babbage ve Lord Byron in kizi Ada lovelace bir yuzyil oncesinde mekanik bilgisayarlar tasarlamislar oradan gelen bir gelenektir belki de. Alanso Church, lambda kalkulu gelistiriyor icin.,ogrencisi Alan Turing ise Turing makinalarini gelistiriyor hesaplamayi matematiksel olarak modellemek icin. Godelin ispatina analog bir ispat geliyor Alan Turingden. (futbol maci anlatiyor gibi hissettim).
Turing verilen bir turing makinasinin durup durmayacagini soylemenin imkansiz oldugunu soyluyor. Bu arada gosteriyor ki lambda kalkul ve turing makinalari denk. [lambda kalkul daha bir programlama diline benziyor, turing makinalari ise gercekten makina gibi bilgisayara yakinlar].
Godel her ne kadar Churchin ve Turingin modelini begenmese de, Church yontemlerin denk oldugunu gosteriyor (en azindan Godelin incompleteness theoreminden daha zayif bir ifadeyi turing makinalarinin durmayacagini gostererek gosterebiliyoruz ).
Alanso Church lambda kalkulde yazilan bir ifadenin durup durmayacagini bilememekten cok rahatsiz. Bu yuzden tipli-lambda kalkunu gelistiriyor. Bu dil turing complete degil. Yani durup durmayacagini soyleyebiliyoruz.
Bu sirada Curry farkediyor ki, kombinatorlerin tipleri sezgisel mantiktaki aksyom semalarina benziyor. Daha sonra farkediyor ki Hilbertin gelistirdigi ispat semalari kendi gelistirdigi kombinatorik mantigin hesaplama modelinin bazi kisimlari ile ortusuyor.
Butun bunlardan sonra Howard farkediyor ki Gentzenin tumdengelim semasi ile tipli-lambda-kalkulun hesaplama modeli ortusuyor. Bu sirada De-Bruijn Automath adi verdigi dilde mantiksel onermeleri tipli lambda kalkulde gosteriyor.
Atladigim ama bahsetmeye deger diger isimler,Kleene, Per Martin-Löf , Vovodsky.