Sistema F

Da Wikipedia, l'enciclopedia libera.

Il Sistema F, anche conosciuto come lambda calcolo polimorfico o lambda calcolo di secondo ordine, è un lambda calcolo tipizzato. È stato scoperto indipendentemente dal logico Jean-Yves Girard e dall'informatico John C. Reynolds. Il Sistema F formalizza la nozione di polimorfismo parametrico nei linguaggi di programmazione e pone le basi per linguaggi come Haskell, ML, e F#. Come sistema di riscrittura di termini, è fortemente normalizzante.

Come il lambda calcolo è composto da variabili sulle funzioni e relativi binder, così il lambda calcolo di secondo ordine ha variabili sui tipi e relativi binder.

Ad esempio, il fatto che la funzione identità può essere di qualunque tipo della forma A→ A può essere formalizzato nel sistema F come segue:

\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha

dove α è una variabile di tipo. Il \Lambda maiuscolo è usato tradizionalmente per indicare funzioni a livello di tipi, mentre il \lambda minuscolo viene usato per le funzioni a livello di valori.

Sotto l'isomorfismo di Curry-Howard, il Sistema F corrisponde a una logica proposizionale di secondo ordine.

Il Sistema F può essere visto come parte del lambda cubo, insieme ad altri lambda calcoli tipati più espressivi, inclusi quelli con solo tipi dipendenti.

Logica e predicati[modifica | modifica wikitesto]

Il tipo Boolean è definito come segue: \forall\alpha.\alpha \to \alpha \to \alpha, dove α è una variabile di tipo. Questo produce le seguenti due definizioni per i valori booleani TRUE e FALSE:

TRUE := \Lambda \alpha.\lambda x^\alpha \lambda y^\alpha.x
FALSE := \Lambda \alpha.\lambda x^\alpha \lambda y^\alpha.y

Così, con questi due λ-termini, possiamo definire alcuni operatori logici:

AND := \lambda x^{Boolean} \lambda y^{Boolean}.((x (Boolean)) y) FALSE
OR := \lambda x^{Boolean} \lambda y^{Boolean}.((x (Boolean)) TRUE) y
NOT := \lambda x^{Boolean}. ((x (Boolean)) FALSE) TRUE

Non c'è un vero bisogno di una funzione IFTHENELSE visto che si possono usare direttamente i termini grezzi di tipo booleano come funzioni di decisione. Comunque, se necessario:

IFTHENELSE := \Lambda \alpha.\lambda x^{Boolean}\lambda y^{\alpha}\lambda z^{\alpha}.((x (\alpha)) y) z

soddisfa tale necessità. Un predicato è una funzione che ritorna un valore booleano. Uno dei predicati fondamentali è ISZERO che ritorna TRUE se e solo se il suo argomento è il numerale di Church 0:

ISZERO := λ n. nx. FALSE) TRUE

Strutture del Sistema F[modifica | modifica wikitesto]

Il sistema F permette alle costruzioni ricorsive di essere incluse in modo naturale, secondo la teoria dei tipi di Martin-Löf. Le strutture astratte (S) sono create usando i constructors. Essi sono funzioni tipate come segue:

K_1\rightarrow K_2\rightarrow\dots\rightarrow S.

La ricorsività diventa manifesta se S stesso appare in uno dei tipi K_i. Se abbiamo m di questi costruttori, possiamo definire un tipo di S come segue:

\forall \alpha.(K_1^1[\alpha/S]\rightarrow\dots\rightarrow \alpha)\dots\rightarrow(K_1^m[\alpha/S]\rightarrow\dots\rightarrow \alpha)\rightarrow \alpha

Ad esempio, i numeri naturali possono essere definiti come un tipo di dato induttivo N con costruttori

\mathit{zero} : \mathrm{N}
\mathit{succ} : \mathrm{N}\to\mathrm{N}

Nel Sistema F il tipo corrispondente a questa struttura è \forall \alpha. \alpha \to (\alpha \to \alpha) \to \alpha. I termini di questo tipo costituiscono una versione tipata dei numerali di Church, i primi dei quali sono:

0 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . x
1 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f x
2 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f x)
3 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f (f x))

Se si inverte l'ordine degli argomenti (cioè, \forall\alpha.(\alpha\to\alpha)\to\alpha\to\alpha), allora il numerale di Church per n è una funzione che ha una funzione f come argomento e ritorna l'nesima potenza di f. Ciò vuol dire che un numerale di Church è una funzione di ordine superiore -- che prende una funzione con un solo argomento f e ritorna un'altra funzione con un singolo argomento.

matematica Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica