Réalisabilité
- 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 (en) 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 
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 
est réalisée par les programmes qui étant donnée 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 », dans 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 », dans Mathematical Structures in Computer Science, 2002 [texte intégral]
Wikimedia Foundation.
2010.
Contenu soumis à la licence CC-BY-SA. Source : Article Réalisabilité de Wikipédia en français (auteurs)
Regardez d'autres dictionnaires:
Realisabilite — Réalisabilité Si on se place dans un cadre où chaque formule peut être « interprétée » par des programmes (voir l article Correspondance de Curry Howard), on dit qu un programme réalise la formule et l on écrit si est précisément l un… … Wikipédia en Français
Réalisibilité — Réalisabilité Si on se place dans un cadre où chaque formule peut être « interprétée » par des programmes (voir l article Correspondance de Curry Howard), on dit qu un programme réalise la formule et l on écrit si est précisément l un… … Wikipédia en Français
Réalisibilté — Réalisabilité Si on se place dans un cadre où chaque formule peut être « interprétée » par des programmes (voir l article Correspondance de Curry Howard), on dit qu un programme réalise la formule et l on écrit si est précisément l un… … Wikipédia en Français
Logique epistemique — Logique épistémique La logique épistémique est la logique de la connaissance d agents pris individuellement. Son nom vient du verbe grec epistémei qui signifie savoir, qui a aussi produit le mot épistémologie. Ses créateurs sont E. J. Lemmon and… … Wikipédia en Français
Logique Épistémique — La logique épistémique est la logique de la connaissance d agents pris individuellement. Son nom vient du verbe grec epistémei qui signifie savoir, qui a aussi produit le mot épistémologie. Ses créateurs sont E. J. Lemmon and Jaakko Hintikka.… … Wikipédia en Français
Logique épistémique — La logique épistémique est la logique de la connaissance d agents pris individuellement. Son nom est tiré du nom grec epistḗmē qui signifie connaissance (du verbe epístamai savoir ), d où vient aussi le mot épistémologie. Ses créateurs sont E. J … Wikipédia en Français
Logique intuitionniste — L intuitionnisme est une position philosophique vis à vis des mathématiques proposée par le mathématicien hollandais Luitzen Egbertus Jan Brouwer comme une alternative à l approche dite classique. Elle a été ensuite formalisée, sous le nom de… … Wikipédia en Français
INTUITIONNISME — Rien a priori de plus opposé au formalisme (cf. théorie de la DÉMONSTRATION; nous supposons que les deux premières parties de cet article sont familières au lecteur) que l’intuitionnisme . Alors que Hilbert met l’accent sur le côté mécanique des… … Encyclopédie Universelle
INVENTION — L’invention est l’acte de produire par ses propres moyens un élément, un objet ou un processus original; plus généralement, de produire ou de créer en utilisant son imagination: inventer une machine, inventer une histoire. Le terme a aussi un… … Encyclopédie Universelle
Correspondance De Curry-Howard — La correspondance de Curry Howard, appelée[1] également correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière entre la logique mathématique, l informatique théorique et la théorie de la… … Wikipédia en Français
