Un algorithme d'abstraction

Theorème. On a :

(λ⁺x.M) N := [N / x] M et x ∉(λ⁺x.M)

et :

(λ⁺x.M) est une forme normale.

Démonstration : x ∉ (λ⁺x.M)

BASE

Si M est une constante, (λ⁺x.M) ≡ K M ne contient pas x.
Si M ≡ x, (λ⁺x.M) ≡ I ne contient pas x.
Si M ≡ y ≠ x, (λ⁺x.M) ≡ K y ne contient pas x.

PAS

Si M ≡ P Q, (λ⁺x.M) ≡ S (λ⁺x.P) (λ⁺x.Q) ne contient pas x puisque (λ⁺x.P) et (λ⁺x.Q)
ne contiennent pas x par hypothèse d’induction.

Démonstration (λ⁺x.M) est une forme normale

BASE

Si M est une constante, (λ⁺x.M) ≡ K M est une f.n.
Si M ≡ x, (λ⁺x.M) ≡ I est une f.n.
Si M ≡ y ≠ x , (λ⁺x.M) ≡ K y est une f.n.

PAS

Si M ≡ P Q, (λ⁺x.M) ≡ S (λ⁺x.P) (λ⁺x.Q) est une f.n. puisque (λ⁺x.P) et (λ⁺x.Q) sont des f.n. par hypothèse d’induction.

Démonstration : (λ⁺x.M) N := [N / x] M

BASE

Si M est une constante, (λ⁺x.M) N ≡ K M N := M [N / x] ≡ M
Si M ≡ x, (λ⁺x.M) N ≡ I N := N ≡ [N/ x]x ≡ [N/ x]M
Si M ≡ y ≠ x, (λ⁺x.M) N ≡ K y N := y ≡ [N / x] y ≡ [N / x] M

PAS
Si M ≡ P Q,
(λ⁺x.M) N ≡ S (λ⁺x.P) (λ⁺x.Q) N := (λ⁺x.P) N ((λ⁺x.Q) N)
Par hypothèse d’induction on a (λ⁺x.P) N := [N / x]P et (λ⁺x.Q) N := [N / x]Q, donc :
(λ⁺x.M) N := ([N / x]P)([N / x]Q) ≡ [N / x](P Q) ≡ [N / x] M