Notes sur les λσ-calculs

1 Un λυ-calcul avec noms

On définit la syntaxe suivante pour le λυ-calcul :

t ::= n | λn.t | (t t) | t[n := t] | t↑_{n}

Les règles de réduction sont

(λn.t u) → t[n := u]  Beta
n[n := t] → t  V ar_{1}
p[n := t] → p  p < n  V ar_{2}
p[n := t] → p − 1  p > n  V ar_{3}
(t u)[n := v] → (t[n := v] u[n := v])  App
(λp.t)[n := u] → λ(p − 1).(t[n := u↑_{p}])  Abs
p↑_{n} → p  p < n V arLift_{1}
p↑_{n} → p + 1  p ≥ n V arLift_{2}
(t u)↑_{n} → (t↑_{n} u↑_{n})  AppLift
(λp.t)↑_{n} → λp.(t↑_{n})  p < n AbsLift_{1}
(λp.t)↑_{n} → λ(p + 1).(t↑_{n})  p ≥ n AbsLift_{2}

Remarque : ce calcul revient à prendre des indices de de Bruijn numérotés à rebours. Il n’est pas complètement avec noms dans la mesure où le choix des indices de liaison dépend du nombre de variables libres présentes dans le contexte.

2 Confluence sur termes ouverts et terminaison

Il suffit de prendre le λυ-calcul en remplaçant la règle App par la restriction suivante :

(n u_{1} ... u_{n})[p := v] → ((x u_{1} ... u_{n−1})[p := v] u_{n}[p := v])

Certes, ce n’est pas local. En revanche, si on adopte un \overline{λ}υ-calcul, on obtient une condition locale :

(p [u_{1}; ...; u_{n}])[p := v] → (v [u_{1}; ...; u_{n}][p := v])(q [u_{1}; ...; u_{n}])[p := v] → (q [u_{1}; ...; u_{n}][p := v]) q ≠ p

3 Simulation de la β-réduction

En ce cas, il faut évidemment la règle App dans toute sa généralité.

4 Simulation de la β-réduction + confluence sur termes ouverts

Par exemple, en permettant la formation de listes de substitutions et en ajoutant une règle Map.

\begin{aligned}t & ::= & n | λn.t | (t t) | t[s] | t↑_{n} \\ s & ::= & n := t | n := t; p := t avec n < p \end{aligned}

Aux règles précédentes, on ajoute les règles suivantes :

\begin{aligned}t[n := u][p := v] & → & t[n := u[p := v]; p := v] & (n ≤ p) & Map_{1} \\ t[n := u][p := v] & → & t[p := v; n := u[p := v]] & (n > p) & Map_{2} \\ t[n := u]↑_{p} & → & t↑_{p} [n := u↑_{p}] & n < p & MapLift_{1} \\ t[n := u]↑_{p} & → & t↑_{p} [n + 1 := u↑_{p}] & n ≥ p & MapLift_{2} \end{aligned}

Cependant, dans ce calcul, on peut construire un contre-exemple à la terminaison du simplement typé.

Un exemple de non-terminaison en λ-calcul avec substitution explicite

De fait, on peut reproduire dans ce calcul l’exemple suivant, proche de celui de Paul-André :

T = (λ2.(λ3.3 (λ3.3 1)) (λ2.21))

On pose :

\begin{aligned}t_{1} & = & (λ2.2 1) \\ s_{n} & = & 2 := t_{n} \\ t_{n+1} & = & 1[s_{n}] \\ t′_{1} & = & (λ3.3 1) \\ s′_{n} & = & 3f := t_{n} ↑_{2} \end{aligned}

Et on a : Lemma 1

t_{1} ↑_{2} = (λ2.2 1)↑_{2}
→^{4} (λ3.3 1)  (AppLift) + (AbsLift) + (V arLift)
= t′_{1}

Lemma 2

T = (λ2.(λ3.3 (λ3.3 1)) t_{1})
→ (λ2.(3[3 := (λ3.3 1)]) t_{1})  (Beta)
→ 3[3 := (λ3.3 1)][2 := t_{1}]  (Beta)
→ 3[2 := t_{1}; 3 := (λ3.3 1)[2 := t_{1}]] (Map)
= 3[s_{1}; 3 := t′_{1}[s_{1}]]

Lemma 3

t′_{1}[s_{n}] = (λ3.3 1)[2 := t_{n}]
→ ((λ3.3)[2 := t_{n}] 1[2 := t_{n}])  (App)
→ (λ2.(3[2 := t_{n} ↑_{2}]) 1[2 := t_{n}])  (Abs)
→ 3[2 := t_{n} ↑_{2}][2 := 1[2 := t_{n}]]]  (Beta)
→ 3[2 := t_{n} ↑_{2} [2 := 1[2 := t_{n}]]; 2 := 1[2 := t_{n}]] (Map)
= 3[2 := t_{n} ↑_{2} [s_{n+1}]; s_{n+1})]

Lemma 4

t_{n+1} ↑_{2} [s_{p}] = 1[2 := t_{n}]↑_{2} [2 := t_{p}]
→^{2} 1[3 := t_{n} ↑_{2}][2 := t_{p}]  (MapLift) + (V arLift)
→ 1[2 := t_{p}; 3 := t_{n} ↑_{2} [2 := t_{p}]]  (Map)
= 1[s_{p}; 3 := t_{n} ↑_{2} [s_{p}]]

D’où la présence de la suite infinie de motifs t′_{1}[s_{n}]

On remarque dans ce contre-exemple que les seules règles permutant des rédex (et donc non indispensables pour mener à bien la normalisation) sont les règles App (dans le cas particulier où l’application n’est pas en forme normale de tête) et les 4 règles Map. En particulier, l’opérateur de composition n’est pas nécessaire pour avoir la non-terminaison.

Cependant, dans quelle mesure les spécificités propres aux différentes versions de calculs dans la manière de gérer les captures de variables influent sur la possibilité de dériver tel ou tel contre-exemple. En particulier, y a-t-il un contre-exemple “universel” qui soit traductible dans n’importe quelle version de λ-calcul avec listes de substitutions, mais sans composition, quelle que soit la manière de gérer les indices (noms explicites, de Bruijn, de Bruijn inverse).