Réalisabilité classique Une introduction

Aloïs Brunel

Description

Réalisabilité classique Une introduction Aloïs Brunel Vérité et Preuves - 11 Mars 2011

• logique implicative minimale


• correspondance preuves-programmes


• arithmétique d'ordre supérieur


• bornes sur la complexité des programmes


• terminaison des programmes


• réalisabilité classique

Sujets

• Brunel

Informations

• Publié par: profil-urra-2012
• Publié le: 01 mars 2011
• Nombre de lectures: 35
• Langue: Français

Extrait

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