Oppnåelighet

Den realiserbarheten er en gren av matematisk logikk , nærmere bestemt teori for demonstrasjonen , som definerer en logisk sammenheng mellom oppskriftene ifølge et logisk system og programmer til en beregningsmodell . Den ble introdusert på 40-tallet av Kleene som en tolkning av formlene til aritmetikken Heyting  (en) ved sett (indeks) av rekursive funksjoner . Den har siden blitt utvidet til alle slags andre logiske systemer, og i dag blir sett på som en generalisering av Curry-Howard-korrespondansen .

Gitt en formel og et program, betegner vi eiendommen "  realiserer  "; denne notasjonen minner om Cohens tvang som realiserbarhet gir formelle analogier. Realiserbarhet fører til en tolkning av formler som programspesifikasjoner: for eksempel oppnås tautologi av programmer som, gitt en type input, gir et typeresultat . PÅ{\ displaystyle A}s{\ displaystyle p}s⊩PÅ{\ displaystyle p \ Vdash A}s{\ displaystyle p}PÅ{\ displaystyle A}PÅ→PÅ{\ displaystyle A \ rightarrow A}PÅ{\ displaystyle A}PÅ{\ displaystyle A}

Bibliografi

• (en) SC Kleene , “  On the interpretation of intuitionistic number theory  ” , Journal of Symbolic Logic ,1945

• (en) Anne Troelstra , “realiserbarheten” , i SR Buss, Handbook of proof teori , Nord-Holland,1998( les online )

• (en) Jaap van Oosten , “  Realizability: an historical essay  ” , Matematical Structures in Computer Science ,2002( les online )

<img src="https://fr.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">