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])

si

  • $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))(𝜆x',y',z'.x'y'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 Chruch-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 Chruch-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 = "Chruch-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

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

  • $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

Leave a Comment