SMF

Réalisabilité en logique classique

Realizability in classical logic

Jean-Louis KRIVINE
Réalisabilité en logique classique
  • Consulter un extrait
  •  
                
  • Année : 2009
  • Tome : 27
  • Format : Électronique
  • Langue de l'ouvrage :
    Anglais
  • Class. Math. : 03B40, 68N18
  • Pages : 197-229

On construit un cadre, appelé maintenant « réalisabilité classique », pour explorer la correspondance de Curry-Howard (preuves-programmes). Le côté « programmation » de la correspondance est un langage impératif de bas niveau, basé sur une machine lambda-calcul en appel par nom. Le côté « preuve » est la formalisation habituelle de l'Analyse en logique du second ordre. On obtient ainsi des programmes pour toutes les preuves classiques de theorèmes d'Analyse. Pour certains d'entre eux, on résout le problème de la « spécification » : trouver le comportement commun de tous ces programmes, pour un théorème donné. On montre que l'axiome du choix dépendant (qui est essentiel pour l'Analyse) correspond, en programmation, à des instructions très simples : l'horloge et la signature.

We build a framework, now called “classical realizability”, to explore the Curry-Howard (proof-program) correspondence. The “programming” side of the correspondence is an imperative low level language, based on a call-by-name lamda-calculus abstract machine. The “proof” side is usual formalization of Analysis in second order logic. In this way, we can get programs for all classical proofs of theorems in Analysis. For some of them, we solve the “specification problem” : find the common behaviour of all these programs, for a given theorem. We show that the axiom of dependent choice (essential for Analysis) corresponds to very simple programming instructions : clock and signature.

lambda-calcul, isomorphisme de Curry-Howard, correspondance preuves-programmes, axiome du choix dépendant
Lambda-calculus, Curry-Howard isomorphism, proof-program correspondence, dependent choice axiom