Sistema F

Niente fonti!
Questa voce o sezione sull'argomento matematica non cita le fonti necessarie o quelle presenti sono insufficienti.

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.

Descrizione

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:

⊢ Λ α . λ x α . x : ∀ α . α → α {\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }

dove α è una variabile di tipo. Il Λ {\displaystyle \Lambda } maiuscolo è usato per indicare una funzione parametrica rispetto alla variabile di tipo α, mentre il λ {\displaystyle \lambda } minuscolo viene usato per indicare l'input di un termine x.

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

Il tipo Boolean è definito come segue: ∀ α . α → α → α {\displaystyle \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 := Λ α . λ x α λ y α . x {\displaystyle \Lambda \alpha .\lambda x^{\alpha }\lambda y^{\alpha }.x}
FALSE := Λ α . λ x α λ y α . y {\displaystyle \Lambda \alpha .\lambda x^{\alpha }\lambda y^{\alpha }.y}

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

AND := λ x B o o l e a n λ y B o o l e a n . ( ( x ( B o o l e a n ) ) y ) F A L S E {\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))y)FALSE}
OR := λ x B o o l e a n λ y B o o l e a n . ( ( x ( B o o l e a n ) ) T R U E ) y {\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))TRUE)y}
NOT := λ x B o o l e a n . ( ( x ( B o o l e a n ) ) F A L S E ) T R U E {\displaystyle \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 := Λ α . λ x B o o l e a n λ y α λ z α . ( ( x ( α ) ) y ) z {\displaystyle \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. n (λ x. FALSE) TRUE

Strutture del sistema F

Il sistema F permette alle costruzioni ricorsive di essere incluse in modo naturale.

Le strutture astratte (S) sono create usando i constructors. Essi sono funzioni tipate come segue:

K 1 → K 2 → ⋯ → S {\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S} .

La ricorsività diventa manifesta se S {\displaystyle S} stesso appare in uno dei tipi K i {\displaystyle K_{i}} . Se abbiamo m {\displaystyle m} di questi costruttori, possiamo definire un tipo di S {\displaystyle S} come segue:

∀ α . ( K 1 1 [ α / S ] → ⋯ → α ) ⋯ → ( K 1 m [ α / S ] → ⋯ → α ) → α {\displaystyle \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 {\displaystyle N} con costruttori

z e r o : N {\displaystyle {\mathit {zero}}:\mathrm {N} }
s u c c : N → N {\displaystyle {\mathit {succ}}:\mathrm {N} \to \mathrm {N} }

Nel sistema F il tipo corrispondente a questa struttura è ∀ α . α → ( α → α ) → α {\displaystyle \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 := Λ α . λ x α . λ f α → α . x {\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x}
1 := Λ α . λ x α . λ f α → α . f x {\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx}
2 := Λ α . λ x α . λ f α → α . f ( f x ) {\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)}
3 := Λ α . λ x α . λ f α → α . f ( f ( f x ) ) {\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))}

Se si inverte l'ordine degli argomenti (cioè, ∀ α . ( α → α ) → α → α {\displaystyle \forall \alpha .(\alpha \to \alpha )\to \alpha \to \alpha } ), allora il numerale di Church per n {\displaystyle n} è una funzione che ha una funzione f come argomento e ritorna l' n {\displaystyle n} esima 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.

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