2015-06-25 20:26:55 +02:00

22 KiB

Raw Permalink Blame History

Interessanti applicazioni: il $\lambda$-calcolo

Il lambda calcolo o $\lambda$-calcolo è un sistema formale inventato dal matematico e logico americano Alonzo Church negli anni '30 che formalizza le computazioni di funzioni.

Il problema della decisione

Questo sistema formale fu introdotto per risolvere un altro problema proposto da Hilbert nel suo programma: il cosiddetto Entscheidungsproblem o problema della decisione. Il problema è il seguente:

Esiste un algoritmo, un metodo completamente meccanico, per verificare se una qualunque stringa di un sistema formale è un teorema in quel sistema?

La risposta fu fornita indipendentemente da Church e Alan Turing nel 1936 e fu un deciso no. Church ci arrivò proprio tramite questo sistema formale mentre Turing attraverso un modello ideale di macchina che oggi è noto come macchina di Turing. Nello stesso anno poi Turing dimostrò che i sistemi da loro inventati erano equivalenti: cioè sono ugualmente potenti perché possono calcolare la stessa classe di funzioni.

Il lambda calcolo e le macchine di Turing rendono formale la nozione intuitiva di calcolabile e decidibile che sono fondamentali per risolvere il problema.

Oggi

I computer moderni sono tuttora basati sul modello delle macchine di Turing e così anche i linguaggi di programmazione imperativi basati sul modo in cui si forniscono istruzioni a tali macchine.

Linguaggi funzionali

Esiste tuttavia un'altra classe di linguaggi di programmazione i cosiddetti linguaggi funzionali che sono invece basati sul lambda calcolo. A differenza dei programmi imperativi che sono un elenco di istruzioni i programmi funzionali consistono di una singola espressione che contiene sia l'algoritmo che il suo input. Quest'espressione, tramite l'applicazione di regole, è ridotta più volte fino ad ottenere il risultato del programma. La riduzione consiste nel sostituire una parte dell'espressione con una più semplice come facciamo in matematica. Per esempio:

 
\begin{aligned}
    (1+2)\times(4\times 3) &\rightarrow 3\times (4\times 3) \\
                           &\rightarrow 3\times 12          \\
                           &\rightarrow 36                  \\
\end{aligned}

Partendo dall'espressione E otteniamo alla fine l'espressione E^* detta forma normale, ovvero il risultato. Il lambda calcolo fa esattamente questo.

Definizione

Vediamo ora la definizione del sistema formale.

Simboli

I simboli usati sono

la lettera \lambda
il punto .
le parentesi tonde ()
un insieme di lettere per le variabili

Lambda termini

Le espressioni (formule) ben formate del $\lambda$-calcolo si chiamano $\lambda$-termini.

I seguenti sono $\lambda$-termini:

variabili: si chiamano variabili tutti i simboli come x, y, z, \cdots
applicazione: si dice applicazione (t\ s) dove s e t sono $\lambda$-termini.
$\lambda$-astrazione si dice $\lambda$-astrazione \lambda v.t dove t è un $\lambda$-termine e v una variabile.

Alcuni esempi di termini:

 (x\ y)

 (\lambda x.(x\ y))

Per comodità userò operatori come \times, +, -, numeri e alcune metasintassi ma ricordiamoci che essi non fanno parte del sistema formale.

Applicazione

La prima operazione di base del $\lambda$-calcolo è l'applicazione: Se F è un algoritmo e A dei dati, indichiamo l'applicazione di F al valore A con:

F\ A

Con applicazione si può intendere sia il risultato dell'algoritmo sia il processo stesso di applicazione. Poiché il lambda calcolo non definisce i tipi possiamo anche applicare F a se stesso (per fare una ricorsione per esempio) così:

F\ F

Un esempio di applicazione è

(\lambda x.x+2)2 \rightarrow 4

dove abbiamo applicato la $\lambda$-espressione (\lambda x.x+2) al valore 2 e ottenuto 4.

Astrazione

Un'altra operazione è l'astrazione: Se F[x] è un espressione che contiene la variabile x: \lambda x.F[x] è un'espressione che denota la funzione x \mapsto F[x].

Quando applichiamo un valore ad un'astrazione facciamo una sostituzione:

(\lambda x.F[x])A è uguale a F[A], scritto anche come:

(\lambda x.F[x])D = F[x:=D]

dove F[x:=D] indica il $\lambda$-termine ottenuto sostituendo tutte le occorrenze di x con D.

Un'astrazione quindi è la definizione di una funzione che non ha un nome specifico. Infatti vengono a volte chiamate funzioni anonime.

Variabili libere e legate

In un'espressione le variabili possono essere legate o libere. Per esempio in \lambda x.(y\ x) y è libera mentre x è legata. Le variabili libere possono quindi essere legate da una $\lambda$-astrazione con il simbolo \lambda.

Quando applichiamo un valore facendo una sostituzione [x:=D] in un'astrazione questa avviene solo dove x è libera. Esattamente come quando abbiamo una funzione integrale tipo F(x)=\int_0 ^x f(x)dx e calcoliamo un suo valore come F(3)=\int_0 ^3 f(x)dx.

Per esempio:


\begin{aligned}
F[y] = \lambda y.(\lambda y.y\ y)  &&F[y:=3] = (\lambda y.y\ 3)
\end{aligned}

Se un $\lambda$-termine non contiene variabili libere si che è un combinatore o termine chiuso.

Applicazione parziale

Abbiamo visto che con la $\lambda$-astrazione possiamo produrre funzioni che accettano un parametro. Spesso però abbiamo la necessità di avere funzioni con argomenti multipli come f(x,y,z) Si può rappresentare queste funzioni usando un metodo noto come applicazione parziale o currying, dal matematico Haskell Curry che lo utilizzò per primo.

Una funzione di più argomenti è rappresentata come una catena di funzioni in cui ciascuna genera a sua volta una funzione di un singolo argomento.

Per esempio la funzione f(x,y,z)=x\times y+z viene così definita:


\lambda x.\lambda y.\lambda z.(x\times y+z)

Se vogliamo calcolare f(2,3,5):

applichiamo la prima volta 2 e otteniamo la funzione \lambda y.\lambda z.(2\times y+z)
applichiamo la seconda volta 3 e otteniamo la funzione \lambda z.(2\times 3+z)
applichiamo infine 5 e otteniamo il risultato (2\times 3+5) \rightarrow 11

complessivamente f(2,3,5) = (((\lambda x.\lambda y.\lambda z.(x\times y+z)\ 2)\ 3)\ 5)

Regole

Vediamo ora le regole per ridurre o convertire una $\lambda$-espressione.

$\alpha$-conversione

L'$\alpha$-conversione è una regola che permette di sostituire le variabili legate in un $\lambda$-termine, cioè rinominarle. I $\lambda$-termini ottenuti con questa conversione si dicono tra loro $\alpha$-equivalenti. L'$\alpha$-conversione è una sostituzione del tipo F[u:=v] dove u è una variabile legate e v una variabile qualsiasi.

Per esempio \lambda x.x \rightarrow_\alpha \lambda z.z.

Non è sempre possibile effettuare un $\alpha$-conversione. Per esempio non è possibile fare la sostituzione (\lambda y.\lambda x.y)[y:=x]. Infatti \lambda x.\lambda x.x è un $\lambda$-termine completamente diverso.

$\beta$-riduzione

La $\beta$-riduzione è un'applicazione del tipo (\lambda x.M)N dove M e N sono dei $\lambda$-termini. Si può calcolare come una sostituzione M[x:=N].

(\lambda x.M)N si dice $\beta$-redex e M[x:=N] la sua $\beta$-contrazione. La riduzione si indica con g \rightarrow_\beta g' e si legge "g riduce a $g'$".

Per esempio (\lambda x.x^3-1)3 \rightarrow_\beta 10

$\eta$-conversione

Quando abbiamo un $\lambda$-termine del tipo (\lambda x.M\ x) l'$\eta$-conversione ci permette di rimuovere la $\lambda$-astrazione se x non appare libera in M. I termini prodotti si dicono $\eta$-equivalenti e la conversione si indica con g \rightarrow_\eta g'.

Per esempio \lambda y. \lambda x.y\ x \rightarrow_\eta \lambda y.y

In 2 righe

Utilizzando la metasintassi di Backus-Naur possiamo riassumere la sintassi e la semantica del $\lambda$-calcolo in appena 2 righe:

L ::= v\ |\ \lambda v.L\ |\ (L\ L)

(\lambda v.L_\beta)L_\alpha \rightarrow L_\beta[v:=L_\alpha]

Utilità

Vediamo ora che abbiamo definito il sistema cosa ci permette di fare.

Aritmetica

Il $\lambda$-calcolo calcolo contiene l'aritmetica di Peano. È possibile rappresentare i numeri naturali tramite i numerali di Church così definiti:

\lambda y. \lambda x.x
\lambda y. \lambda x. y\ x
\lambda y. \lambda x. y\ (y\ x)
\lambda y. \lambda x. y\ (y\ (y\ x))
\cdots

I numerali di Church sono funzioni di ordine maggiore: una funzione che accetta una funzione come parametro e ne genera un'altra. In particolare l'$n$-esimo numerale prende una funzione y e la applica n volte a se stessa.

La funzione successore è definita come:

\text{succ} := \lambda n.\lambda y.\lambda x.y (n\ y\ x)

succ semplicemente prende come argomento un numerale n a cui applica nuovamente la funzione y per ottenere n+1.

È altrettanto semplice definire le operazioni aritmetiche. Per esempio:


\begin{aligned}
    \text{mult} &:= \lambda m.\lambda n.m\ \text{succ}\ n \\
    \text{plus} &:= \lambda m.\lambda n.\lambda y.m\ (n\ y)
\end{aligned}

Logica booleana

I valori di vero e falso sono rappresentati per convenzione tramite i booleani di Church:


\begin{aligned}
    T := &\lambda x.\lambda y.x && \text{(vero)} \\
    F := &\lambda x.\lambda y.y && \text{(falso)}
\end{aligned}

È poi possibile formulare gli operatori logici così:


\begin{aligned}
    \text{and}  &:= \lambda p.\lambda q.p\ q\ p            \\
    \text{or}   &:= \lambda p.\lambda q.p\ p\ q            \\
    \text{not}  &:= \lambda p.\lambda a.\lambda b.p\ b\ a  \\
\end{aligned}

Un esempio di uso:


\begin{aligned}
    \text{and}\ T\ F & \rightarrow (\lambda p.\lambda q.p\ q\ p)\ T\ F   \\
                     & \rightarrow (T\ F)\ T                             \\
                     & \rightarrow (\lambda x.\lambda y.x\ F)\ T         \\
                     & \rightarrow \lambda x.\lambda y.y                 \\
                     & \rightarrow F                                     \\
\end{aligned}

Ricorsione anonima

Una funzione ricorsiva essenzialmente è una funzione che nella sua definizione contiene se stessa. L'esempio più semplice è la funzione fattoriale n! = 1\cdot 2\cdot 3\dots (n-1)\cdot n che può essere così definita:


n! =
\begin{cases}
    1            & x = 0            \\
    n\cdot(n-1)! & \text{altrimenti}
\end{cases}

È fondamentale quindi che la funzione abbia un nome associato. Nel $\lambda$-calcolo nonostante le astrazioni siano anonime e quindi non possono riferirsi tramite un nome è possibile ottenere lo stesso risultato. Per fare ciò usiamo il combinatore $Y$

Il combinatore Y, o di punto fisso, è una qualunque funzione di ordine maggiore che soddisfa la relazione y\ f=f\ (y\ f) per qualunque f. Per esempio il combinatore di Curry è di punto fisso:


Y := \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f\ (x x))

Possiamo dimostrare che vale la relazione del combinatore Y tramite riduzione:


\begin{aligned}
    Y\ g &= \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f\ (x\ x))\ g     && \text {per definizione}        \\
         &\rightarrow_\beta (\lambda x.g(x\ x))\ (\lambda x.g\ (x\ x))  && \text {applicazione di $Y$ a $g$} \\
         &\rightarrow_\beta g(\lambda x.g(x\ x))\ (\lambda x.g\ (x\ x)) && \text {applicazione del primo termine} \\
         &= g\ (Y\ g)                                                   && \text {uguaglianza al secondo passaggio}          \\
\end{aligned}

Continuando ad applicare l'uguaglianza si ottiene:

g\ (Y\ g) = g\ (g\ (Y\ g)) = g\ (g\ (g\ (Y\ g))) = g\ (\dots(Y\ g)\dots)

Quindi il combinatore Y continua ad applicare la funzione argomento e questo ci permette di scrivere una funzione ricorsiva tramite una $\lambda$-astrazione senza la necessità di darle un nome.

Torniamo al nostro fattoriale: scriviamo subito la definizione di fattoriale nel modo classico:


\text{fact} := \lambda n.(\text{if } n=0 \text{ then } 1 \text{ else } n\times \text{fact } (n-1))

invece di chiamare fact usiamo una funzione f tramite la $\lambda$-astrazione \lambda f.:


\lambda f.\lambda n.(\text{if } n=0 \text{ then } 1 \text{ else } n\times f\ (n-1))

infine applichiamo Y all'espressione per ottenere:


\text{fact} := Y\ (\lambda f.\lambda n.(\text{if } n=0 \text{ then } 1 \text{ else } n\times f\ (n-1)))

In modo più formale usiamo i combinatori standard del lambda calcolo:


\text{fact} := Y\ (\lambda f.\lambda n.(\text{isZero }n)\ 1\ (\text{mult }n\ (f\ (\text{pred }n))))

Turing-equivalenza

Con la capacità di esprimere l'aritmetica, la logica ed infine anche la ricorsione il $\lambda$-calcolo è diventato Turing-equivalente: può compiere qualunque operazione una macchina di Turing sia in grado di svolgere. Secondo la tesi di Church-Turing cioè può calcolare qualsiasi funzione intuitivamente calcolabile. È sicuramente sorprendente per un sistema che si può descrivere in solo due righe. Per accorgersi di quanto è semplice e potente basta fare un confronto con TNT che per poter esprimere ogni proprietà dei numeri necessita di ben 7 regole di inferenza, 5 assiomi ed ingloba un intero sistema formale a parte (il calcolo proposizionale).

$\lambda$-calcolo tipizzato

La versione che abbiamo visto del $\lambda$-calcolo è senza tipi: cioè non ci sono limitazioni su cosa si può applicare a qualunque espressione. I termini possono persino essere applicati a se stessi. Questo permette una grande capacità di espressione ma porta agli stessi problemi individuati da Russell nella teoria naive degli insiemi. Per esempio il combinatore Y che abbiamo utilizzato per la ricorsione può essere utilizzato per produrre un paradosso (paradosso di Curry) che permette di derivare qualsiasi $\lambda$-termine. Lo stesso paradosso di Russel è presente in questa formulazione.

Questo si può risolvere introducendo una teoria dei tipi nel $\lambda$-calcolo, esattamento quello che ha fatto Russel in Principia mathematica.

Tipi

Diciamo che \mathcal{G} sia l'insieme dei tipi primitivi. Sono tipi:

ogni A \in \mathcal{G}
A \to B dove A e B sono tipi

Pre-termini

Modifichiamo la definizione precedente di termine per inserire i tipi:

I seguenti sono pre-termini:

variabili: si chiamano variabili tutti i simboli come x, y, z, \cdots
applicazione: si dice applicazione (t\ s) dove s e t sono pre-termini.
$\lambda$-astrazione si dice $\lambda$-astrazione \lambda v^A.t dove t è un pre-termine, v una variabile e A è un tipo.

Test

Per confermare che un pre-termine sia un termine dobbiamo verificare che tutte le variabili presenti in esso abbiano i tipi corretti. Un test ha la seguente forma:


\underbrace{x_1: A_1, x_2: A_2, \dots, x_n:A_n}_\text{contesto} \vdash \underbrace{M: A}_\text{termine}

dove:

x_1, x_2, \dots, x_n sono variabili presenti in M
A_1, A_2, \dots, A_n sono tipi
M è un pre-termine

Se il tipo di ogni variabile in M è confermato allora il test è passato e M è un $\lambda$-termine. Il processo con cui si determina il tipo delle variabili nel termine e se il tipo A esiste si chiama type inference e l'insieme di regole che definiscono i tipi e come si assegnano ai termini si chiama type system.

L'assegnazione di tipi ai termini potrebbe sembrare un inutile complicazione e una limitazione ma rende impossibile la produzione di espressioni prive di significato e spesso evita di fare errori durante l'applicazione e la riduzione ma la cosa più importante è che è possibile fare una formulazione del lambda calcolo in non esistono problemi indecidibili.

Haskell

Haskell, che prende il nome da Haskell Curry, è un linguaggio di programmazione puramente funzionale staticamente tipizzato che si basa sulla teoria delle categorie e proprio sul $\lambda$-calcolo tipizzato. Il programma stesso utilizzato per generare questo documento è scritto interamente in haskell così come i vari programmi da me scritti allegati alla tesi.

Haskell usa un particolare type system noto come Hindley–Milner usato anche da altri linguaggi funzionali. HM permette di dedurre il tipo di ogni espressione anche in assenza di qualunque annotazione dei tipi e lo fa in tempo quasi-lineare rispetto alla dimensione del programma. Consente inoltre tipi polimorfici e funzioni di ordine maggiore.

Un programma in haskell è un'espressione costituita da una o più definizioni di funzioni e costanti. Essendo puramente funzionale le funzioni sono funzioni matematiche: un'associazione di un valore ad un altro valore. Non è possibile che fornendo lo stesso dato la funzioni produca risultati diversi nel tempo, né che la sua esecuzione possa modificare lo stato del programma o di altre funzioni (side effects). Non esistono stati variabili: tutte le strutture dati sono immutabili. Se è necessario fare delle modifiche semplicemente se ne producono di nuove.

Questa descrizione dà un idea di un linguaggio fortemente limitato ma in realtà le sue caratteristiche funzionali forniscono degli enormi vantaggi:

Non essendoci possibili stati mutabili o side effects non possono esistere problemi dovuti all'accesso concorrente alla memoria. L'intero programma è thread-safe.
La gestione della memoria è basata sul garbage collecting ma a differenza di altri linguaggi l'immutabilità delle strutture rende il processo di cancellazione dei dati deferenziati estremamente semplice e rapido.
I risultati dell'applicazione di funzioni vengono calcolati solo quando necessario lazy evaluation. Questo permette di creare strutture dati infinite Per esempio fib = 0 : scanl (+) 1 fib{.haskell} è lista infinita di tutti i numeri di Fibonacci.
Anche quando non si vuole ragionare sui tipi il compilatore è in grado dedurli da sé e impedisce di fare errori in ogni caso. Con il type system di haskell è impossibile produrre un programma che compili ma che produca degli errori in runtime se non volutamente.
Per l'isomorfismo di Curry-Howard un programma haskell type checked è analogo ad una dimostrazione formale. Il type system può essere perciò usato per controllare la validità di una dimostrazione matematica.
Lo stile funzionale e il pattern matching sono molto espressivi e solitamente un programma è molto più conciso della controparte imperativa.

Esempi di programma

Game of Life

Un'implementazione del Game of Life di John Conway su una griglia rettangolare

import Control.Applicative
import Data.List  ((\\))
import Data.Maybe (fromMaybe)
import Matrix

type Cell = Int
type Grid = Mat Cell

(!) :: Grid -> Pos -> Cell
(Mat g) ! (x, y) = fromMaybe 0 (g ?? y >>= (?? x))

near :: Grid -> Pos -> [Cell]
near g (x, y) = map state $ neighbours \\ [(0,0)]
  where
    neighbours = liftA2 (,) [-1..1] [-1..1]
    state (x', y') = g ! (x+x', y+y')

alive :: Grid -> Pos -> Cell
alive g p
  | v == 0 &&  n == 3            = 1
  | v == 1 && (n == 2 || n == 3) = 1
  | otherwise                    = 0
  where (n, v) = (sum (near g p), g ! p)

next :: Grid -> Grid
next g = alive g <$> indeces g

main :: IO ()
main = mapM_ print (iterate next grid)

grid = Mat
  [ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
  , [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0]
  , [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0]
  , [0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0]
  , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
  , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
  , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

RPN

Un programma che risolve espressioni in notazione polacca inversa