Osiągalność

Realność jest gałęzią logiki matematycznej , a konkretnie teoria demonstracji , która definiuje logiczny związek między wzorami o systemie logicznym i programów o modelu obliczeniowego . Został wprowadzony w latach czterdziestych przez Kleene jako interpretację formuł arytmetycznych Heyting (en) przez zbiory (indeks) funkcji rekurencyjnych . Od tego czasu została rozszerzona na wszelkiego rodzaju inne systemy logiczne, a dziś jest postrzegana jako uogólnienie korespondencji Curry-Howard .

Na podstawie wzoru i programu oznaczamy nieruchomość „ realizuje ”; Zapis ten przypomina o Cohena zmuszając z których realizowalności prezenty analogii formalnych. Realizowalność prowadzi do interpretacji formuł jako specyfikacji programu: na przykład tautologia jest osiągana przez programy, które przy danych wejściowych typu dają wynik typu . $W$ $p$ ${\ displaystyle p \ Vdash A}$ $p$ $W$ ${\ displaystyle A \ rightarrow A}$ $W$ $W$

Bibliografia

(en) SC Kleene , „ O interpretacji intuicjonistycznej teorii liczb ” , Journal of Symbolic Logic ,1945

(en) Anne Troelstra , »Realizability« , w: SR Buss, Podręcznik teorii dowodu , Holandia Północna,1998( czytaj online )

(en) Jaap van Oosten , „ Realizability: an history essay ” , Mathematical Structures in Computer Science ,2002( czytaj online )