Cours 2 : 𝜆-calcul simplement typé

$𝜆$-calcul simplement typé

$F, G, ⋯,$ =

  • $b$ : type de base
  • $F⟶G$

Jugement de typage : $\underbrace{x_1:F_1, x_2:F_2, ⋯, x_n:F_n}_{ \text{contexte de typage : } 𝛤} \vdash u:F$

  • $𝛤, 𝛥$ : union de $𝛤$ et $𝛥$, si leurs ensembles de variables sont disjoints
  • $𝛤, x:F$ : union de $𝛤$ et $\lbrace x:F \rbrace$

Règle des variables :

\[\cfrac{}{𝛤, x:F \vdash x:F}\quad (Var)\]

Règle d’application :

\[\cfrac{𝛤 \vdash u:F ⟶ G \qquad 𝛤 \vdash v:F}{𝛤 \vdash uv : G}\quad (App)\]

Règle d’application :

\[\cfrac{𝛤, x:F \vdash u:G}{𝛤 \vdash 𝜆x. u : F⟶G}\quad (Abs)\]

à $𝛼$-équivalence près

\[\cfrac{\cfrac{}{𝛤, x:F \vdash x:F} \quad (Var)}{𝛤 \vdash 𝜆x. x: F⟶ F}\quad (Abs)\]

MAIS :

$𝜆x. xx ≝ 𝛿$ n’est pas typable

LEMME : Subject reduction (Auto-réduction) :

Si $𝛤 \vdash u:F$ dérivable et si $u ⟶^\ast v$, alors

\[𝛤 \vdash v:F\]

dérivable

Lemme (Affaiblissement) :

si $𝛤 \vdash u:F$ dérivable, alors $𝛤, 𝛥 \vdash u:F$

Heureusement qu’on a considéré $(Abs)$ à $𝛼$-renommage près !

Correspondance de Curry-Howard

Types = Formules

Les Types sont maintenant des formules !!!

Et les derivations de typage des preuves !

Programmes : $𝜆$-termes typés = Preuves

Exécution : $𝛽$-réduction = Simplification des preuves = Élimination des détours/coupures

Élimination des coupures :

Th : Si $𝛤 \vdash u:F$ dérivable, alors $u$ est fortement normalisable.

Gödel-Dummett : logique intuitionniste + $∀P, Q, P⟶Q ∨ Q ⟶ P$

⟶ strictement intermédiaire entre la logique intuitionniste et la logique classique

\[𝒞(\underbrace{u}_{¬¬(F⟶G)})\underbrace{v}_{F} ⟶ 𝒞(𝜆 \underbrace{k}_{¬G}. u (𝜆 \underbrace{f}_{F⟶G} . k (fv)))\]

Mathias Felleisen

Th : Si $u$ est typable au premier ordre, alors $u$ est fortement normalisable.

Système-T de Gödel : transforme les preuves de l’arithmétique ordinaires en des preuves utilisant des schémas d’axiomes primitifs récursifs d’ordre supérieur (⟶ système cohérent).

Th : tout terme typable dans le Système-T est dans $S_N$

Corollaire : L’arithmétique est cohérente.

Système F

Girard 1971 / Reynolds 1974

\[PA_2 / HA_2 \vdash F ⟺ LK_2 / LJ_2 + Peano° \vdash F°\]
Types Logiques Arithmétique
$F$ $LJ_2$ $HA_2$
$F_𝜔$ $F_𝜔$ $HA_𝜔$
$LF$    

Implémentations du $𝜆$-calcul

Deux difficultés :

  1. $𝛼$-renommage
  2. complexité de la $𝛽$-réduction

Machines d’environnements

\[(programme, environnement) \\ ((𝜆x.u)v, 𝜌) ⟶ (u, 𝜌[x \mapsto v]) \\ (x, 𝜌) ⟶ (𝜌(x), 𝜌)\]

Machines de Krivine

Sans environnement :

  • Sémantique : $(u, l) = “u u_1 ⋯ u_n”$ où $l = [u_1, ⋯, u_n]$
Machine de Krivine :
\[(uv, l) ⟶ (u, v :: l)\\ (𝜆x.u, v::l) ⟶ (u[x:=v], l)\]

Si $u ⟶^\ast_{\text{red. de tête faible}} x u_1 ⋯ u_n$, alors

\[(u, [\;]) ⟶^\ast_{\text{Krivine}} (x, [u_1, ⋯, u_n])\]

Combinateurs $S, K, I$

$\ast$ : traduction

\[(x)^\ast = x \\ (MN)^\ast = M^\ast N^\ast \\ (𝜆x. M)^\ast = [x]M^\ast\]

où

  • $[x]x = I$
  • $[x]y = Ky$
  • $[x]S = KS$
  • $[x]K = KK$

  • $[x]I = KI$

  • $[x]MN = S\; ([x]M)\; ([x]N)$

Calculs à substitutions explicites

Géométrie de l’interaction

Par Girard

$𝜆$-calculs à substitutions explicites

$𝜆𝜎$-calcul (ACCL 90) et $𝜆𝜐$-calcul par Rouyer-Degli-Lescanne 94

$𝜆𝜎$-calcul

Notation de De Bruijn :

\[M, N, P, ⋯ := 1 \mid MN \mid 𝜆M \mid M[S]\]

Piles :

\[S, S', ⋯ := \underbrace{id}_{\text{pile vide}} \mid \underbrace{M \cdot S}_{M \textsf{ cons } S} \mid \underbrace{\uparrow}_{\text{shift}} \mid S \circ S'\]

Règles de réécriture :

  • $(𝛽)$-réduction : $(𝜆M)N ⟶ M[N \cdot id]$ : $M$ évalué dans une pile où la variable $1$ vaut $N$, les autres sont inchangées

Non fortement normalisant

$𝜆𝜎$-calcul

  • $M \cdot id$ est remplacé par $M/$

  • $1 \cdot (S\circ \uparrow)$ devient le “lift de $S$” : $\Uparrow S$

Leave a comment