Saavutettavuus

Realisoitavuuteen on haara matemaattista logiikkaa , erityisesti teoria esittelyn , joka määrittelee looginen suhde kaavat on looginen järjestelmän ja ohjelmista laskentamallia . Kleene esitteli sen 40-luvulla aritmeettisen Heyting (en) -kaavojen tulkinnalla rekursiivisten funktioiden sarjoilla (indeksi) . Sitä on sittemmin laajennettu kaikkiin muihin loogisiin järjestelmiin, ja nykyään sitä pidetään Curry-Howard-kirjeenvaihdon yleistymisenä .

Annettu kaava ja ohjelma merkitsemme ominaisuutta " ymmärtää "; Tämä merkintätapa tuo mieleen sekä Cohenin pakottaa jolla realisoitavuutta esittelee virallisen analogioita. Toteutettavuus johtaa kaavojen tulkintaan ohjelmamäärityksinä: esimerkiksi tautologia saavutetaan ohjelmilla, jotka antavat tyyppituloksen antamalla tyypin tuloksen . $AT$ $s$ ${\ displaystyle p \ Vdash A}$ $s$ $AT$ ${\ displaystyle A \ oikeanpuoleinen nuoli A}$ $AT$ $AT$

Bibliografia

(en) SC Kleene , ” Intuitionistisen lukuteorian tulkinnasta ” , Journal of Symbolic Logic ,1945

(en) Anne Troelstra , ”Realisoitavuus” , SR Buss, Handbook of proof theory , Pohjois-Hollanti,1998( lue verkossa )

(en) Jaap van Oosten , ” Realisoitavuus: historiallinen essee ” , Matematiikkarakenteet tietojenkäsittelytieteessä ,2002( lue verkossa )