Ulaşılabilirlik

Gerçeklenebilirlik bir kolu olan matematiksel mantık , özellikle gösteri teorisi bir formülleri arasındaki mantıksal ilişkiyi tanımlar, mantıksal sistem ve programları hesaplama modeli . 40'lı yıllarda Kleene tarafından aritmetik Heyting (en) formüllerinin özyinelemeli fonksiyonların kümeleri (indeksi) tarafından yorumlanması olarak tanıtıldı . O zamandan beri diğer tüm mantıksal sistemlere genişletildi ve bugün Curry-Howard yazışmalarının bir genellemesi olarak görülüyor .

Bir formül ve bir program verildiğinde , " gerçekleştirdiği " özelliği belirtiriz ; Bu notasyonu anımsatır ait Cohen'in zorlayarak hangi gerçeklenebilirlik hediyeler biçimsel Analojilerle. Gerçekleştirilebilirlik, formüllerin program özellikleri olarak yorumlanmasına yol açar: örneğin totoloji , bir tür girdisi verildiğinde, bir tür sonucu oluşturan programlarla elde edilir . $AT$ $p$ ${\ displaystyle p \ Vdash A}$ $p$ $AT$ ${\ displaystyle A \ rightarrow A}$ $AT$ $AT$

Kaynakça

(tr) SC Kleene , " Sezgisel sayı teorisinin yorumlanması üzerine " , Journal of Symbolic Logic ,1945

(tr) Anne Troelstra , "Gerçekleştirilebilirlik" , SR Buss, Handbook of proof teorisi , Kuzey Hollanda,1998( çevrimiçi okuyun )

(en) Jaap van Oosten , " Gerçekleştirilebilirlik: tarihsel bir deneme " , Bilgisayar Bilimlerinde Matematiksel Yapılar ,2002( çevrimiçi okuyun )