Lambda-calcolo

Durata: 28 ore

Periodo didattico: primo semestre

Programma

Periodo didattico: da novembre

Settore disciplinare: INF/01

 

  • Primo modulo (Prof. Fabio Alessi), 10 ore.

 

  • Secondo modulo (Prof. Pietro Di Gianantonio), 9 ore.

 

  • Terzo modulo (Prof.ssa Marina Lenisa), 9 ore.

 

Il corso si propone di presentare un quadro sufficientemente completo del lambda calcolo considerandolo sotto differenti aspetti.  Si inizia mostrando come la computazione possa essere definita all'interno del lambda calcolo, per poi analizzare i diversi meccanismi di computazione e le teorie da loro indotte.  Infine vengono presentate le costruzioni di modelli per il lambda calcolo.

 Nel dettaglio gli argomenti affrontati sono i seguenti:  Sintassi del lambda calcolo. Alfa e beta regola.  Forme normali e riduzioni infinite. Il Teorema di Church-Rosser.  Codifica di Church dei numeri naturali. Sviluppo della teoria della calcolabilità all'interno del lambda calcolo.  Strategie di riduzione:  call by value, call by name. Semantica operazionale e semantica denotazionale.  Equivalenza osservazionale, adeguatezza e full-abstraction.

 


Elenco corsi 2013/2014