Réalisabilité classique Une introduction
73
pages
Français
Documents
2011
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe en t'inscrivant gratuitement
Découvre YouScribe en t'inscrivant gratuitement
73
pages
Français
Ebook
2011
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
- logique implicative minimale
- correspondance preuves-programmes
- arithmétique d'ordre supérieur
- bornes sur la complexité des programmes
- terminaison des programmes
- réalisabilité classique
Réalisabilité classique
Une introduction
Aloïs Brunel
Vérité et Preuves - 11 Mars 2011Introduction
Sommaire
1 Introduction
2 La réalisabilité classique
3 Modèles et vérité subjective
Réalisabilité classique
2 / 30
NCertains programmes sans être typables sont corrects vis-à-vis
de l’ exécution :
let fonction = fun n =>
if n+1=0 then 16
else true
Le terme fonction a moralement le type Nat) Bool
La correction vis-à-vis du typage assure certaines propriétés :
La terminaison des programmes
Des bornes sur la complexité des programmes (logiques allégées)
:::
Réalisabilité classique
1 / 30
NLa correction vis-à-vis du typage assure certaines propriétés :
La terminaison des programmes
Des bornes sur la complexité des programmes (logiques allégées)
:::
Certains programmes sans être typables sont corrects vis-à-vis
de l’ exécution :
let fonction = fun n =>
if n+1=0 then 16
else true
Le terme fonction a moralement le type Nat) Bool
Réalisabilité classique
1 / 30
NGriffin, 90 : pour l’étendre à la logique classique (tiers exclu ou
formule de Peirce), on a besoin d’une nouvelle instruction : call-cc.
De manière générale, pour habiter de nouveaux axiomes il faut de
nouveaux programmes.
La correspondance preuves-programmes
Logique implicative minimale $ -calcul simplement typé
!Arithmétique d’ordre supérieur $ système F
:::
Réalisabilité classique
2 / 30
NDe manière générale, pour habiter de nouveaux axiomes il faut de
nouveaux programmes.
La correspondance preuves-programmes
Logique implicative minimale $ -calcul simplement typé
!Arithmétique d’ordre supérieur $ système F
:::
Griffin, 90 : pour l’étendre à la logique classique (tiers exclu ou
formule de Peirce), on a besoin d’une nouvelle instruction : call-cc.
Réalisabilité classique
2 / 30
NLa correspondance preuves-programmes
Logique implicative minimale $ -calcul simplement typé
!Arithmétique d’ordre supérieur $ système F
:::
Griffin, 90 : pour l’étendre à la logique classique (tiers exclu ou
formule de Peirce), on a besoin d’une nouvelle instruction : call-cc.
De manière générale, pour habiter de nouveaux axiomes il faut de
nouveaux programmes.
Réalisabilité classique
2 / 30
N
