Nouveau professeur pour cette seconde partie : Michele Pagani

Rappels

En $\lambda$-calcul simplement typé:

Types:

$$A,B\stackrel{\scriptscriptstyle\mathrm{def}}{=}\sigma \mid A\to B$$

Termes:

$$M\stackrel{\scriptscriptstyle\mathrm{def}}{=}x\mid \lambda x^A.M\mid MN$$

Sémantique dénotationnelle dans $Set$:

• $⟦\sigma {⟧}_X=X\in Set$
• $⟦A\to B{⟧}_{\chi }=⟦B{⟧}_X^{⟦A{⟧}_X}$
• $⟦x_1:A_1,\cdots ,x_n:A_n⊢M:B{⟧}_X=⟦x_1:A_1{⟧}_X\times \cdots \times ⟦x_n:A_n{⟧}_X⟶⟦B{⟧}_X$

Exponentielle dans une CCC:

Pour le $\lambda$-calcul simplement typé: on a besoin d’un objet réflexif dans une CCC

i.e.

tout élément de $D\Rightarrow D$ est aussi un élément de $D$.

NB: $Set$ n’a pas d’objet réflexif, ce qui a poussé Dana Scott à définir ses domaines de Scott.

Modèles du $\lambda$-calcul

• $Set$ pour le simplement typé
• $Scott$ (CPOs et fonction Scott-continues): pour le $\lambda$-calcul typé et non typé
• $Stab$ (espaces cohérents et fonctions stables)

NB: sématnique dénotationnelle: pourquoi?

1. Pour étudier la théorie équationnelle entre les termes:

   $$M\sim N⟺⟦\Gamma ⊢M⟧=⟦\Gamma ⊢N⟧$$

   et parler “d’équivalences de programmes”, et de leurs propriétés partagées

2. on peut introduire de nouvelles primitives dans le calcul:

   $$A\Rightarrow B=!A⊸B$$

   Exemples:

   • primitives probabilistes
   • computation quantique ⟶ on a besoin de la linéarité (non duplication, etc…)

3. 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:

   $$⟦(\lambda x.x)y⟧=ev\circ ⟨\Lambda ({\pi }_2^2),{\pi }_2^2⟩$$

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 $\lambda$-calculi” ⟶ théorème 4.5.8

Th (Friedman, 1973): Let $X$ be an infinite set and $\text{⟦\_⟧\_X}$ be the interpretation of the simply typed $\lambda$-calculus in the CCC Set associating $X$ with the ground type. For any terms $\Gamma ⊢M:A$ and $\Gamma ⊢N:A$, we have:

$$M{=}_{\beta \eta }N⟺⟦M{⟧}_X=⟦N{⟧}_X$$

NB:

• on peut alors profiter du fait que travailler avec $⟦M{⟧}_X$ et $⟦N{⟧}_X$ est beaucoup plus agréable !

• pas vrai pour n’importe quelle CCC

$\beta \eta$-equivalence

Congruence:

• symetric
• reflexive
• transitive

• and:

  $$\begin{array}{c}\frac{M{=}_{\beta \eta }N}{\lambda x.M{=}_{\beta \eta }\lambda x.N}\\ \\ \frac{M{=}_{\beta \eta }NP{=}_{\beta \eta }Q}{MP{=}_{\beta \eta }NQ}\end{array}$$

${=}_{\beta \eta }$:

is the smallest congruence over $\Lambda$ s.t.

$$\begin{array}{c}(\lambda x.M)N{=}_{\beta \eta }M\{N/x\}\\ \lambda x.Mx{=}_{\beta \eta }M\text{ if }x\notin fv(M)\end{array}$$

Definition de $\text{⟦\_⟧\_X}$

• Variables ⟶ projections:

  $$⟦x_1:A_1,\cdots ,x_n:A_n⊢x_i:A_i⟧={\pi }_i$$

• $\lambda$-abstractions ⟶ use the adjonction:

  $$\begin{array}{c}⟦\Gamma ⊢\lambda x^A.M:A\to B⟧=\Lambda (⟦\Gamma ,x:A⊢M:B⟧)\\ =\overrightarrow{g}⟼(a⟼⟦M⟧(\overrightarrow{g},a))\end{array}$$

• Application ⟶ pairing:

  $$\begin{array}{c}⟦\Gamma ⊢MN:B⟧=ev\circ ⟨⟦\Gamma ⊢M:A\to B⟧,⟦\Gamma ⊢N:A⟧⟩\\ =\overrightarrow{g}⟼⟦M⟧(\overrightarrow{g},⟦N⟧(\overrightarrow{g}))\end{array}$$

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 ${=}_{\beta \eta }$

Trois actions possibles :

Le plus délicat: premier cas: $⟦(\lambda x.M)N⟧=⟦M\{N/x\}⟧$

Substitution lemma: Let $\Gamma ,x:A⊢M:B$ and $\Gamma ⊢N:A$, then

$$⟦\Gamma ⊢M\{N/x\}:B⟧=\overrightarrow{g}⟼⟦M⟧(\overrightarrow{g},⟦N⟧(\overrightarrow{g}))$$

Proof: By induction on $M$.

Attention: il y a une difficulté pour $⟦\lambda x.Mx⟧=⟦M⟧$ (contextes et types omis): on a besoin de montrer que $(a⟼⟦\Gamma ,x:A⊢M:B⟧(\overrightarrow{g},a)a)=(a⟼⟦\Gamma ⊢M:A\to B⟧(\overrightarrow{g},a))$, via

Weakening lemma: si $x\notin fv(M)$:

$$⟦\Gamma ,x:A⊢M:B⟧(\overrightarrow{g},a)=⟦\Gamma ⊢M:B⟧(\overrightarrow{g})$$

Complétude

Preuve de Friedman: définit

• un modèle syntaxique $S$

• une famille de relations $\{R^A{\}}_{A\in Types}$

  • $R^A\subseteq ⟦A{⟧}_X^{Set}\times ⟦A{⟧}^S$
  • pour tout $M$: $⟦⊢M:A{⟧}^{Set}{R}^A⟦⊢M:A{⟧}^S$

  • $R^A$ est fonctionnelle:

    $$\begin{array}{c}\forall d\in ⟦A{⟧}_X^{Set},⟦N⟧,⟦N^{\prime }⟧\in ⟦A{⟧}^S\\ d{R}^A⟦N{⟧}^S\text{ et }d{R}^A⟦N{⟧}^S⟹⟦N{⟧}^S=⟦N^{\prime }{⟧}^S\end{array}$$
  • $$\frac{⟦M{⟧}^S=⟦N{⟧}^S}{M{=}_{\beta \eta }N}$$

NB: $R^A$ est un cas particulier de relation logique (logical relation) ⟶ ex: les candidats de réductibilité (on s’intéressait aux termes fortement normalisables au lieu de la relation de $\beta \eta$-équivalence) étaient des cas particuliers de relation logique unaire.