73 pages
Français

Réalisabilité classique Une introduction

-

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

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

Informations

Publié par
Publié le 01 mars 2011
Nombre de lectures 24
Langue Français

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