Programmation fonctionnelle - Lambda Calculus

Le calcul Lambda est un cadre développé par Alonzo Church dans les années 1930 pour étudier les calculs avec des fonctions.

Function creation - L'Église a introduit la notation λx.Epour désigner une fonction dans laquelle «x» est un argument formel et «E» est le corps fonctionnel. Ces fonctions peuvent être sans noms et sans arguments.
Function application - Church a utilisé la notation E₁.E₂ pour désigner l'application de la fonction E₁ à l'argument réel E₂. Et toutes les fonctions sont sur un seul argument.

Syntaxe de Lambda Calculus

Le calcul Lamdba comprend trois types d'expressions différents, à savoir,

E :: = x (variables)

| E ₁ E ₂(application de fonction)

| λx.E (création de fonction)

Où λx.E est appelée abstraction Lambda et E est appelée expressions λ.

Le calcul lambda pur n'a pas de fonctions intégrées. Évaluons l'expression suivante -

(+ (* 5 6) (* 8 3))

Ici, on ne peut pas commencer par «+» car il ne fonctionne que sur les nombres. Il existe deux expressions réductibles: (* 5 6) et (* 8 3).

Nous pouvons d'abord réduire l'un ou l'autre. Par exemple -

(+ (* 5 6) (* 8 3)) 
(+ 30 (* 8 3)) 
(+ 30 24) 
= 54

Nous avons besoin d'une règle de réduction pour gérer les λs

(λx . * 2 x) 4 
(* 2 4) 
= 8

C'est ce qu'on appelle la β-réduction.

Le paramètre formel peut être utilisé plusieurs fois -

(λx . + x x) 4 
(+ 4 4) 
= 8

Lorsqu'il y a plusieurs termes, nous pouvons les gérer comme suit -

(λx . (λx . + (− x 1)) x 3) 9

L'intérieur x appartient à l'intérieur λ et le x extérieur appartient au x extérieur.

(λx . + (− x 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
= 11

Dans une expression, chaque apparence d'une variable est soit "libre" (à λ), soit "liée" (à un λ).

β-réduction de (λx . E) y remplace chaque x qui se produit gratuitement dans E avec y. Par exemple -

La réduction alpha est très simple et peut être effectuée sans changer la signification d'une expression lambda.

λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x)

Par exemple -

(λx . (λx . + (− x 1)) x 3) 9 
(λx . (λy . + (− y 1)) x 3) 9 
(λy . + (− y 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
11

Le théorème de Church-Rosser déclare ce qui suit:

Si E1 ↔ E2, alors il existe un E tel que E1 → E et E2 → E. «Une réduction de quelque manière que ce soit peut finalement produire le même résultat.»
Si E1 → E2, et E2 est de forme normale, alors il y a une réduction d'ordre normal de E1 en E2. "La réduction d'ordre normal produira toujours une forme normale, s'il en existe une."