L'equivalence de Curry Howard en logique lineaire

De
Publié par

L'equivalence de Curry Howard en logique lineaire David Salinas 14 fevrier 2010

  • equivalence de curry howard en logique lineaire

  • isomorphisme classique de curry-howard

  • logique intuitioniste

  • nj construction de l'equivalence de curry


Publié le : lundi 1 février 2010
Lecture(s) : 47
Source : math.unice.fr
Nombre de pages : 22
Voir plus Voir moins
Lequivalence
de
Curry
Howard
David Salinas
14
f´evri er
2010
en
logique
lineaire
Sommaire
Isomorphisme classique de Curry-Howard La logique intuitioniste NJ Construction de l’equivalence de Curry Howard Propriete fondamentale
L’isomorphisme lineaire de Curry Howard La logique intuitionniste lineaire Le λ calcul lineaire L’isomorphisme lineaire de Curry-Howard Interpretation
Logique intuitioniste
La syntaxe
I
Enonces
de
la forme
p ::= α
suivante
:
| ⊥ | p
p
|
p
p
|
p
p
Logique
Les
intuitioniste
regles
Equivalence de Curry Howard Donnez une preuve, je vous donnerai un programme et reciproquement
I On remplace Δ = p 1 , ..., p n par Δ = x 1 : p 1 , ..., x n : p n ou les x i sont des variables distinctes I on annote les noeuds
On obtient des temoins de preuves de la forme
t , u , v = x | λ x p . t | ( t u )
Equivalence
Elimination
des
de
Curry
coupures
et
β
Howard
reduction
Equivalence de Curry Howard... ... expliquee en un tableau
logique en deduction naturelle formule derivation conclusion regle hypothese introduction de elimination de coupure (sur )
λ calcul a la Church type λ terme type du terme variable λ abstraction application β redex
Equivalence de Curry Howard Propriete fondamentale
Theoreme Si Δ ` t : p alors t est confluent et fortement normalisant
Forme des formes normales Elles sont engendrees par la grammaire
n := x | λ p . n | ( x n 1 ... n k )
Plan
Isomorphisme classique de Curry-Howard
L’isomorphisme lineaire de Curry Howard La logique intuitionniste lineaire Le λ calcul lineaire L’isomorphisme lineaire de Curry-Howard Interpretation
La
logique intuitionniste lineaire
I
I
On a vu en cours la logique intuitionniste classique
La logique lineaire intuitioniste a les memes regles sauf que l’on s’autorise une seule formule a droite du sequent dans les regles
La
Les
logique
re
les
intuitionniste
lineaire
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.