Strumenti Utente

Strumenti Sito


magistraleinformatica:mod:2015-16:start

Modelli di calcolo - Models of computation

MOD 2015/16 (375AA, 9 CFU)

Lecturer: Roberto Bruni
web - 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
    • 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: x1,…,xk should be n1,…,nk
      • 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 (Vtau)bottom not in Zbottom
      • 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(f1,d1) should be apply(f2,d2)
    • 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: Xn+1= shoudl be Xn+1=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
    • 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): 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):
    1. first name and last name (please clarify which is which, to avoid ambiguities)
    2. enrolment number (numero di matricola)
    3. bachelor degree (course of study and university)
    4. 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
Exam
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
CAAL
PseuCo
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
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
PEPA
38 Wed 25/05 09:00-11:00 C1 Second mid-term written exam
Exam
39 Wed 08/06 14:00-16:00 C1 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 Exam
41 Mon 25/07 14:00-16:00 C1 Exam
42 Tue 06/09 14:00-16:00 L1 Exam
43 Wed 02/11 11:00-13:00 C1 Extra-ordinary Exam
44 Fri 20/01 14:00-16:00 L1 Exam
45 Fri 10/02 14:00-16:00 L1 Exam

Past courses

magistraleinformatica/mod/2015-16/start.txt · Ultima modifica: 10/02/2017 alle 13:42 (20 mesi fa) da Roberto Bruni