title: Sistema F
text: # Sistema F
  
  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:
  
      $\vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha$
  
  dove α è una variabile di tipo. Il $\Lambda$ maiuscolo è usato per indicare una funzione parametrica rispetto alla variabile di tipo α, mentre il $\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: $\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. 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}\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 }.fx$
      2 := $\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)$
      3 := $\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))$
  
  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'$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.
  
  