Cours 1 : 𝛽-réduction et 𝛼-renommage

$\sim$ 1930 : Alonzo Church.

$𝜆$-termes :

$s,t,u, v \ldots :=$

variables : $x,y,z, \ldots$
applications : $uv$
$𝜆$-abstractions : $𝜆x.u$

Intro historique : crise des fondements mathématiques.

Hilbert, Church, Cantor

Cantor : a découvert que tout ensemble $A$ s’injecte strictement dans $𝒫(A)$ ⟶ cardinalités non comparables.

⟶ a écrit une lettre au pape pour s’excuser car “l’infini c’est Dieu, et Dieu est unique” (l’a beaucoup troublé).

Infini de $ℝ$ : $2^{\aleph_0} > \aleph_0$

$\aleph_1$ : plus petit cardinal strictement plus grand que $\aleph_0$.

Question :

\[\aleph_1 \overset{?}{=} 2^{\aleph_0}\]

⟶ Proposition indépendante de ZFC (on peut la rajouter ou rajouter sa négation).

NB : Beaucoup de logiciens sont morts fous.

Théroème de Zermello :: Tout ensemble peut être bien ordonné.

⟶ Pour le démontrer : part d’un certain ensemble d’axiomes (mais oublie l’axiome du choix).

Peano avait découvert 30 ans avant le caractère fondamental de l’axiome du choix ⟶ avait “tout inventé avant tout le monde” (théorie de l’intégration Borel/Lebesgue, Painlevé, …), mais on l’a oublié.

Church : “La théorie des ensembles, c’est nul” ⟶ ça ne parle que d’ensembles, les fonctions sont définies à partir des ensembles, etc…

NB : En maths, on fait des preuves qui pourraient se traduire en th des ensembles, mais dans les faits : on ne l’utilise pas en pratique.

⟹ Church invente le $𝜆$-calcul en 1940 pour remédier à ça (et fonder les maths).

Mais Kleene, son élève, découvrira plus tard ça n’exprime que les fonctions calculables ⟶ grosse déception pour Church.

Mais au début : tout le monde s’en fiche.

NB : Renommage des variables muettes ⟶ trivialité à formaliser.

Mais de manière “amusante” : Church s’était trompé la première fois là-dessus.

$𝛽$-réduction :: \[(𝛽) : \underbrace{(𝜆x.u)v}_{\text{un redex (Reduction Expression)}} ⟶ \underbrace{u[x:=v]}_{\text{contractum (du redex)}}\]

Quel était le bug de Church ?

Redécouvert par McCarthy en 53, avec Lisp, et l’a nommé “le problème du fun arg ascendant/descendant”

\[(𝜆x.x)v ⟶ v\]

ex :

\[(𝜆x.+x1)4 ⟶ +41\]

NB : le $𝜆$-calcul est non typé

Ex impossible à comprendre avec un esprit “bien typé” :

\[𝛿 ≝ 𝜆x.(xx)\]

Puis :

\[𝛺 ≝ 𝛿𝛿\]

Donc, par la $𝛽$-réduction :

\[𝛺 ≝ (𝜆x.xx)𝛿 ⟶ 𝛿𝛿 = 𝛺\]

⟶ programme qui boucle : équivalent du

while (1) ;;

NB : pourquoi on définit une relation binaire de “réduction”, si on voudrait plutôt une relation d’équivalence ?

⟶ d’un point de vue informatique, on va parler du “nombre d’étapes de réduction”, etc… (pas d’intérêt a priori en logique, mais on verra par la suite que si)

NB : Pour les parenthèses, on utilisera la même convention que OCamL :

\[xyz ≝ (xy)z ≠ x(yz)\]

L’application n’est PAS associative !

\[𝜆 x_1 ⋯ x_n.u = 𝜆 x_1 (𝜆x_2 ⋯ (𝜆x_n.u))))\]

\[(𝜆x.x)[x := yz] = 𝜆x.yz\]

car $𝜆yz.yz$ n’a pas de sens (pas un $𝜆$-terme).

Problème : ne préserve pas la sémantique

Plusieurs solutions :

Le meilleure : Solution de De Bruijn

On va faire autrement : si on “oublie” toutes les occurrences de $x$ après $𝜆x.$

\[(𝜆x.𝜆y.y)[y:=x]\\ = (𝜆x.𝜆y.y)\]

(fonction de projection sur la deuxième coordonnée)

\[(𝜆x.𝜆y.z)[z:=x]\\ = (𝜆x.𝜆y.x)\]

encore une fois : viole la sémantique intuitive.

Solution ? Remplacement des variables :

\[(𝜆x'.𝜆y'.z)[z:=x]\\ (𝜆x'.𝜆y'.x)\]

MAIS on ne peut pas faire ça, car on n’a pas de notion de substitution de variables : on est en train d’essayer de le faire !

NB : $𝜋$-calcul ⟶ il y a des variables liées qui deviennent libres !

Un patch qui marche : substitution partielle

Donnera :

soit le résultat attendu
soit sera non défini

Notion de variables libres / liées : définies par récurrence sur les termes de manière naturelle.

$fv(x)$ : “free variables” : ensemble des variables libres de $x$
$bv(x)$ : “bound variables” : ensemble des variables liées de $x$

NB : Il n’y a aucun rapport entre le fait d’être libre ou lié :

Ex :

\[𝜆z.\underbrace{(𝜆x.xy)}_{x \text{ lié}}\underbrace{(zx)}_{x \text{ libre}}\] \[fv = \lbrace x, y \rbrace \\ bv = \lbrace x, z \rbrace\]

Substitution partielle :

$u[x := v]$ défini lorsque $x∉bv(u)$
Puis, par récurrence sur $u$ lorsque $fv(u)∩bv(u) = ∅$

$𝛼$-équivalence

\[(𝛼) : 𝜆x.u \, 𝛼 \, 𝜆y.(u[x:=y])\]

$x≠y$
$x, y∉bv(u)$

MAIS : ces conditions sont vérifiées dans ce cas :

\[𝜆x.y \, 𝛼 \, 𝜆x.x\]

mais on ne pas qu’il y ait égalité, donc on rajoute la condition :

$y∉fv(u)$

Congruence $=_𝛼$ :

c’est une relation d’équivalence qui est une congruence, i.e :

\[u =_𝛼 v ⟹ uw =_𝛼 vw \\ u =_𝛼 v ⟹ wu =_𝛼 wv \\ u =_𝛼 v ⟹ 𝜆x.u =_𝛼 𝜆x.v \\\]

et c’est la plus petite congruence qui contient $𝛼$, avec $u=_𝛼v ≝ u \, 𝛼 \, v$

⟶ Convention de Barendregt :

on refuse d’avoir des variables libres et liées
on ne peut pas avoir deux variables liées de même nom (du type $𝜆x.𝜆y.𝜆x. \ldots$)

Mais problème ici :

\[(𝜆x.yxx)(𝜆z.z) ⟶ y (𝜆z.z) (𝜆z.z)\]

⟹ on le remplace, icognito, par :

\[(𝜆x.yxx)(𝜆z.z) ⟶ y (𝜆z.z) (𝜆z'.z')\]

Morale : On peut considérer tous les termes modulo $𝛼$-renommage et tout se passe bien.

\[\begin{align*} (𝜆x.x(𝜆y.yyx)(𝜆z.xz))(𝜆x',y',z'.x'y'z') & = (𝜆x',y',z'.x'y'z')(𝜆y.yy(𝜆x',y',z'.x'y'z'))(𝜆z.(𝜆x',y',z'.x'y'z')z) \\ & \\ \end{align*}\]

$u$ se $𝛽$-contracte en $v$, noté $u ⟶_𝛽 v$

NB : pas de réduction parallèle : contraction de plusieurs redex identiques en même temps de la même manière.

  digraph {
    rankdir=TB;
    A[label="(𝜆y.(𝜆x.x)y)z"];
    B[label="(𝜆x.x)z"];
    C[label="(𝜆y.y)z"];
    D[label="z"];
    A -> {B,C};
    B -> D;
    C -> D;

  }

Fortement normalisable ( = terminant) :: toutes les branches terminent
Normalisable ( = faiblement trerminant) :: il existe une branche qui termine

Ex :

l’ex précédent est fortement normalisable, donc a fortiori normalisable.
$𝛺$ n’est pas normalisable
Normalisable mais pas fortement normalisable :

  digraph {
    rankdir=TB;
    A[label="(𝜆x.y)𝛺"];
    B[label="y"];
    C[label="(𝜆x.y)𝛺"];
    D[label="(𝜆x.y)𝛺"];
    E[label="⋯"];
    A -> {B,C};
    C -> D;
    C -> B;
    D -> E;
    E -> B;
    D -> B;
  }

Si on prend deux stratégies différentes qui arrivent à une forme normale, c’est nécessairement la même.

Relations binaires

Soit $⟶$ une relation binaire sur $A$.

Prop de Church-Rosser (CR) :

ssi $\overset{\ast}{\longleftrightarrow} = \overset{\ast}{⟶}\overset{\ast}{⟵}$

NB :

c’est la plus petite relation d’équivalence qui contient $⟶$.
Dans la théorie des groupes $1\cdot x$ n’est pas un redex, $x$ non plus, donc on ne peut pas les réduire pour obtenir la même chose. Mais ils sont égaux ⟶ pas de Church-Rosser

Confluence :: si $u ⟶^\ast v_1$ et $u⟶^\ast v_2$, alors il existe $w$ tel que $v_1 ⟶^\ast w$ et $v_2 ⟶^\ast w$

Th : La confluence équivaut à CR

Le $𝜆$-calcul est confluent.

Confluence locale :: si $u ⟶ v_1$ et $u⟶ v_2$, alors il existe $w$ tel que $v_1 ⟶^\ast w$ et $v_2 ⟶^\ast w$

Évidemment : Confluence ⟹ Confluence locale, mais la réciproque n’est pas vraie :

Contre-exemple de Curry

  digraph {
    A -> B;
    B -> A;
    A -> C;
    B -> D;
  }

C’est localement confluent

\[A ⟶ C \\ A ⟶ B\]

puis $B ⟶ C$

mais pas confluent :

\[A ⟶ C \\ A ⟶ B ⟶ D\]

Confluence forte :: si $u ⟶ v_1$ et $u⟶ v_2$, alors il existe $w$ tel que $v_1 ⟶^{≤1} w$ et $v_2 ⟶^{≤1} w$

Confluence forte + réduction parallèle ⟹ confluence

Th de Neumann :

Si $⟶$ est localement confluente, fortement normalisante, alors elle est confluente.

Hypothèse superflue :

$⟶$ finiment branchante :: tous les sommets du diagramme sont d’arité finie.

Lemme de König :

Tout arbre $T$ tq :

(a) $T$ est à branchement fini

(b) toutes les branches de $T$ sont finies

(c) est fini.

NB :

  digraph {
    rankdir=TB;
    A -> A11;
    A -> A21;
    A21 -> A22;
    A -> A31;
    A31 -> A32;
    A32 -> A33;
    A -> ⋯;
  }

Toutes les branches sont finies, mais il n’existe pas de plus grande branche.

On montre

\[¬(c)∧ (a) ⟹ ¬(b)\]

Arbre :: Ensemble ordonné (par la relation “être ancêtre de”) bien fondé, dont les segments initiaux sont des chaînes (totalement ordonnés).

NB : Le lemme de König est une forme faible de l’axiome du choix ⟶

axiome des choix dépendants :: si j’ai une fonction qui a toute suite de choix finis associe un nouveau choix, il existe une fonction de choix.

MAIS :

Gödel : l’axiome du choix est indépendant de la théorie ZF

⟶ avec ensembles constructibles :: la plus petite famille d’ensembles qu’on peut former avec les constructions classiques de ZF.

Gödel montre que le sous-modèle des ensembles constructibles vérifie immédiatement l’AC dès qu’il existe un modèle des ensembles le vérifiant.

⟹ Il y a une hiérarchie d’axiomes, plus ou moins forts : AC > Axiome des choix dépendants, etc…

NB : Peano, 30 ans avant Zermello, avait eu ce problème, dans König, et avait déjà pris des précautions dans la définition des arbres pour ne pas avoir à recourir à l’AC.

\[𝜈(u) = \max \lbrace \text{ longueur d'une branches } u ≝ u_0 ⟶ ⋯ ⟶ u_n \rbrace\]

  digraph {
    rankdir=TB;
    A[label = "Confluence locale"];
    B[label = "Confluence"];
    C[label = "Confluence forte"];
    D[label = "Church-Rosser"];
    A -> B[label="si ft normalisant (Neumann)"];
    B -> A;
    C -> B;
    B -> D;
    D -> B;

  }

Confluence ⟹ Propriété de la forme normale unique

$𝜂$-règle

\[(𝜂) : 𝜆x.ux ⟶ u\]

uniquement si

\[x∉fv(u)\]

NB :

Aucun langage de programmation n’implémente $𝜂$ : ni OCamL, ni Coq, …
Il y a $𝛽$-équivalence si $u$ est une abstraction : $u ≝ 𝜆y.t$
MAIS : il existe des termes $u$ (par ex: les variables : $u≝y$) tels que
\[𝜆x.yx ≠_{𝛽} y\]
En effet : par l’absurde, sinon : il seraient réductibles, par confluence, en un même terme $w$ : mais ils sont déjà en forme normale !

NB : cf. Procédure de Knuth et Bendix

$𝜆^\ast$-calcul

On rajoute des termes de la forme

let x=u in v

let x=u in v ⟶ $v[x:=u]$

Prop : le $𝜆^\ast$-calcul est fortement confluent

NB : Barendregt en a inventé une preuve utilisant une “mesure entière”.

\[SN ≝ \lbrace u \mid u \text{ termine } \rbrace\] \[\overline{SN} ≝ \lbrace 𝜃≝ [x_1 := w_1, ⋯, x_n := w_n ], \text{ où } w_i∈SN \rbrace\]

Substitution parallèle $𝜃 ≝ [x_1 := w_1, ⋯, x_n := w_n ]$ :: une fonction qui à chaque $x_i$ associe $w_i$ (modulo $𝛼$-renommage, toujours)

Dém :

Démontrons, apr réc sur la structure de $u$ :

\[u∈ SN\]

Si $u = x$ : OK
Si $u = st$, $u ⟶ s_1 t_1 ⟶ ⋯$ : où on réduit à gauche ou à droite à chaque étape. Si la réduction est infinie, il y a une réduction infinie à gauche ou à droite : impossible, car $⟶$ est fortement normalisante par HR.
$u = 𝜆x. s$, $𝜆x. s_1 ⟶ 𝜆x. s_2 ⟶ ⋯$ est finie.
$u = $ let x=s in t ⟶ $u = $ let x=s' in t'

⟶ Il “faut” renforcer l’hypothèse de récurrence

Pouvoir expressif du $𝜆$-calcul

On va coder toutes les fonctions calculables, grâce aux fonctions récursives de Gödel : la plus petite classe de fonctions contenant les fonctions constantes, la fonction successeur, les projections, la récurrence primitive (cf. le cours de calculabilité).

BUT : Pour chaque $f$ récursive, on veut trouver un $𝜆$-terme $\lceil f \rceil$ tq :

\[∀n_1, ⋯, n_k ∈ℕ, \text{ si } f(n_1, ⋯, n_k) \text{ défini, alors } \lceil f \rceil \lceil n_1 \rceil ⋯ \lceil n_k \rceil ⟶^\ast \lceil f(n_1, ⋯, n_k) \rceil\]

let rec f x  = u f x in f

Le terme $f$ cherché est tq

\[∀v, fv =_{𝛽} u f v\]

On cherche un $f$ tq :

\[f =_{𝛽} uf\]

⟶ un point fixe de $u$

⟶

Th : Tous les termes du $𝜆$-calcul ont un point fixe, et même MIEUX :

Il existe un terme clos (appelé combinateur, souvent noté $y$) tq :
\[∀u, yu \text{ est un point fixe de } u\]

Corollaire : $yu =_{𝛽} u (yu)$

Combinateur de pts fixes de Church

\[Y ≝ 𝜆f.(𝜆x.f(xx))(𝜆x.f(xx))\]

NB : aucun combinateur de point fixe ne peut normaliser.

\[Yu ⟶_𝛽 (𝜆x. u(xx)) (𝜆y. u(y)) \\ ⟶_𝛽 u (𝜆y. u(y)) (𝜆y. u(y)) \\ ⟵_𝛽 u(Yu)\]

Combinateur de pts fixes de Turing :

\[𝛳 ≝ AA\]

où

\[A ≝ 𝜆g,h.h(ggh)\]

⟶

\[𝛳u ⟶_𝛽 (𝜆g,h.h(ggh))Au \\ ⟶_𝛽 u(AAu) ⟵_𝛽 u(𝛳u)\]

Donc let rec f x = u f x in f $≝ Yu$

Déf : $u ⟶_1 v$ ssi il existe un $𝜆^\ast$-terme $u’$ tel que $u’$

est obtenu à partir de $u$ en ajoutant des $\ast$ à certains rédex.

$u’ ⟶^\ast v$ en $𝜆^\ast$-calcul

NB : $v$ est un $𝜆$-terme, mais aussi en particulier un $𝜆^\ast$-terme.

Effacement des étoiles :: \[E(u')=u\]

\[match = 𝜆m \underbrace{x}_{\text{si } m=0} \underbrace{y}_{\text{si } m≠0}. m \, (𝜆z. y (pred \, \, m)) \, x \\ ⟹ match 0 \, u \, v ⟶^\ast u \\ match (m+1) \, u \, v ⟶^\ast v m\]

Th : Pour toute fonction récursive $f: ℕ^k⟶ℕ$, il existe un $𝜆$-terme $f$ tq

Si $f(n_1, ⋯, n_k)$ est définie, alors $\lceil f \rceil \lceil n_1 \rceil ⋯ \lceil n_k \rceil ⟶^\ast \lceil f(n_1, ⋯, n_k) \rceil$

Si $f(n_1, ⋯, n_k)$ n’est pas définie, alors $\lceil f \rceil \lceil n_1 \rceil ⋯ \lceil n_k \rceil$ ne termine pas

Théorème de standardisation

Forme de tête :

tout terme $u$ s’écrit de façon unique $𝜆 x_1 ⋯ x_n. h u_1 ⋯ u_n$ où

$h$ (la tête) est
- soit une variable $x$ : la variable de tête ⟶ alors de $u$ est en forme “normale de tête” (ce n’est pas nécessairement une forme normale par contre).
- soit une $𝜆$-abstraction $𝜆x.t$ (et alors $n≥1$), et $(𝜆x.t)u_1$ est appelé rédex de tête

Réduction de tête :

$u⟶_t v$ ssi $u = 𝜆x_1 ⋯ x_m. (𝜆x.t) u_1 ⋯ u_n$ ($n≥1$) et $v=𝜆x_1 ⋯ x_m.t[x:=u_1] u_2 ⋯ u_n$

NB : elle est dite faible si $m=0$ : c’est une réduction de tête faible qu’implémentent les langages qui font de l’appel par nom.

Ex $𝜆x. x((𝜆y.y)z)$ est en forme normale de tête, mais pas en forme normale.

  digraph {
    rankdir=TB;
    App2[label="App"];
    𝜆x -> App;
    App -> {x, App2};
    App2 -> {𝜆y, z};
    𝜆y -> y;
  }

⇓

  digraph {
    rankdir=TB;
    h[label="𝜆x_1⋯x_n.h"]
    h -> {u_1, u_2, ⋯, u_n};
  }

R. David : Réduction standard ⟶ on descend dans l’arbre pour réduire, en s’interdisant de remonter.

$u ⟹_s v$ ssi

soit $v$ n’est pas une variable ($m≥1$ ou $n≥ 1$) : $u ⟶ ^\ast_t 𝜆 x_1 ⋯ x_m. u_0 ⋯ u_n \\ ⟹_s 𝜆 x_1 ⋯ x_m. v_0 ⋯ v_n = v$

sinon : $u ⟶^\ast_t v$

Th : $⟶^\ast = ⟹_s$

Share on

Twitter Facebook Google+ LinkedIn

Quel était le bug de Church ?

Un patch qui marche : substitution partielle

$𝛼$-équivalence

Relations binaires

Contre-exemple de Curry

$𝜂$-règle

$𝜆^\ast$-calcul

Pouvoir expressif du $𝜆$-calcul

Théorème de standardisation

Share on

Leave a comment