Cours 13: Théorème de Friedman: correction
Nouveau professeur pour cette seconde partie : Michele Pagani
Rappels
En
- Types:
-
- Termes:
-
Sémantique dénotationnelle dans
Exponentielle dans une CCC:
Pour le
i.e.
tout élément de
NB:
Modèles du -calcul
pour le simplement typé (CPOs et fonction Scott-continues): pour le -calcul typé et non typé (espaces cohérents et fonctions stables)
NB: sématnique dénotationnelle: pourquoi?
-
Pour étudier la théorie équationnelle entre les termes:
et parler “d’équivalences de programmes”, et de leurs propriétés partagées
-
on peut introduire de nouvelles primitives dans le calcul:
Exemples:
- primitives probabilistes
- computation quantique ⟶ on a besoin de la linéarité (non duplication, etc…)
-
Compilation dans le langage haut-niveau vers un langage bas-niveau: Ex: Categorical Abstract Machine (a donné naissance à CamL) basée sur les catégories cartésiennes closes.
Ex:
NB: dans cette seconde partie du cours, on se concentrera surtout sur 1 et 2.
Théorème de Friedman (1973)
Chap. 4 de AMADIO-CURIEN: “Domains and
Th (Friedman, 1973): Let
be an infinite set and be the interpretation of the simply typed -calculus in the CCC Set associating with the ground type. For any terms and , we have:
NB:
-
on peut alors profiter du fait que travailler avec
et est beaucoup plus agréable ! -
pas vrai pour n’importe quelle CCC
-equivalence
- Congruence:
-
- symetric
- reflexive
- transitive
-
and:
:-
is the smallest congruence over
s.t.
Definition de
-
Variables ⟶ projections:
-
-abstractions ⟶ use the adjonction: -
Application ⟶ pairing:
NB: on a fait un effacement dans le premier point, une duplication dans le dernier point.
Démonstration du théorème de Friedman
Correction
par induction sur la taille de la dérivation de
Trois actions possibles :
Le plus délicat: premier cas:
Substitution lemma: Let
and , then
Proof: By induction on
Attention: il y a une difficulté pour
Weakening lemma: si
:
Complétude
Preuve de Friedman: définit
- un modèle syntaxique
-
une famille de relations
- pour tout
: -
est fonctionnelle: -
NB:
Leave a comment