UNIVERSITÀ DEGLI STUDI ROMA TRE FACOLTÀ DI S.M.F.N.

Sintesi della Tesi di Laurea in Matematica di

Giorgia Maffezzoli

Semantica Denotazionale: Tipi, Dimostrazioni,

Programmazione Funzionale

Relatore Correlatore

Prof. V. Michele Abrusci Prof. Marco Pedicini

ANNO ACCADEMICO 2002 - 2003 LUGLIO 2003

Classificazione AMS: 03B70, 03B40, 68Q55, 68N18, 03F50. Parole chiave: Semantica, Sistema T , Sistema F , tipi, funzioni.

Vista l’importanza dell’informatica ai nostri giorni, in questo lavoro, si è pensato di studiare la relazione che esiste tra la Logica e l’Informatica puntando la nostra attenzione sulla Semantica Denotazionale giungendo in conclusione alla Programmazione Funzionale.

La suddetta relazione viene formalizzata dalla Corrispondenza di Curry-Howard argomento del primo capitolo di questo lavoro.

La corrispondenza di Curry-Howard ha come oggetti di studio le Deduzioni Naturali. Le deduzioni naturali sono delle strutture ad albero lette dall’alto verso il basso. L’idea è che le foglie poste in alto sono le ipotesi da cui partiamo per giungere ad una dimostrazione dell’espressione che costituisce la radice di tale albero.

Viene quindi data una lista delle regole che stabiliscono il comportamento durante una deduzione. Da sottolineare è l’aspetto simmetrico delle regole, vedremo, infatti, che ad una regola di eliminazione ne corrisponde esattamente una di introduzione. Le deduzioni naturali possono dare origine a delle funzioni. Tali funzioni associano all’insieme delle ipotesi una possibile deduzione. In particolare diremo che una deduzione δ di una espressione A è un elemento dell’insieme delle possibili deduzioni di A, sciveremo quidi δ ∈ A invece di “δ è una dimostrazione di A”.

Nella nostra interpretazione le formule corrispondono ai tipi la cui definizione induttiva è:

1. I tipi atomici, al più numerabili ed indicati con T_{1}, …, T_{n}, sono tipi;

2. (Passo induttivo) Se U e V sono tipi, allora U × V e U → V sono tipi;

3. Gli unici tipi sono quelli ottenuti con le operazioni precedenti.

Questo corrisponde al segmento (∧, ⇒) del calcolo proposizionale dove le proposizioni atomiche sono indicate con T_{i}, “∧” diventa “×” e “⇒” diventa “→”.

Diremo che un termine di tipo A è una dimostrazione di una formula A.

La corrispondenza di Curry-Howard agisce nel seguente modo:

1. Le variabili x_{0}^{T} , …, x_{n}^{T}, … sono termini di tipo T.

2. Se u e v sono termini di tipo, rispettivamente, U e V, allora la coppia ⟨u, v⟩ è un termine di tipo U × V.

3. Se t è un termine di tipo U × V allora π^{1}t è un termine di tipo U e π^{2}t è di tipo V.

4. Se v è un termine di tipo V, la variabile x_{n}^{U} è di tipo U allora λx_{n}^{U}.v è un termine di tipo U → V.

Dove λ è una operazione di astrazione definita nel seguente modo: Se M ≡ M[x] è una espressione dipendente dalla variabile x allora λx.M[x] denota la mappa intuitiva

x ↦ M[x]

che ad x associa M[x]

5. Se t è un termine di tipo U → V ed u è di tipo U, allora tu è un termine di tipo V.

Con la giustapposizione di t ed u indichiamo l’operazione di applicazione dove t è considerato come un algoritmo applicato ad u e, quest’ultimo, è considerato come un input.

Si enuncia poi un teorema di normalizzazione che ci assicura la possibilità di ridurre un termine, in un numero finito di passi, in forma normale (Definizione 1.2.3).

Tale teorema sarà prima enunciato in una forma debole (Teorema 1.3.1)

Introdurremo poi un Calcolo dei Sequenti (Definizione 1.4.1)con delle regole simili a quelle date per le deduzioni naturali. Osserviamo che nel calcolo dei sequenti le regole saranno solo introduttive ma non saranno “uguali”.

In un sequente, infatti, abbiamo due parti: la prima costituisce l’insieme delle ipotesi mentre la seconda costituisce la tesi. Le regole saranno quindi distinte in due classi, una per l’introduzione nell’insieme delle ipotesi ed una per l’introduzione nella parte costituita dalla tesi.

Si conclude il primo capitolo con una dimostrazione del Teorema di Riducibilità 1.5.2 nel quale è affermata la riducibilità di tutti i termini.

Nel secondo capitolo inizieremo il nostro studio elencando alcune definizioni sulle funzioni ricorsive ed in particolare definendo la funzione di Ackermann (Paragrafo 2.1.2).

Tali funzioni vengono introdotte poiché l’idea principale è quella di prendere un sistema formale e vedere quali sono le funzioni in esso rappresentabili per vederne il potere espressivo.

Il sistema più semplice, da noi, introdotto è quello degli Assiomi di Peano per il quale si dimostra che solo un certo numero di funzioni è rappresentabile.

Passiamo quindi ad una definizione formale del Sistema T (Definizione 2.2.8). Gödel introdusse il sistema T per dimostrare la consistenza di PA , tradusse ogni formula dell’aritmetica in un’espressione circa i funzionali primitivi ricorsivi di tipo finito per mezzo della sua interpretazione Dialectica.

Tale sistema, dal punto di vista logico, non è un passo avanti bensì indietro, ma quello su cui vogliamo focalizzare la nostra attenzione in questo momento è il potere espressivo. Purtroppo, infatti, questi nuovi schemi non corrispondono a dimostrazioni in un sistema logico esteso. Un altro problema è che se si vuole migliorare l’espressività restando in questo sistema si perde in semplicità e modularità.

In conclusione si vede che le funzioni esprimibili in tale sistema sono quelle ricorsive primitive.

Passiamo poi al Sistema F definito in 2.2.3 (definizione 2.2.11). Daremo poi una rappresentazione per i tipi semplici definendo le operazioni di prodotto e somma ovvero congiunzione e disgiunzione. Vedremo la rappresentazione di una struttura libera introducendo il concetto di albero. Ed in conclusione daremo la rappresentazione per i tipi induttivi.

Nel terzo, ed ultimo, capitolo passiamo all’interpretazione dei sistemi sopra introdotti da un punto di vista legato all’informatica, alla programmazione funzionale.

Riassumiamo la Corrispondenza di Curry-Howard ed affermiamo il seguente principio:

Il valore di un’espressione dipende solo dai valori delle sue sottoespressioni, se ne esistono.

Tale principio è fondamentale per la programmazione funzionale. Diremo che un tipo è un insieme di valori con un insieme di operazioni e daremo una sintassi per le espressioni di tipo. In particolare daremo degli esempi di operazioni sulle liste vedendo la sintassi per la definizione di funzioni.

In 3.1 si passa al livello semantico dove definiremo la macchina di Krivine che è un esmpio di interprete per la semantica operazionale e ne studieremo l’azione sul termine

(λu.λw.(π^{2}u)((π^{1}u)w))⟨λx.x, λy.y⟩

di cui considereremo l’albero per la valutazione (3.1) ed una tabella (3.2) dove viene riportata la situazione degli stack ad ogni passo dell’analisi.

Vista la semantica operazionale presentiamo la semantica denotazionale associata ai sistemi T ed F . Per quanto riguarda il primo di tali sistemi daremo una interpretazione con delle proprietà. In particolare vedremo come interpretare i booleani e gli interi.

Il secondo dei due sistemi ha come semantica denotazionale associata gli Spazi Coerenti dove per Spazio Coerente intendiamo un insieme, di insiemi, 𝒜 che soddisfa:

1. Chiusura dal basso: se a ∈ 𝒜 e a′ ⊂ a, allora a′ ∈ 𝒜.

2. Completezza binaria: se M ⊂ 𝒜 e se ∀a_{1}, a_{2} ∈ M (a_{1} ∪ a_{2} ∈ 𝒜), allora ⋃ M ∈ 𝒜.

Ed abbiamo anche un oggetto indefinito: ∅ ∈ 𝒜.

Sugli spazi coerenti definiremo delle funzioni e daremo la definizione di funzione stabile (Definizione 3.1.3). Consideriamo il Prodotto Diretto tra spazi corenti nella definizione 3.1.4. Diremo inoltre che una funzione è univocamente determinata dalla sua Traccia (Definizione 3.1.6).

Concludiamo il lavoro con un’applicazione alla Finanza Matematica. Dopo un piccolo cenno alla finanza il nostro intento è quello di definire un elenco di combinatori in grado di generare nuovi contratti a partire da dei contratti base. Su tali combinatori daremo una semantica operazionale ed una denotazionale.

Bibliografia

[1] Lloyd Allison. A practical introduction to denotational semantics. Cambridge University Press, Cambridge, 1986. capp. 1 - 5.

[2] Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Cambridge University Press, Cambridge, 1989.

[3] Simon Peyton Jones, Jean-Marc Eber, and Julian Seward. Composing contracts: An adventure in financial engineering functional pearl. In Fifth ACM SIGPLAN(ICFP ’00), 2000.

[4] Ravi Sethi. Programming Languages. Addison-Wesley, 1997. Capp. 8, 9, 13.

[5] Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the curryhoward isomorphism. Available as DIKU Rapport 98/14, 1998.