Teoria della dimostrazione: lambda calcolo

Scuola Italiana di Logica 2005




English Version
Docente:Stefano Berardi ( http://www.di.unito.it/~stefano/ , stefano.berardi presso di.unito.it)
Testo del corso: disponibile in formato zipped ppt . Include gli esercizi del corso (al fondo). Le soluzioni degli esercizi sono disponibili in formato zipped ppt .

Obbiettivi formativi:
Il corso introduce il lambda calcolo come modello astratto della nozione di computazione e di prova costruttiva. Obbiettivo č rendere lo studente familiare con nozioni quali l'espansione di una definizione, l'unicitá del risultato, la completezza di una strategie di computazione, l'eguaglianza di programmi. Per una migliore comprensione del corso sono utili, ma non richiesti, i primi rudimenti di programmazione .

Programma del corso:

  • 1. Introduzione. Il lambda calcolo come modello per i linguaggi funzionali.
  • 2. Sintassi del lambda calcolo. alpha, beta-riduzioni. Forme normali, normalizzazione, normalizzazione forte. Strategie di calcolo call-by-name e call-by-value.
  • 3. Principali risultati teorici. Forma normale di testa, strategia di riduzione di testa e sinistra e relativi risultati di completezza. Teoremi: Confluenza e Church-Rosser. Teorie della beta-conversione. Ordine e eguaglianza osservazionale, termini solvable.
  • 4. Rappresentazione delle funzioni ricorsive. Numeri naturali e booleani nel lambda calcolo. Aritmetica sui numerali di Church. Funzioni ricorsive e minimo punto fisso.
  • 5. Lambda calcolo tipato semplice. Unificazione e isomorfismo di Curry-Howard tra lambda termini e prove costruttive.

    Ringraziamenti.
    Il corso é una espansione, immaginata esplicitamente per questa scuola estiva, del corso di Lambda Calcolo tenuto dal Prof. Barbanera all'universitá di Catania, per la laurea specialistica in Informatica. Il corso di Barbanera, piu'di base rispetto al nostro, e' disponibile in formato html , pdf, corredato di esercizi: es1, es2. L'ultima sezione del corso e' un adattamento di una lezione di Teoria dei tipi tenuta dal Prof. H. Geuvers nel 2002 (alla Scuola estiva di Logica e Teoria dei Tipi, Eugene, Oregon, USA).
    Ringraziamo caldamente il Prof. Barbanera e i suoi allievi e il Prof. Geuvers per aver fornito il materiale.

    Bibliografia

  • Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics. 2d ed. North-Holland, 1984.
  • Barendregt, H. 1992. Lambda Calculi with Types. In: Abramsky, G., & Maibaum (eds), Handbook of Logic in Computer Science, vol. II. Oxford University Press. http://citeseer.ist.psu.edu/barendregt92lambda.html

    Stefano Berardi