Isomorfismo di Curry-Howard

L'isomorfismo di Curry-Howard dà una corrispondenza fra programma e prova e fra tipo e formula. Permette di dare una equivalenza fra il fatto che esiste un programma P che ha il tipo T e il fatto che esiste una prova P' della formula T'.

ML

Il linguaggio di programmazione che consideriamo è un linguaggio della famiglia di ML (Caml, Ocaml, Mosml, Sml,...). Per i nostri esempi usiamo la sintassi di OCaml.

Tipo

Il linguaggio è tipato, quindi ogni oggetto ha un tipo. Ciò si scrive oggetto:tipo. Per esempio:

1: int
"a": string
(1,"a"): int*string

Funzioni

IL linguaggio ML è funzionale. Ciò vuol dire che le funzioni sono oggetti di prima classe. Si possono manipolare funzioni come un qualsiasi altro oggetto, come i numeri interi per esempio. Il tipo di una funzione si scrive usando una freccia fra il tipo di partenza della funzione verso il tipo d'arrivo. Per creare una funzione si usa la parola chiave fun. Per esempio:

(fun x -> x): int -> int

Si può usare una funzione facendo una applicazione (funzione argumento). Per esempio:

(fun f -> (fun x -> (f (x+1))+1)): (int->int)->int->int

Infine si può dare un nome ad una funzione usando il let:

let incr = fun x -> x+1

Adesso (incr 1) vale 2. Una sintassi piú frequente per la dichiarazione precedente è:

let incr x = x+1

Polimorfismo

Una funzione può avere un tipo generico usando il cosidetto polimorfismo. Per esempio,

let id = (fun x -> x)

definisce la funzione identità che si può applicare a tutti i tipi di oggetto. Ciò viene reso esplicito mettendo come prefisso al tipo il carattere '. Per esempio,

id: 'a -> 'a

vuole dire che l'identità prende un oggetto di un qualunque tipo e restituisce un oggetto dello stesso tipo.

Facciamo altri esempi:

let pair = (fun x -> (fun y -> (x,y)))

La funzione pair prende due oggetti e restituisce una coppia. Il tipo di pair è

pair: 'a -> 'b -> 'a*'b

let fst = (fun x -> match x with (a,b) -> a)

La funzione fst prende una coppia e restituisce il primo elemento. Il tipo di fst è

fst: 'a*'b -> 'a

let snd = (fun x -> match x with (a,b) -> b)

La funzione snd prende una coppia e restituisce il secondo elemento. Il tipo di snd è

snd: 'a*'b -> 'b

Esempi

Con le tre funzioni precedenti possiamo dare un primo esempio dell'isomorfismo di Curry-Howard. Supponiamo di voler costruire una funzione che scambia gli elementi in una coppia, ovvero il primo elemento diventa il secondo e viceversa. Una funzione possibile è la seguente:

let swap = (fun x -> (pair (snd x) (fst x)))

Usando i tipi di fst, snd e pair, si può dedurre il tipo di swap:

'a * 'b

¯snd

'b

'a * 'b

¯fst

'a

¯pair

'b * 'a

¯fun

('a * 'b) -> ('b * 'a)

Ciò è esattamente l'equivalente della prova: A ∧ B B A ∧ B A B ∧ A (A ∧ B) ⇒ (B ∧ A)

Con le tabelle di corrispondenza:

Tipo Formula

'a * 'b A ∧ B

'a -> 'b A ⇒ B

Funzione Regola

fst ∧ eliminazione 1

snd ∧ eliminazione 2

pair ∧ introduzione

fun ⇒ introduzione

Una prova di A ∧ B è dunque vista come una coppia costituita da una prova di A e da una prova di B.

Una prova di A ⇒ B è vista come una funzione che prende una prova di A e restituisce una prova di B. Adesso si può dare l'equivalente dell'eliminazione dell'implicazione:

A ⇒ B A B

Tale regola corrisponde all'applicazione: per avere una prova di B è sufficiente applicare alla funzione che prende una prova di A e restituisce una prova di B una prova di A.
In Caml, si scrive:

let app = fun f -> (fun x -> (f x))

Il tipo di questa funzione è ('a->'b)->'a->'b.

Adesso proviamo a trovare una prova di
((A ⇒ B) ∧ (C ⇒ D)) ⇒ ((A ∧ C) ⇒ (B ∧ D))

Usando l'isomorfismo ciò è equivalente a trovare un progamma che ha il tipo:
(('a -> b) * ('c -> 'd)) -> (('a * 'c) -> ('b * 'd))

Una possibilità è la seguente:

(fun x ->
  (fun y -> (pair ((fst x) (fst y)) ((snd x) (snd y)))))

La prova corrispondente è:

(A ⇒ B) ∧ (C ⇒ D) A ⇒ B A ∧ C A B (A ⇒ B) ∧ (C ⇒ D) C ⇒ D A ∧ C C D B ∧ D (A ∧ C) ⇒ (B ∧ D) ((A ⇒ B) ∧ (C ⇒ D)) ⇒ ((A ∧ C) ⇒ (B ∧ D))

Proviamo a dare una prova di
A ⇒ ((A ⇒ B) ⇒ B)

Vuole dire trovare una funzione di tipo 'a -> (('a -> 'b) -> 'b). Una possibilità è:

(fun x ->  (fun f -> (f x)))

che corrisponde a

A ⇒ B A B (A ⇒ B) ⇒ B A ⇒ ((A ⇒ B) ⇒ B)

Adesso proviamo a dare una prova di
(A ⇒ B) ⇒ A ⇒ B

Vuole dire trovare una funzione di tipo ('a -> b) -> 'a -> 'b. Una possibilità è:

(fun f ->  (fun x -> (f x)))

che corrisponde a

A ⇒ B A B A ⇒ B (A ⇒ B) ⇒ A ⇒ B

C'è una prova più semplice: A ⇒ B (A ⇒ B) ⇒ A ⇒ B

che corrisponde alla funzione identità:

(fun x -> x)

Ma il tipo di questa funzione è troppo generale 'a -> 'a. Per avere il tipo esatto, bisogna dare esplicitamente il tipo di x

(fun (x:'a->'b) -> x)

Disgiunzione

Per dare l'intuizione a che cosa corrisponde la disgiunzione, bisogna lavorare un po' in CAML. Le liste sono rappresentate come un pettine, :: è il costruttore che permette di aggiungere un elemento all'inizio di una lista e [] è la lista vuota. 1::2::nil rappresenta la lista con due elementi 1 e 2. Si scrive anche come [1;2]. Si possono creare liste di ogni tipo: [1;2] ha per tipo int list, ["a"; "b"] ha per tipo string list. Dunque i costruttori di lista sono polimorfici, ed abbiamo:

(fun x -> [x]): 'a ->'a list

Però una lista è monomorfica: tutti i suoi elementi sono dello stesso tipo. Dunque non si può creare una lista come [1;"a"]. Per avere qualcosa di simile in un linguaggio come CAML, bisogna creare degli incapsulatori (wrapper). Nel nostro caso ciò vuol dire creare un nuovo tipo sum:

type sum =
  Inl of int
| Inr of string

sum può essere visto con un tipo che permette di avere sia oggetti di tipo int che oggetti di tipo string.
Il tipo di Inl è int -> sum.
Il tipo di Inr è string -> sum.
La lista che non si poteva creare prima, adesso può essere rappresentata tramite la lista [(Inl 1); (Inr "a")] di tipo sum list.

Adesso abbiamo un tipo, ma come si scrivono delle funzioni su questo tipo? Si può usare una costruzione generica: supponendo di avere una funzione che prende un int e un'altra funzione di un tipo simile ma che prende un string, si può creare una funzione su sum:

let f_sum c f1 f2 =
  match c with
    Inl a -> (f1 a)
  | Inr a -> (f2 a)

Il tipo di tale funzione è sum-> (int -> 'a) -> (string -> 'a) -> 'a. Per esempio si può avere

let is_int_null i = (i = 0)
let is_string_null s = (s = "")
let is_sum_null c = f_sum c f1 f2
let rec is_list_null l = match l with
  [] -> true
| (a::l1) -> if (is_sum_null a) then (is_list_null l1) else false

L'ultima funzione verifica se una lista di sum è nulla, i.e. contiene solo 0 e "".

La costruzione che abbiamo fatto per i tipi int e string può essere fatta a partire da due tipi arbitrari usando il polimorfismo:

type ('a,'b) sum =
  Inl of 'a
| Inr of 'b

Il tipo di Inl è 'a -> ('a,'b) sum.
Il tipo di Inr è 'b -> ('a,'b) sum.
La definizione di f_sum non cambia ma adesso il suo tipo è ('a,'b) sum -> ('a -> 'c) -> ('b -> 'c) -> 'c.

Adesso possiamo aggiungere altre righe alle nostre tabelle:

Tipo Formula

'a * 'b A ∧ B

'a -> 'b A ⇒ B

('a,'b) sum A ∨ B

Funzione Regola

fst ∧ eliminazione 1

snd ∧ eliminazione 2

pair ∧ introduzione

fun ⇒ introduzione

app ⇒ eliminazione

Inl ∨ introduzione 1

Inr ∨ introduzione 2

L'interpretazione di una prova di A ∨ B è che è una prova di A o una prova di B.

Per convincersi della nuova corrispondenza consideriamo la funzione:

let swap_sum = (fun x -> f_sum x Inr Inl)

Il suo tipo è ('a,'b) sum -> ('b,'a) sum che corrisponde alla formula (A ∨ B) ⇒ (B ∨ A).
La prova corrisponde a A ∨ B A B ∨ A B B ∨ A B ∨ A

Falso

L'unica regola di falso è l'eliminazione: False A Il corrispondente in CAML sarebbe un tipo impossibile, cioé un tipo senza costruttore:

type False =

Non si può avere tale tipo in CAML. La regola d'eliminazione corrisponderebbe alla funzione

let f = (fun x -> match x with )

Non si potrebbe discutere sul valore di x, in qunto non esiste un costruttore. Dunque il tipo di tale funzione sarebbe False -> 'a.

Negazione

Si può definire la negazione in termini dell'implicazione e del falso. Si vede con le regole seguenti:

[A] . . False ¬A

che è equivalente a

[A] . . False A ⇒ False e

A ¬A False

che è equivalente a

A A ⇒ False False

Quantificatore universale

(P c) ∀x. (P x) Anche il corrispondente della quantificazione universale è una funzione. Consideriamo la regola d'introduzione: (P c) ∀x. (P x) Tale regola può essere descritta come segue: se abbiamo una prova di P c per un c arbitrario, vuole dire che possiamo costruire una funzione che, dato un x, dà una prova di (P x). Si può procedere nello stesso modo per l'eliminazione ∀x . (P x) [(P a)] . . B B Se abbiamo una funzione che prende un x e restituisce una prova di (P x), si può usare una prova di (P a) per qualunque a.

La differenza fra un'implicazione e una quantificazione universale è solo il fatto che l'attuale valore del parametro compare nel tipo risultato. Si parla di tipo dipendente.

Non è possibile costruire tale tipo in CAML. Per dare un'idea consideriamo la funzione:

let rec array n a = match n with
  0 -> []
| _ -> a:: (array (n-1) a)

Il suo tipo è int -> 'a -> 'a list. Applicando tale funzione con 0 e "a", il risultato è []. Con 1 e "a", il risultato è ["a"]. Con 2 e "a", il risultato è ["a";"a"]. Con i tipi dipendenti si potrebbe avere un tipo più preciso dicendo che la funzione prende due argomenti e restituisce una lista la cui lunghezza è uguale al valore del primo parametro. Dunque il tipo sarebbe qualcosa come ∀x:int. 'a -> 'a (list x) dove (list n) rappresenta il tipo delle liste di lunghezza n.

Laurent Théry

Last modified: Tue Jun 4 21:38:21 MEST 2002

Funzione	Regola
fst	∧ eliminazione 1
snd	∧ eliminazione 2
pair	∧ introduzione
fun	⇒ introduzione