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."