Elérhetőség

A megvalósíthatóság a matematikai logika egyik ága , konkrétan a demonstráció elmélete , amely logikai kapcsolatot határoz meg egy logikai rendszer képletei és egy számítási modell programjai között . A 40-es években Kleene vezette be a számtani Heyting (en) képleteinek a rekurzív függvények halmazaival (indexe) való interpretációjaként . Azóta minden más logikai rendszerre kiterjesztették, és ma a Curry-Howard-megfelelés általánosításának tekintik .

Ha képletet és programot adunk , akkor a tulajdonságot " megvalósítja " jelöljük ; Ezzel a jelöléssel emlékeztet a Cohen kényszerítve , amellyel megvalósíthatóság ajándékokat formai hasonlóságok. A megvalósíthatóság a képletek programspecifikációként való értelmezéséhez vezet: például a tautológiát olyan programok érik el, amelyek egy típusbevitel alapján típusú eredményt adnak . $NÁL NÉL$ $o$ ${\ displaystyle p \ Vdash A}$ $o$ $NÁL NÉL$ ${\ displaystyle A \ jobbra nyíl A}$ $NÁL NÉL$ $NÁL NÉL$

Bibliográfia

(en) SC Kleene , „ Az intuitionisztikus számelmélet értelmezéséről ” , Journal of Symbolic Logic ,1945

en) Anne Troelstra , „Megvalósíthatóság” , SR Buss, Handbook of proof theory , North Holland,1998( online olvasás )

(en) Jaap van Oosten , „ Megvalósíthatóság: történelmi esszé ” , Matematikai struktúrák a számítástechnikában ,2002( online olvasás )