DidaWiki

Questa pagina è in sola lettura. Puoi visualizzare il sorgente, ma non puoi modificarlo. Contatta l'amministratore se pensi che ci sia un errore.
====== Modelli di calcolo - Models of computation ======

{{:magistraleinformatica:mod:prova.png?150 | }}

**MOD 2015/16 (375AA, 9 CFU)**

Lecturer: **Roberto Bruni**\\
[[http://www.di.unipi.it/~bruni|web]] - [[mailto:bruni@di.unipi.it|email]] - phone 050 2212785 - fax 050 2212726

Office hours: **Wednesday 15:00-17:00 or by appointment**


----

==== Objectives ====

The objective of the course is to present:
  * different models of computation,
  * their programming paradigms,
  * their mathematical descriptions, both //concrete// and //abstract//,
and also to present some intellectual tools/techniques:
  * for reasoning on models, and
  * for proving (some of) their properties.

To this aim, a rigorous approach will be followed for both the //syntax// and the //semantics// of the paradigms we work on:
  * **IMP**: imperative models
  * **HOFL**: functional models
  * **CCS**, pi-calculus: concurrent, non-deterministic and interactive models
  * **PEPA**: probabilistic/stochastic models

The focus will be on basic proof techniques (there will be not time to introduce more advanced topics in detail).

In doing so, several important notions will be presented (not necessarily in this order):
context-free grammars, 
proof systems (axioms and inference rules),
goal-driven derivations,
various incarnations of well-founded induction,
structural recursion,
lambda-calculus,
program equivalence,
compositionality,
completeness and correctness,
type systems,
domain theory (complete partial orders, continuous functions, fixpoint),
labelled transition systems,
bisimulation equivalences,
temporal and modal logics,
Markov chains,
probabilistic reactive and generative systems.

----

==== Course Overview ====

We introduce the principles of operational semantics, the principles of denotational semantics, and the techniques to relate one to the other for an imperative language and for a higher order functional language. Operational and observational semantics of two process description languages (CCS and pi-calculus) are presented. Several examples of temporal and modal logics are also discussed (HM, LTL, CTL*, mu-calculus). Finally, we consider operational nondeterministic models with discrete probabilities, and we present them from the perspective of probabilistic and stochastic automata, and of the PEPA calculus.

----

==== Textbook(s) ====


  * Glynn Winskel, "The formal Semantics of Programming Languages", MIT Press, 1993. Chapters: 1.3, 2, 3, 4, 5, 8, 11.\\ "La Semantica Formale dei Linguaggi di Programmazione", traduzione italiana a cura di Franco Turini, UTET 1999. 
  * Robin Milner, "Communication and Concurrency, Prentice Hall, 1989. Chapters: 1-7, 10.
  * Lecture notes: a monograph is under preparation, drafts of the chapters are made available (with errata), comments are welcome
    * {{:magistraleinformatica:mod:01-10-with-sol-book-draft-2016.pdf|Chapters 01-10}}: Introduction, IMP, HOFL, revised version, with solutions to selected exercises
      * P23, factorial example: the inclusion symbol is missing between {(1,1)} and {(1,1),(2,2)}
      * P86, text of the proof of Th.4.5: implication is written several times (three occurrences) as a single arrow; a double arrow should be used instead
      * P95, line -5: x<sub>1</sub>,...,x<sub>k</sub> should be n<sub>1</sub>,...,n<sub>k</sub>
      * P96, statement of Th.4.2: < should be \prec
      * P97, end of first part of the proof: f(a)=F(y,f... )=F(y,g...)=g(a) should be f(a)=F(a,f...)=F(a,g...)=g(a)
      * P182, line 8: "the element" should be deleted
      * P200, last line: the bottom element returned as a result is in (V<sub>tau</sub>)<sub>bottom</sub> not in Z<sub>bottom</sub>
      * P351, Problem 3.4, lines -10 and -8: the subscript \sigma'=\sigma must be deleted
      * P354, line 4: false should be true
      * P358, Solution to Problem 6.4: B[skip] should be C[skip]
      * P364, Solution to Problem 8.5, last line: apply(f<sub>1</sub>,d<sub>1</sub>) should be apply(f<sub>2</sub>,d<sub>2</sub>)
    * {{:magistraleinformatica:mod:11-16-with-sol-book-draft-2016.pdf|Chapters 11-16}}: Concurrent systems, probabilistic systems, revised version, with solutions to selected exercises
      * P234, line -3: delete the sentence: "all process names in X and all recursively defined names in p occur guarded in p."
      * P25, line 11: r should be q (twice)
      * P277, line 6: X p should be O p
      * P294, Fig. 13.1, line 5: [x=y].p should be [x=y]p (twice)
      * P294, Fig. 13.1, line 8: (y).p should be (y)p (twice)
      * P304, Ex. 13.5, line 7: tau.nil should be nil
      * P322, Def. 14.14: X<sub>n+1</sub>= shoudl be X<sub>n+1</sub>=x
      * P328, P329, P330, P337: the domain and codomain of all transformations \Phi is the powerset of S x S, not the powerset of S 
      * P363, Problem 3.4, lines -10 and -8: the subscript \sigma'=\sigma must be deleted
      * P366, line 4: false should be true
    * [[magistraleinformatica:mod:errata-2016:|link]] to previous versions of all chapters, with errata

----

==== Exams ====

The evaluation will be based on written and oral exams.

The written exam is not necessary if the two (written) mid-terms exams are evaluated positively.

  * First (written) mid-term exam: **30-03-2016, 14:00-16:00, room B** 
  * Second (written) mid-term exam: **25-05-2016, 9:00-11:00, room C1**

Registration to written exams (mandatory): [[https://esami.unipi.it/esami/|Exams registration system]]

In the written exam the student must demonstrate 
  * knowledge: his/her knowledge of the course material
  * problem solving: the ability to solve some exercises, and
  * organisation: the ability to organise an effective and correctly written reply.

During the oral exam the student must demonstrate 
  * knowledge: his/her knowledge of the course material, and 
  * understanding: the ability to discuss the reading matter thoughtfully and with propriety of expression.

----

==== Announcements ====

  * **as the course starts**:\\ Each student should send an email to the professor from his/her favourite email account with **subject MOD15** and the following data\\ (by doing so, the account will be included in the class mailing-list, where important announcements can be sent):
    - **first name** and **last name** (please clarify which is which, to avoid ambiguities)
    - **enrolment number** (numero di matricola)
    - bachelor degree (**course of study** and **university**)
    - your favourite topics in computer science (optional)

----


==== Lectures ====

^ N ^ Date ^ Time ^ Room ^ Lecture notes ^ Links ^
|  1 | Mon 22/02 | 14:00-16:00 | C1 | Introduction to the course |  |
|  2 | Wed 24/02 | 11:00-13:00 | L1 | Preliminaries:\\ //formal semantics// |  |
|  3 | Thu 25/02 | 11:00-13:00 | L1 | Preliminaries:\\ //signatures, unification problem// |  |
|  4 | Mon 29/02 | 14:00-16:00 | C1 | Preliminaries:\\ //logical systems, goal-oriented derivations//\\ \\ Operational semantics of IMP:\\ //syntax of IMP//  |  |
|  5 | Wed 02/03 | 11:00-13:00 | L1 | Operational semantics of IMP:\\ //inference rules, non-termination, equivalence// |  |
|  6 | Thu 03/03 | 11:00-13:00 | L1 | Operational semantics of IMP:\\ //equivalence and inequivalence proofs//\\ \\ Induction and recursion:\\ //well-founded relations, transitive closures// |  |
|  7 | Mon 07/03 | 14:00-16:00 | C1 | Induction and recursion:\\ //well-founded induction, mathematical induction, structural induction// |  |
|  8 | Wed 09/03 | 11:00-13:00 | L1 | Induction and recursion:\\ //induction on derivations, rule induction// |  |
|  9 | Thu 10/03 | 11:00-13:00 | L1 | Induction and recursion:\\ //lexicographic precedence relation, primitive recursive functions\\ well-founded recursion, Ackermann function//\\ \\ Exercises on the operational semantics of IMP and induction  |  |
| 10 | Mon 14/03 | 14:00-16:00 | C1 | Exercises on the operational semantics of IMP and induction\\ \\ Partial orders and fixpoints:\\ //partial orders, Hasse diagrams, least upper bound// |  |
| 11 | Wed 16/03 | 11:00-13:00 | L1 | Partial orders and fixpoints:\\ //chains, complete partial orders, bottom element, monotonicity, continuity// |  |
| 12 | Thu 17/03 | 11:00-13:00 | L1 | Partial orders and fixpoints:\\ //fixpoint theorem, immediate consequences operator//\\ \\ Denotational semantics of IMP:\\ //lambda-notation, abstraction, application, alpha-conversion, beta-rule// |  |
| 13 | Mon 21/03 | 14:00-16:00 | C1 | Denotational semantics of IMP:\\ //capture-avoiding substitutions, denotational semantics of IMP, examples// |  |
| 14 | Wed 23/03 | 11:00-13:00 | L1 | Denotational semantics of IMP:\\ //equivalence between operational and denotational semantics: completeness,\\ equivalence between operational and denotational semantics: correctness// |  |
| 15 | Thu 24/03 | 11:00-13:00 | L1 | Exercises about CPOs and the denotational semantics of IMP |  |
| 16 | Wed 30/03 | 14:00-16:00 | B | **First mid-term written exam**\\ {{:magistraleinformatica:mod:testo-2016-03-30.pdf|Exam}}\\ {{:magistraleinformatica:mod:testo-2016-03-30-appello-straordinario.pdf|Appello Straordinario}} |  |
| 17 | Wed 06/04 | 11:00-13:00 | L1 | Denotational semantics of IMP:\\ //Computational induction (optional argument)//\\ \\ Operational semantics of HOFL:\\ //Pre-terms, well-formed terms, typability// |  |
| 18 | Thu 07/04 | 11:00-13:00 | L1 | Operational semantics of HOFL:\\ //Lazy and eager semantics, canonical forms//\\ \\ Domain theory:\\ //Integers with bottom, cartesian product//  |  |
| 19 | Mon 11/04 | 14:00-16:00 | C1 | Solutions to the first mid-term exam\\ \\ Domain theory:\\ //Cartesian product, functional domains// |  |
| 20 | Wed 13/04 | 11:00-13:00 | L1 | Domain theory:\\ //functional domains//\\ \\ Exercises on the equivalence between the operational and denotational semantics of IMP and on the operational semantics of HOFL  |  |
| 21 | Thu 14/04 | 11:00-13:00 | L1 | Domain theory:\\ //Lifting, continuity theorems//\\ \\ Exercises on the equivalence between the operational and denotational semantics of IMP and on the operational semantics of HOFL |  |
| 22 | Mon 18/04 | 14:00-16:00 | C1 | Domain theory:\\ //continuity theorems, apply, currry, fix//\\ \\ Exercises on the equivalence between the operational and denotational semantics of IMP and on the operational semantics of HOFL |  |
| 23 | Wed 20/04 | 11:00-13:00 | L1 | HOFL denotational semantics |  |
| 24 | Thu 21/04 | 11:00-13:00 | L1 | Equivalence between the operational and denotational semantics of HOFL:\\ //Correctness of the operational semantics, counterexample to completeness// |  |
| 25 | Mon 25/04 |  |  | **Festa della libertà** |  |
| 26 | Wed 27/04 | 11:00-13:00 | L1 | Equivalence between the operational and denotational semantics of HOFL:\\ //Operational convergence, denotational convergence,\\ operational convergence implies denotational convergence,\\ denotational convergence implies operational convergence (optional),\\ operational equivalence, denotational equivalence, unlifted semantics// |  |
| 27 | Thu 28/04 | 11:00-13:00 | L1 | Exercises on the denotational semantics of HOFL and on the equivalence between the operational and denotational semantics of HOFL |  |
| 28 | Mon 02/05 | 14:00-16:00 | C1 | CCS:\\ //extensible stack, syntax, operational semantics, guarded processes// |  |
| 29 | Wed 04/05 | 11:00-13:00 | L1 | CCS:\\ //abstract semantics, graph isomorphism, trace equivalence, bisimulation game,\\ strong bisimulation, strong bisimilarity// |  |
| 30 | Thu 05/05 | 11:00-13:00 | L1 | CCS:\\ //properties of strong bisimilarity, Knaster-Tarski's fixpoint theorem, compositionality// |  |
| 31 | Mon 09/05 | 14:00-16:00 | C1 | CCS:\\ //Hennessy-Milner logic, axiomatisation of strong bisimilarity,\\ weak bisimilarity//  |  |
| 32 | Wed 11/05 | 11:00-13:00 | L1 | CCS:\\ //Weak observational congruence, Milner's tau-laws, dynamic bisimilarity,\\ modelling with CCS//   | [[http://caal.cs.aau.dk/|CAAL]]\\ [[http://pseuco.com|PseuCo]]\\ [[http://rap.dsi.unifi.it/tapas/en/index.htm|TAPAS]] |
| 33 | Thu 12/05 | 11:00-13:00 | L1 | Temporal and modal logics:\\ //linear temporal logic (LTL), computational tree logic (CTL* and CTL), mu-calculus// |  |
| 34 | Mon 16/05 | 14:00-16:00 | C1 | Pi-calculus:\\ //syntax and operational semantics,\\ structural equivalence and reduction semantics (optional reading)\\ abstract semantics, early and late bisimulations// | [[http://golang.org/|Google Go]] |
| 35 | Wed 18/05 | 11:00-13:00 | L1 | Pi-calculus:\\ //early and late bisimilarities, weak bisimilarities//\\ \\ Measure theory and Markov chains:\\ //probability space, random variables, exponential distribution,\\ stochastic processes, homogeneous Markov chains, DTMC, finite path probability,\\ steady state distribution//  |  |
| 36 | Thu 19/05 | 11:00-13:00 | L1 | Measure theory and Markov chains:\\ //Ergodic DTMC, CTMC, sojourn time, infinitesimal generator matrix, embedded DTMC,\\ bisimilarity revisited, reachability predicate, CTMC bisimilarity, DTMC bisimilarity//\\ \\ Exercises on CCS, modal logic and pi-calculus |  |
| 37 | Mon 23/05 | 14:00-16:00 | C1 | Markov chains with actions and nondeterminism:\\ //reactive systems, bisimilarity for reactive systems, Larsen-Skou logic,\\ generative systems, simple Segala automata, Segala automata\\ alternating and bundle transitions systems (optional reading)//\\ \\ PEPA (optional reading)\\ \\ Exercises on CCS, modal logic and pi-calculus\\ \\ Exercises on probabilistic systems  | [[http://www.dcs.ed.ac.uk/pepa/|PEPA]] |
| 38 | Wed 25/05 | 09:00-11:00 | C1 | **Second mid-term written exam**\\ {{:magistraleinformatica:mod:testo-2016-05-25.pdf|Exam}} |  |
| 39 | Wed 08/06 | 14:00-16:00 | C1 | {{:magistraleinformatica:mod:testo-2016-06-08.pdf|Exam}}\\ 1st mid-term: Exercises 1,2,3 (1h15')\\ 2nd mid-term: Exercises 4,5,6 (1h15')\\ full exam: Exercises 2,3,4,5 (1h55', exercises 1 and 6 optional) |  |
| 40 | Thu 30/06 | 14:00-16:00 | C1 | {{:magistraleinformatica:mod:testo-2016-06-30.pdf|Exam}} |  |
| 41 | Mon 25/07 | 14:00-16:00 | C1 | {{:magistraleinformatica:mod:testo-2016-07-25.pdf|Exam}} |  |
| 42 | Tue 06/09 | 14:00-16:00 | L1 | {{:magistraleinformatica:mod:testo-2016-09-06.pdf|Exam}} |  |
| 43 | Wed 02/11 | 11:00-13:00 | C1 | {{:magistraleinformatica:mod:testo-2016-11-02.pdf|Extra-ordinary Exam}} |  |
| 44 | Fri 20/01 | 14:00-16:00 | L1 | {{:magistraleinformatica:mod:testo-2017-01-20.pdf|Exam}} |  |
| 45 | Fri 10/02 | 14:00-16:00 | L1 | {{:magistraleinformatica:mod:testo-2017-02-10.pdf|Exam}} |  |

----

==== Past courses ====

  * [[magistraleinformatica:mod:2014-15:|A.A. 2014/15]]
  * [[magistraleinformatica:mod:2013-14:|A.A. 2013/14]]

----