Réalisabilité

La réalisabilité est une branche de la logique mathématique, et plus précisément de la théorie de la démonstration, qui définit une relation logique entre les formules d'un système logique et les programmes d'un modèle de calcul. Elle a été introduite dans les années 40 par Kleene comme une interprétation des formules de l'arithmétique de Heyting par des ensembles (d'indices) de fonctions récursives. Elle a depuis été étendue à toute sorte d'autres systèmes logiques, et aujourd'hui est vue comme une généralisation de la correspondance de Curry-Howard.

Étant donnés une formule $A$ et un programme $p$ on note $p\Vdash A$ la propriété « $p$ réalise $A$ » ; cette notation est réminiscente du forcing de Cohen avec lequel la réalisabilité présente des analogies formelles. La réalisabilité conduit à une interprétation des formules comme des spécifications de programme : par exemple la tautologie $A\rightarrow A$ est réalisée par les programmes qui étant donné une entrée de type $A$ rendent un résultat de type $A$.

Bibliographie

• (en) S. C. Kleene, « On the interpretation of intuitionistic number theory », Journal of Symbolic Logic,‎ 1945
• (en) Anne Troelstra, « Realizability », dans S. R. Buss, Handbook of proof theory, North Holland, 1998 (lire en ligne)
• (en) Jaap van Oosten, « Realizability: an historical essay », Mathematical Structures in Computer Science,‎ 2002 (lire en ligne)