Programmazione Funzionale - Lambda Calculus
Lambda calcolo è un framework sviluppato da Alonzo Church negli anni '30 per studiare calcoli con funzioni.
Function creation - Church ha introdotto la notazione λx.Eper denotare una funzione in cui "x" è un argomento formale e "E" è il corpo funzionale. Queste funzioni possono essere senza nomi e singoli argomenti.
Function application - Church ha usato la notazione E1.E2 per denotare l'applicazione della funzione E1 all'argomento effettivo E2. E tutte le funzioni sono su un singolo argomento.
Sintassi del Lambda Calculus
Il calcolo di Lamdba include tre diversi tipi di espressioni, ovvero
E :: = x (variabili)
| E 1 E 2 (funzione applicazione)
| λx.E (creazione della funzione)
Dove λx.E si chiama astrazione Lambda e E è noto come espressioni λ.
Valutazione del Lambda Calculus
Il lambda calcolo puro non ha funzioni integrate. Valutiamo la seguente espressione:
(+ (* 5 6) (* 8 3))
Qui, non possiamo iniziare con "+" perché funziona solo sui numeri. Esistono due espressioni riducibili: (* 5 6) e (* 8 3).
Possiamo prima ridurre uno dei due. Ad esempio:
(+ (* 5 6) (* 8 3))
(+ 30 (* 8 3))
(+ 30 24)
= 54
Regola β-riduzione
Abbiamo bisogno di una regola di riduzione per gestire λs
(λx . * 2 x) 4
(* 2 4)
= 8
Questa è chiamata β-riduzione.
Il parametro formale può essere utilizzato più volte:
(λx . + x x) 4
(+ 4 4)
= 8
Quando ci sono più termini, possiamo gestirli come segue:
(λx . (λx . + (− x 1)) x 3) 9
L'interno x appartiene all'interiore λ e la x esterna appartiene a quella esterna.
(λx . + (− x 1)) 9 3
+ (− 9 1) 3
+ 8 3
= 11
Variabili libere e vincolate
In un'espressione, ogni aspetto di una variabile è "libero" (a λ) o "vincolato" (a λ).
β-riduzione di (λx . E) y sostituisce ogni x che si verifica gratuitamente in E con y. Ad esempio -
Riduzione alfa
La riduzione alfa è molto semplice e può essere eseguita senza modificare il significato di un'espressione lambda.
λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x)
Ad esempio:
(λ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
Teorema di Church-Rosser
Il teorema di Church-Rosser afferma quanto segue:
Se E1 ↔ E2, allora esiste una E tale che E1 → E ed E2 → E. "La riduzione in qualsiasi modo può eventualmente produrre lo stesso risultato."
Se E1 → E2 ed E2 è la forma normale, allora c'è una riduzione di ordine normale da E1 a E2. "La riduzione dell'ordine normale produrrà sempre una forma normale, se esiste."