| - Understand the basics of complete partial orders (cpo) and domain theory
- Manage the basic machinery for applying domain theory in a computer science context: monotonicity, least upper bound, continuity, least fixed point, Scott induction
- Being able to prove properties about cpos
- Being able to define the denotational semantics of a programming language and of a specific programming construct
- Being able to compute the denotational semantics of a program (in While or in PCF)
- Being able to prove properties about the denotational semantics of a program
- Being able to relate the denotational and the operational semantics of PCF
- Being able to compute the denotational semantics of untyped lambda terms
- Being able to prove properties about the denotational semantics of untyped lambda terms
|
|
Semantics of a programming language can be given in an operational, axiomatic and a denotational way. Operational semantics describes the computational behaviour of programs (their evaluation) and axiomatic semantics describes their properties using logical formulas. Denotational semantics describes a program as a mathematical function (basically, a function from input to output). This course studies denotational semantics of programming languages and the mathematical theory required for giving a denotational semantics: domain theory.
We assume that the students are familiar with operational (and preferably also some axiomatic) semantics, especially for a simple imperative "while" language and for a simple functional language like (untyped) lambda calculus. In this course we describe the denotational semantics for the simple imperative programming language "while". Then we move on to PCF, which is the archetypical functional programming language, being a simply typed lambda calculus with two basic data types (booleans and naturals) and a fixed-point operator. We define the operational semantics of PCF and a notion of program equivalence that emerges from that. program equivalence is given through the important concept of observational (or contextual) equality. We describe the denotational semantics of PCF and we relate the denotational equality with the operational program equivalence.
Mathematically, denotational semantics rests on the field of "domain theory". A domain is an partially ordered structure with some additional properties: they are so called "complete partial orders". The ordering may be regarded as an "information ordering": a larger element contains more information than a smaller element. In the course we study the basic elements of domain theory that are needed to give a denotational semantics to while and PCF: monotonicity and continuity of functions; constructions on domains like the sum, product and function space domain; basic domains like the flat domains of booleans and numbers. We study the important construction of a "least fixed point" of a continuous function and the concept of "Scott induction".
We discuss how different operational semantics (like call-by-name and call-by-value) give rise to a different domain of interpretation. We discuss the notion of sequential computation and show that all the standard domain model for PCF is not "fully abstract". (A notion we will define.) We show how to use domain theory to give a denotational semantics to other formal (programming) languages, especially the untyped lambda calculus. We describe the D_A model as a concrete model for the untyped lambda calculus and study its basic properties, using Bohm trees of untyped lambda term
|
 |
|
|
|
• complete partial orders (cpos) and domains
• monotonicity, continuity, chain, directed set, least upperbound, Knaster-Tarski fixed point theorem, Scott-induction
• operations on domains: product, sum, function space; examples of domains.
• denotational semantics of the simple "While" language
• program analysis via denotational semantics
• the language PCF, functional languages with higher-types;
• operational semantics of PCF via call-by-name and call-by-value
• denotational semantics of PCF
• equivalence of denotational and operational semantics, e.g. via logical relations
• full abstraction in PCF
• denotational semantics of the untyped lambda calculus
• D_A model and Bohm trees |
|
The following courses taught at the RU give you the required starting knowledge:
• beweren en bewijzen
• berekenbaarheid
• semantiek en correctheid
• berekeningsmodellen
The required contents of these courses is captured by any set of courses covering
• predicate logic (derivations and models)
• operational semantics of a simple While programming language (natural semantics or structured operational semantics)
• basic knowledge of lambda calculus
Additionally, some knowledge of basic recursion theory would be useful. |
|
|
• Lecture Notes on Denotational Semantics by Andy Pitts and Glynn Winskel. (Available via internet: http://www.cl.cam.ac.uk/~gw104/dens.pdf)
• Grondslagen van de Informatica 2 course notes by Erik Barendsen, http://www.cs.ru.nl/~herman/onderwijs/semantics2013/GI2-dictaat.pdf
• Handout on dI domains: http://www.cs.ru.nl/~herman/onderwijs/semantics2014/didomainsnote.pdf
Pre-knowledge on operational semantics of a simple While programming language (natural semantics or structured operational semantics) is in Hanne Riis Nielson en Flemming Nielson: Semantics with applications, 1999 (available via internet: http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.pdf) |
• 32 hours lecture
• 32 hours problem session
• 104 hours individual study period
Extra information teaching methods: lectures + exercise class |
| | Verplicht materiaalDictaat| Lecture Notes on Denotational Semantics by Andy Pitts and Glynn Winskel. (Available via internet: http://www.cl.cam.ac.uk/~gw104/dens.pdf) |
| Dictaat| Grondslagen van de Informatica 2 course notes by Erik Barendsen, http://www.cs.ru.nl/~herman/onderwijs/semantics2013/GI2-dictaat.pdf |
| Handouts| Handout on dI domains: http://www.cs.ru.nl/~herman/onderwijs/semantics2014/didomainsnote.pdf |
|
|
Aanbevolen materiaalBoek| Hanne Riis Nielson en Flemming Nielson: Semantics with applications, 1999 (available via internet: http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.pdf) |
|
|
WerkvormenToetsenTentamen| Weging | | 1 |
| Gelegenheden | | Blok KW4, Blok KW4 |
|
|
| |