Approfondire gli aspetti matematici del concetto di computazione, lo studio delle relazioni tra diversi modelli di calcolo e la complessità computazionale.
Curriculum
scheda docente materiale didattico
- Introduzione ai problemi di decisione, procedure algoritmiche e non algoritmiche, computazioni deterministiche, procedure discrete, nozione di alfabeto, di parola. Decidibilità e semidecidibilità di un insieme. Computazioni deterministiche, finitarie e discrete. Algoritmi formali: definizione formale di algoritmo, configurazioni di input, di output, funzione di transizione. Esempio di formalizzazione di un algoritmo. Decidibilità per automa finito. Rappresentazione degli automi mediante matrici. Monoide libero delle parole. Semianelli formali. Automi Finiti Non-deterministici. Linguaggi Regolari. Equivalenza tra automi deterministici e quelli non-deterministici.
- Macchine di Turing: definizione, decidibilità per macchina di Turing, tempo di arresto, spazio di arresto. Costo della computazione. Complessità: caso peggiore e caso medio. Indipendenza del tempo di decisione da un numero finito di configurazioni di input. Funzioni di complessità, classi di complessità DTIME e DSPACE (deterministic time e space). Inclusione DTIME(T (n)) ⊂ DSPACE(T(n)) ⊂ DTIME(2^{cT(n)}). Pumping Lemma per gli insiemi decidibili in tempo lineare. Simulazione di algoritmi, simulazione della macchina di Turing a seminastro, simulazione di una macchina multinastro. Macchine di Turing speciali. Teorema di Speedup lineare per macchine di Turing con alfabeto esteso. Valutazione del coefficente di accelerazione in relazione agli alfabeti. Decidibilità di insiemi di numeri naturali. Indipendenza dalla rappresentazione. Considerazioni sulla complessità.
- Turing calcolabilità: definizione di funzione Turing calcolabile, funzioni caratteristiche di insiemi Turing decidibili, la classe delle funzioni Turing calcolabili è chiusa per composizione, coppia, ricorsione primitiva e minimizzazione. Esempi di funzioni Turing calcolabili. Funzioni Ricorsive: equivalenza tra Turing computabilità e funzioni ricorsive. Funzione di Ackermann ([1] capp. 1,2,3,4,5 e [4] cap. 1).
- Funzioni costruibili in tempo. Nozione di T-orologio. Esempi di alcune funzioni costruibili in tempo. Chiusura per composizione.
- Macchine di Turing non-deterministiche: caratterizzazione mediante la decidibilità di insiemi proiezione. Definizione della classe delle funzioni non-deterministiche polinomiali. Problemi NP-completi.
2) Lambda calcolo e programmazione funzionale:
- Programmazione dichiarativa: cenni storici sul lambda calcolo, definizioni di base, i termini del lambda calcolo, la sostituzione semplice. Relazioni sui lambda termini. Congruenze, passaggio al contesto. α-equivalenza. L’α-equivalenza passa al contesto. Chiusura transitiva di una relazione, proprietà di Church-Rosser. Quozientamento dei lambda-termini rispetto all’alpha equivalenza.
- Definizione di beta-redesso e di beta-riduzione. Teorema di Church-Rosser per la beta-riduzione. Forme normali per beta-riduzione. Strategie di beta-riduzione. Strategia normalizzante: riduzione di sinistra (left most-outer most). Riduzione di testa. Termini Risolubili. Forme Normali di Testa. Teorema di caratterizzazione della risolubilità.
- Rappresentazione delle funzioni ricorsive: teorema di lambda definibilità. Esistenza del punto fisso per il lambda termini. Punto Fisso di Church ed punto fisso di Curry.
- Rappresentazione di altri tipi di dato nel lambda-calcolo: coppie, liste, alberi, soluzione di equazioni ricorsive su lambda-termini ([2] capp. 1, 2, 5).
[2] KRIVINE, J.-L., LAMBDA CALCULUS: TYPES AND MODELS. ELLIS HORWOOD, (1993).
[3] SIPSER,M., INTRODUCTION TO THE THEORY OF COMPUTATION.THOMSON COURSE TECHNOLOGY, (2006).
Programma
1) Computabilità, complessità e rappresentabilità:- Introduzione ai problemi di decisione, procedure algoritmiche e non algoritmiche, computazioni deterministiche, procedure discrete, nozione di alfabeto, di parola. Decidibilità e semidecidibilità di un insieme. Computazioni deterministiche, finitarie e discrete. Algoritmi formali: definizione formale di algoritmo, configurazioni di input, di output, funzione di transizione. Esempio di formalizzazione di un algoritmo. Decidibilità per automa finito. Rappresentazione degli automi mediante matrici. Monoide libero delle parole. Semianelli formali. Automi Finiti Non-deterministici. Linguaggi Regolari. Equivalenza tra automi deterministici e quelli non-deterministici.
- Macchine di Turing: definizione, decidibilità per macchina di Turing, tempo di arresto, spazio di arresto. Costo della computazione. Complessità: caso peggiore e caso medio. Indipendenza del tempo di decisione da un numero finito di configurazioni di input. Funzioni di complessità, classi di complessità DTIME e DSPACE (deterministic time e space). Inclusione DTIME(T (n)) ⊂ DSPACE(T(n)) ⊂ DTIME(2^{cT(n)}). Pumping Lemma per gli insiemi decidibili in tempo lineare. Simulazione di algoritmi, simulazione della macchina di Turing a seminastro, simulazione di una macchina multinastro. Macchine di Turing speciali. Teorema di Speedup lineare per macchine di Turing con alfabeto esteso. Valutazione del coefficente di accelerazione in relazione agli alfabeti. Decidibilità di insiemi di numeri naturali. Indipendenza dalla rappresentazione. Considerazioni sulla complessità.
- Turing calcolabilità: definizione di funzione Turing calcolabile, funzioni caratteristiche di insiemi Turing decidibili, la classe delle funzioni Turing calcolabili è chiusa per composizione, coppia, ricorsione primitiva e minimizzazione. Esempi di funzioni Turing calcolabili. Funzioni Ricorsive: equivalenza tra Turing computabilità e funzioni ricorsive. Funzione di Ackermann ([1] capp. 1,2,3,4,5 e [4] cap. 1).
- Funzioni costruibili in tempo. Nozione di T-orologio. Esempi di alcune funzioni costruibili in tempo. Chiusura per composizione.
- Macchine di Turing non-deterministiche: caratterizzazione mediante la decidibilità di insiemi proiezione. Definizione della classe delle funzioni non-deterministiche polinomiali. Problemi NP-completi.
2) Lambda calcolo e programmazione funzionale:
- Programmazione dichiarativa: cenni storici sul lambda calcolo, definizioni di base, i termini del lambda calcolo, la sostituzione semplice. Relazioni sui lambda termini. Congruenze, passaggio al contesto. α-equivalenza. L’α-equivalenza passa al contesto. Chiusura transitiva di una relazione, proprietà di Church-Rosser. Quozientamento dei lambda-termini rispetto all’alpha equivalenza.
- Definizione di beta-redesso e di beta-riduzione. Teorema di Church-Rosser per la beta-riduzione. Forme normali per beta-riduzione. Strategie di beta-riduzione. Strategia normalizzante: riduzione di sinistra (left most-outer most). Riduzione di testa. Termini Risolubili. Forme Normali di Testa. Teorema di caratterizzazione della risolubilità.
- Rappresentazione delle funzioni ricorsive: teorema di lambda definibilità. Esistenza del punto fisso per il lambda termini. Punto Fisso di Church ed punto fisso di Curry.
- Rappresentazione di altri tipi di dato nel lambda-calcolo: coppie, liste, alberi, soluzione di equazioni ricorsive su lambda-termini ([2] capp. 1, 2, 5).
Testi Adottati
[1] DEHORNOY, P., COMPLEXITÈ ET DECIDABILITÈ. SPRINGER-VERLAG, (1993).[2] KRIVINE, J.-L., LAMBDA CALCULUS: TYPES AND MODELS. ELLIS HORWOOD, (1993).
[3] SIPSER,M., INTRODUCTION TO THE THEORY OF COMPUTATION.THOMSON COURSE TECHNOLOGY, (2006).
Bibliografia Di Riferimento
G. Lolli, Hilbert e la logica, Le Matematiche, [S.l.], v. 55, n. 3, p. 93-126, mar. 2005. ISSN 2037-5298. Dexter C. Kozen, Theory of Computation, Springer-Verlag (2006). G. Ausiello, G. Gambosi, F. d'Amore Linguaggi, Modelli, Complessità Aho, Hopcroft, Ullman, Design and Analysis of Computer Programming. A. Bernasconi, B. Codenotti, Introduzione alla complessità computazionale, Springer-Verlag. H. Hermes, Enumerability, Decidability, Computability, Die Grundlehren der Mathematichen Wissenshaften in Einzeldarstellungen, n. 127, Springer-Verlag. F. Cardone and J. R. Hindley, History of Lambda-calculus and Combinatory Logic, from Swansea University Mathematics Department Research Report No. MRRS-05-06.Modalità Erogazione
Lezione frontale in aula.Modalità Frequenza
Facoltativa.Modalità Valutazione
L'esame consiste di due parti: un esame scritto, sostituibile con due prove in itinere (il voto finale viene calcolato pesando la prima prova al 35% e la seconda al 65%) e una prova orale opzionale, prevista per supplire alle insufficienze lievi (a partire dal 15, compreso) o per migliorare il voto ottenuto allo scritto. scheda docente materiale didattico
- Introduzione ai problemi di decisione, procedure algoritmiche e non algoritmiche, computazioni deterministiche, procedure discrete, nozione di alfabeto, di parola. Decidibilità e semidecidibilità di un insieme. Computazioni deterministiche, finitarie e discrete. Algoritmi formali: definizione formale di algoritmo, configurazioni di input, di output, funzione di transizione. Esempio di formalizzazione di un algoritmo. Decidibilità per automa finito. Rappresentazione degli automi mediante matrici. Monoide libero delle parole. Semianelli formali. Automi Finiti Non-deterministici. Linguaggi Regolari. Equivalenza tra automi deterministici e quelli non-deterministici.
- Macchine di Turing: definizione, decidibilità per macchina di Turing, tempo di arresto, spazio di arresto. Costo della computazione. Complessità: caso peggiore e caso medio. Indipendenza del tempo di decisione da un numero finito di configurazioni di input. Funzioni di complessità, classi di complessità DTIME e DSPACE (deterministic time e space). Inclusione DTIME(T (n)) ⊂ DSPACE(T(n)) ⊂ DTIME(2^{cT(n)}). Pumping Lemma per gli insiemi decidibili in tempo lineare. Simulazione di algoritmi, simulazione della macchina di Turing a seminastro, simulazione di una macchina multinastro. Macchine di Turing speciali. Teorema di Speedup lineare per macchine di Turing con alfabeto esteso. Valutazione del coefficente di accelerazione in relazione agli alfabeti. Decidibilità di insiemi di numeri naturali. Indipendenza dalla rappresentazione. Considerazioni sulla complessità.
- Turing calcolabilità: definizione di funzione Turing calcolabile, funzioni caratteristiche di insiemi Turing decidibili, la classe delle funzioni Turing calcolabili è chiusa per composizione, coppia, ricorsione primitiva e minimizzazione. Esempi di funzioni Turing calcolabili. Funzioni Ricorsive: equivalenza tra Turing computabilità e funzioni ricorsive. Funzione di Ackermann ([1] capp. 1,2,3,4,5 e [4] cap. 1).
- Funzioni costruibili in tempo. Nozione di T-orologio. Esempi di alcune funzioni costruibili in tempo. Chiusura per composizione.
- Macchine di Turing non-deterministiche: caratterizzazione mediante la decidibilità di insiemi proiezione. Definizione della classe delle funzioni non-deterministiche polinomiali. Problemi NP-completi.
2) Lambda calcolo e programmazione funzionale:
- Programmazione dichiarativa: cenni storici sul lambda calcolo, definizioni di base, i termini del lambda calcolo, la sostituzione semplice. Relazioni sui lambda termini. Congruenze, passaggio al contesto. α-equivalenza. L’α-equivalenza passa al contesto. Chiusura transitiva di una relazione, proprietà di Church-Rosser. Quozientamento dei lambda-termini rispetto all’alpha equivalenza.
- Definizione di beta-redesso e di beta-riduzione. Teorema di Church-Rosser per la beta-riduzione. Forme normali per beta-riduzione. Strategie di beta-riduzione. Strategia normalizzante: riduzione di sinistra (left most-outer most). Riduzione di testa. Termini Risolubili. Forme Normali di Testa. Teorema di caratterizzazione della risolubilità.
- Rappresentazione delle funzioni ricorsive: teorema di lambda definibilità. Esistenza del punto fisso per il lambda termini. Punto Fisso di Church ed punto fisso di Curry.
- Rappresentazione di altri tipi di dato nel lambda-calcolo: coppie, liste, alberi, soluzione di equazioni ricorsive su lambda-termini ([2] capp. 1, 2, 5).
[2] KRIVINE, J.-L., LAMBDA CALCULUS: TYPES AND MODELS. ELLIS HORWOOD, (1993).
[3] SIPSER,M., INTRODUCTION TO THE THEORY OF COMPUTATION.THOMSON COURSE TECHNOLOGY, (2006).
Programma
1) Computabilità, complessità e rappresentabilità:- Introduzione ai problemi di decisione, procedure algoritmiche e non algoritmiche, computazioni deterministiche, procedure discrete, nozione di alfabeto, di parola. Decidibilità e semidecidibilità di un insieme. Computazioni deterministiche, finitarie e discrete. Algoritmi formali: definizione formale di algoritmo, configurazioni di input, di output, funzione di transizione. Esempio di formalizzazione di un algoritmo. Decidibilità per automa finito. Rappresentazione degli automi mediante matrici. Monoide libero delle parole. Semianelli formali. Automi Finiti Non-deterministici. Linguaggi Regolari. Equivalenza tra automi deterministici e quelli non-deterministici.
- Macchine di Turing: definizione, decidibilità per macchina di Turing, tempo di arresto, spazio di arresto. Costo della computazione. Complessità: caso peggiore e caso medio. Indipendenza del tempo di decisione da un numero finito di configurazioni di input. Funzioni di complessità, classi di complessità DTIME e DSPACE (deterministic time e space). Inclusione DTIME(T (n)) ⊂ DSPACE(T(n)) ⊂ DTIME(2^{cT(n)}). Pumping Lemma per gli insiemi decidibili in tempo lineare. Simulazione di algoritmi, simulazione della macchina di Turing a seminastro, simulazione di una macchina multinastro. Macchine di Turing speciali. Teorema di Speedup lineare per macchine di Turing con alfabeto esteso. Valutazione del coefficente di accelerazione in relazione agli alfabeti. Decidibilità di insiemi di numeri naturali. Indipendenza dalla rappresentazione. Considerazioni sulla complessità.
- Turing calcolabilità: definizione di funzione Turing calcolabile, funzioni caratteristiche di insiemi Turing decidibili, la classe delle funzioni Turing calcolabili è chiusa per composizione, coppia, ricorsione primitiva e minimizzazione. Esempi di funzioni Turing calcolabili. Funzioni Ricorsive: equivalenza tra Turing computabilità e funzioni ricorsive. Funzione di Ackermann ([1] capp. 1,2,3,4,5 e [4] cap. 1).
- Funzioni costruibili in tempo. Nozione di T-orologio. Esempi di alcune funzioni costruibili in tempo. Chiusura per composizione.
- Macchine di Turing non-deterministiche: caratterizzazione mediante la decidibilità di insiemi proiezione. Definizione della classe delle funzioni non-deterministiche polinomiali. Problemi NP-completi.
2) Lambda calcolo e programmazione funzionale:
- Programmazione dichiarativa: cenni storici sul lambda calcolo, definizioni di base, i termini del lambda calcolo, la sostituzione semplice. Relazioni sui lambda termini. Congruenze, passaggio al contesto. α-equivalenza. L’α-equivalenza passa al contesto. Chiusura transitiva di una relazione, proprietà di Church-Rosser. Quozientamento dei lambda-termini rispetto all’alpha equivalenza.
- Definizione di beta-redesso e di beta-riduzione. Teorema di Church-Rosser per la beta-riduzione. Forme normali per beta-riduzione. Strategie di beta-riduzione. Strategia normalizzante: riduzione di sinistra (left most-outer most). Riduzione di testa. Termini Risolubili. Forme Normali di Testa. Teorema di caratterizzazione della risolubilità.
- Rappresentazione delle funzioni ricorsive: teorema di lambda definibilità. Esistenza del punto fisso per il lambda termini. Punto Fisso di Church ed punto fisso di Curry.
- Rappresentazione di altri tipi di dato nel lambda-calcolo: coppie, liste, alberi, soluzione di equazioni ricorsive su lambda-termini ([2] capp. 1, 2, 5).
Testi Adottati
[1] DEHORNOY, P., COMPLEXITÈ ET DECIDABILITÈ. SPRINGER-VERLAG, (1993).[2] KRIVINE, J.-L., LAMBDA CALCULUS: TYPES AND MODELS. ELLIS HORWOOD, (1993).
[3] SIPSER,M., INTRODUCTION TO THE THEORY OF COMPUTATION.THOMSON COURSE TECHNOLOGY, (2006).
Bibliografia Di Riferimento
G. Lolli, Hilbert e la logica, Le Matematiche, [S.l.], v. 55, n. 3, p. 93-126, mar. 2005. ISSN 2037-5298. Dexter C. Kozen, Theory of Computation, Springer-Verlag (2006). G. Ausiello, G. Gambosi, F. d'Amore Linguaggi, Modelli, Complessità Aho, Hopcroft, Ullman, Design and Analysis of Computer Programming. A. Bernasconi, B. Codenotti, Introduzione alla complessità computazionale, Springer-Verlag. H. Hermes, Enumerability, Decidability, Computability, Die Grundlehren der Mathematichen Wissenshaften in Einzeldarstellungen, n. 127, Springer-Verlag. F. Cardone and J. R. Hindley, History of Lambda-calculus and Combinatory Logic, from Swansea University Mathematics Department Research Report No. MRRS-05-06.Modalità Erogazione
Lezione frontale in aula.Modalità Frequenza
Facoltativa.Modalità Valutazione
L'esame consiste di due parti: un esame scritto, sostituibile con due prove in itinere (il voto finale viene calcolato pesando la prima prova al 35% e la seconda al 65%) e una prova orale opzionale, prevista per supplire alle insufficienze lievi (a partire dal 15, compreso) o per migliorare il voto ottenuto allo scritto. scheda docente materiale didattico
- Introduzione ai problemi di decisione, procedure algoritmiche e non algoritmiche, computazioni deterministiche, procedure discrete, nozione di alfabeto, di parola. Decidibilità e semidecidibilità di un insieme. Computazioni deterministiche, finitarie e discrete. Algoritmi formali: definizione formale di algoritmo, configurazioni di input, di output, funzione di transizione. Esempio di formalizzazione di un algoritmo. Decidibilità per automa finito. Rappresentazione degli automi mediante matrici. Monoide libero delle parole. Semianelli formali. Automi Finiti Non-deterministici. Linguaggi Regolari. Equivalenza tra automi deterministici e quelli non-deterministici.
- Macchine di Turing: definizione, decidibilità per macchina di Turing, tempo di arresto, spazio di arresto. Costo della computazione. Complessità: caso peggiore e caso medio. Indipendenza del tempo di decisione da un numero finito di configurazioni di input. Funzioni di complessità, classi di complessità DTIME e DSPACE (deterministic time e space). Inclusione DTIME(T (n)) ⊂ DSPACE(T(n)) ⊂ DTIME(2^{cT(n)}). Pumping Lemma per gli insiemi decidibili in tempo lineare. Simulazione di algoritmi, simulazione della macchina di Turing a seminastro, simulazione di una macchina multinastro. Macchine di Turing speciali. Teorema di Speedup lineare per macchine di Turing con alfabeto esteso. Valutazione del coefficente di accelerazione in relazione agli alfabeti. Decidibilità di insiemi di numeri naturali. Indipendenza dalla rappresentazione. Considerazioni sulla complessità.
- Turing calcolabilità: definizione di funzione Turing calcolabile, funzioni caratteristiche di insiemi Turing decidibili, la classe delle funzioni Turing calcolabili è chiusa per composizione, coppia, ricorsione primitiva e minimizzazione. Esempi di funzioni Turing calcolabili. Funzioni Ricorsive: equivalenza tra Turing computabilità e funzioni ricorsive. Funzione di Ackermann ([1] capp. 1,2,3,4,5 e [4] cap. 1).
- Funzioni costruibili in tempo. Nozione di T-orologio. Esempi di alcune funzioni costruibili in tempo. Chiusura per composizione.
- Macchine di Turing non-deterministiche: caratterizzazione mediante la decidibilità di insiemi proiezione. Definizione della classe delle funzioni non-deterministiche polinomiali. Problemi NP-completi.
2) Lambda calcolo e programmazione funzionale:
- Programmazione dichiarativa: cenni storici sul lambda calcolo, definizioni di base, i termini del lambda calcolo, la sostituzione semplice. Relazioni sui lambda termini. Congruenze, passaggio al contesto. α-equivalenza. L’α-equivalenza passa al contesto. Chiusura transitiva di una relazione, proprietà di Church-Rosser. Quozientamento dei lambda-termini rispetto all’alpha equivalenza.
- Definizione di beta-redesso e di beta-riduzione. Teorema di Church-Rosser per la beta-riduzione. Forme normali per beta-riduzione. Strategie di beta-riduzione. Strategia normalizzante: riduzione di sinistra (left most-outer most). Riduzione di testa. Termini Risolubili. Forme Normali di Testa. Teorema di caratterizzazione della risolubilità.
- Rappresentazione delle funzioni ricorsive: teorema di lambda definibilità. Esistenza del punto fisso per il lambda termini. Punto Fisso di Church ed punto fisso di Curry.
- Rappresentazione di altri tipi di dato nel lambda-calcolo: coppie, liste, alberi, soluzione di equazioni ricorsive su lambda-termini ([2] capp. 1, 2, 5).
[2] KRIVINE, J.-L., LAMBDA CALCULUS: TYPES AND MODELS. ELLIS HORWOOD, (1993).
[3] SIPSER,M., INTRODUCTION TO THE THEORY OF COMPUTATION.THOMSON COURSE TECHNOLOGY, (2006).
Programma
1) Computabilità, complessità e rappresentabilità:- Introduzione ai problemi di decisione, procedure algoritmiche e non algoritmiche, computazioni deterministiche, procedure discrete, nozione di alfabeto, di parola. Decidibilità e semidecidibilità di un insieme. Computazioni deterministiche, finitarie e discrete. Algoritmi formali: definizione formale di algoritmo, configurazioni di input, di output, funzione di transizione. Esempio di formalizzazione di un algoritmo. Decidibilità per automa finito. Rappresentazione degli automi mediante matrici. Monoide libero delle parole. Semianelli formali. Automi Finiti Non-deterministici. Linguaggi Regolari. Equivalenza tra automi deterministici e quelli non-deterministici.
- Macchine di Turing: definizione, decidibilità per macchina di Turing, tempo di arresto, spazio di arresto. Costo della computazione. Complessità: caso peggiore e caso medio. Indipendenza del tempo di decisione da un numero finito di configurazioni di input. Funzioni di complessità, classi di complessità DTIME e DSPACE (deterministic time e space). Inclusione DTIME(T (n)) ⊂ DSPACE(T(n)) ⊂ DTIME(2^{cT(n)}). Pumping Lemma per gli insiemi decidibili in tempo lineare. Simulazione di algoritmi, simulazione della macchina di Turing a seminastro, simulazione di una macchina multinastro. Macchine di Turing speciali. Teorema di Speedup lineare per macchine di Turing con alfabeto esteso. Valutazione del coefficente di accelerazione in relazione agli alfabeti. Decidibilità di insiemi di numeri naturali. Indipendenza dalla rappresentazione. Considerazioni sulla complessità.
- Turing calcolabilità: definizione di funzione Turing calcolabile, funzioni caratteristiche di insiemi Turing decidibili, la classe delle funzioni Turing calcolabili è chiusa per composizione, coppia, ricorsione primitiva e minimizzazione. Esempi di funzioni Turing calcolabili. Funzioni Ricorsive: equivalenza tra Turing computabilità e funzioni ricorsive. Funzione di Ackermann ([1] capp. 1,2,3,4,5 e [4] cap. 1).
- Funzioni costruibili in tempo. Nozione di T-orologio. Esempi di alcune funzioni costruibili in tempo. Chiusura per composizione.
- Macchine di Turing non-deterministiche: caratterizzazione mediante la decidibilità di insiemi proiezione. Definizione della classe delle funzioni non-deterministiche polinomiali. Problemi NP-completi.
2) Lambda calcolo e programmazione funzionale:
- Programmazione dichiarativa: cenni storici sul lambda calcolo, definizioni di base, i termini del lambda calcolo, la sostituzione semplice. Relazioni sui lambda termini. Congruenze, passaggio al contesto. α-equivalenza. L’α-equivalenza passa al contesto. Chiusura transitiva di una relazione, proprietà di Church-Rosser. Quozientamento dei lambda-termini rispetto all’alpha equivalenza.
- Definizione di beta-redesso e di beta-riduzione. Teorema di Church-Rosser per la beta-riduzione. Forme normali per beta-riduzione. Strategie di beta-riduzione. Strategia normalizzante: riduzione di sinistra (left most-outer most). Riduzione di testa. Termini Risolubili. Forme Normali di Testa. Teorema di caratterizzazione della risolubilità.
- Rappresentazione delle funzioni ricorsive: teorema di lambda definibilità. Esistenza del punto fisso per il lambda termini. Punto Fisso di Church ed punto fisso di Curry.
- Rappresentazione di altri tipi di dato nel lambda-calcolo: coppie, liste, alberi, soluzione di equazioni ricorsive su lambda-termini ([2] capp. 1, 2, 5).
Testi Adottati
[1] DEHORNOY, P., COMPLEXITÈ ET DECIDABILITÈ. SPRINGER-VERLAG, (1993).[2] KRIVINE, J.-L., LAMBDA CALCULUS: TYPES AND MODELS. ELLIS HORWOOD, (1993).
[3] SIPSER,M., INTRODUCTION TO THE THEORY OF COMPUTATION.THOMSON COURSE TECHNOLOGY, (2006).
Bibliografia Di Riferimento
G. Lolli, Hilbert e la logica, Le Matematiche, [S.l.], v. 55, n. 3, p. 93-126, mar. 2005. ISSN 2037-5298. Dexter C. Kozen, Theory of Computation, Springer-Verlag (2006). G. Ausiello, G. Gambosi, F. d'Amore Linguaggi, Modelli, Complessità Aho, Hopcroft, Ullman, Design and Analysis of Computer Programming. A. Bernasconi, B. Codenotti, Introduzione alla complessità computazionale, Springer-Verlag. H. Hermes, Enumerability, Decidability, Computability, Die Grundlehren der Mathematichen Wissenshaften in Einzeldarstellungen, n. 127, Springer-Verlag. F. Cardone and J. R. Hindley, History of Lambda-calculus and Combinatory Logic, from Swansea University Mathematics Department Research Report No. MRRS-05-06.Modalità Erogazione
Lezione frontale in aula.Modalità Frequenza
Facoltativa.Modalità Valutazione
L'esame consiste di due parti: un esame scritto, sostituibile con due prove in itinere (il voto finale viene calcolato pesando la prima prova al 35% e la seconda al 65%) e una prova orale opzionale, prevista per supplire alle insufficienze lievi (a partire dal 15, compreso) o per migliorare il voto ottenuto allo scritto.