Ichiro Hasuo

• Department of Computer Science
• University of Tokyo
• ichiro [at] is.s.u-tokyo.ac.jp

• English
• Japanese
• Dutch
• Chinese

• Home
• Contact
• Research
• Cv
• Papers
• Talks
• Teaching

[Back to Teaching]

Mathematical Semantics of Computer Systems (AY 2014)

General

• IMPORTANT: there won't be a lecture on Monday 2 Feb. The next and last lecture will be on 9 Feb.
• Monday 10.30h-12.00h
• Room 102, School of Science Bldg. No. 7
• For Graduate Students. Code: 4810-1168
• Lectures are in English

Course Objective

Correctness of computer systems and programs is a pressing issue in the modern world. Their verification—providing mathematical proofs for their correctness—calls for their mathematical modeling; this is what the field called semantics is all about. The course introduces some basic techniques in the field, most notably those which employ category theory.

Keywords: category theory, lambda calculus, type theory, logic, categorical semantics, algebraic semantics, denotational semantics, algebra, coalgebra, automaton, fibration, categorical logic

References

• [Lambek & Scott 1986]
  J. Lambek, P. J. Scott, Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1988
• [Awodey 2010]
  S. Awodey, Category Theory. Oxford University Press, 2010.
• [Leinster 2014]
  T. Leinster, Basic Category Theory. Cambridge University Press, 2014.
• [Jacobs 2012]
  Bart Jacobs, Introduction to Coalgebra: Towards Mathematics of States and Observations. Draft of a book, available online. 2012
• [Jacobs, 1999]
  Bart Jacobs, Categorical Logic and Type Theory. Elsevier Science, 1999

Besides the above ones, there is a series of fantastic online lectures on category theory by Eugenia Cheng and Simon Willerton. Recommended!

Course Structure (Tentative)

1. Basic Category Theory

   We exhibit basic constructs in category theory used in the subsequent parts.

   • categories, functors, natural transformations
   • monoids and preorders as degenerate cases
   • epis and monos
   • (co)products, (co)equalizers, (co)limits
   • adjoint functors, equivalences of categories
   • exponents, Cartesian closed categories

   We will roughly follow [Lambek & Scott 1986, Part 0] which is however way too fast for beginners; [Awodey 2010, Leinster 2014] will be nice supplementary material.

   Goal of Part I: familiarize yourself with the Yoneda lemma, a celebrated result in category theory by Prof. Nobuo Yoneda (Dept. IS, U. Tokyo), desirably in its end/coend form.

2. The Curry-Howard-Lambek Correspondence

   As a first example of categorical semantics, a correspondence between typed lambda-calculi and Cartesian closed categories is introduced. An emphasis is on the view that categorical semantics is an extension of algebraic semantics (such as Boolean algebras for classical logic and Heyting algebras for intuitionistic logic).

   • typed lambda-calculi
   • natural deduction for intuitionistic logic
   • syntactic presentation of Cartesian closed categories
   • free Cartesian closed categories and completeness

   We will follow [Lambek & Scott 1986, Part 1] omitting some topics.

   Goal of Part II: the completeness result for Moggi's computational lambda-calculus as an extension of the Curry-Howard-Lambek correspondence, following

   Computational lambda-calculus and monads. Tech. Report ECS-LFCS-88-66, Edinburgh Univ., 1988. [pdf]

3. Coalgebras and State-Based Transition Systems

   Our second usage of category theory has quite different a flavor: it models various state-based transition systems as coalgebras, a categorical dual of algebras. Here the view of categories as "many-sorted algebras (or monoids)" is not so important as in the previous part---in fact we will almost exclusively work in the category of sets and functions. An alternative categorical genericity from which we benefit is a functor as a parameter: it allows to develop a uniform theory of state-based systems like automata of various kinds (deterministic, nondeterministic, probabilistic, or even quantum).

   • coalgebraic modeling
   • bisimulation
   • final coalgebras
   • (process algebra and bialgebra)

   We will follow [Jacobs 2012, Chapters 1-3].

   Goal of Part III: the completeness result for Moggi's computational lambda-calculus as an extension of the Curry-Howard-Lambek correspondence.

4. Fibrations and Categorical Logic

   The last part introduces a more advanced bit of category theory, namely the theory of fibrations that are a categorical way of "organizing indexed entities." It will be applied to modeling predicate logic, extending Part 2. If time allows another application, namely coinductive predicates in state-based transition systems, will be introduced. This will unify the views in Parts 2--3 and illustrate the versatility of the mathematical language of category theory.

   • fibrations
   • indexed categories, the Grothendieck construction
   • fiberwise structures
   • (co)products between fibers
   • equational logics as fibrations
   • first-order predicate logics as fibrations
   • (inductive and coinductive predicates)

   The topics are picked from [Jacobs, 1999]

   Goal of Part IV: Understand coinduction up-to formulated in a fibration, as in

   Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot: Coinduction up-to in a fibrational setting. CSL-LICS 2014: 20

Course Material

Coming soon

Evaluation

Based on homework assignments.

Schedule

• 2014.10.6 (Mon) CANCELED due to Typhoon Phanfone :(
• 2014.10.15 (Wed) handout
• 2014.10.20 (Mon) I went slowly and left the explanations of:

  functors, (split) eps and monos, coproducts

  to the next lecture. Will start with the explanation of "Today's Goal." handout
• 2014.10.27 (Mon) Barely finished "Today's Goal I" (on the uniqueness of products). NOTICE: there is a report assignment; see the handout. handout (updated from the version distributed at the lecture)
• 2014.11.10 (Mon) Finished up to the definition of cone as a natural transformation. The next lecture will continue with the same handout.
  We are going much slower (roughly twice) than I'd planned. I suppose it's better than going too fast and losing a lot of you (^_^;)
  handout
• 2014.11.17 (Mon) Finished till Section 2.2 of the handout from the previous lecture (concrete presentation of limits in Sets). NOTICE: there is a report assignment; see the handout. handout
• 2014.12.1 (Mon) Introduced adjunction, with examples: free monoids, discrete/attached topologies, exponentials and Currying, a dual adjunction with 2^(_). We'll start with the triangular equations. handout
• 2014.12.8 (Mon) Finished (finally!) the adjunction part. The next lecture will start with the Yoneda lemma.
  Report problems: Exercise 3.1, 3.2 on page 2 of the handout, with Exercise 3.3 optional. Due: 2014.12.22 (the beginning of the lecture)
  handout
• 2014.12.15 (Mon) We just finished a sketch of a proof of the Yoneda lemma. We'll resume with the explanation how an entire natural transformation \alpha: C(_,X) => P is reconstructed from the data \alpha_X(id_X), eventually moving back to the analogy to the Cayley theorem.
  NOTICE: the next lecture will feature John Power (U. Bath, UK) as a guest lecturer! handout
• 2014.12.22 (Mon) We had the pleasure of having John Power (U. Bath, UK) as a guest lecturer! He talked about the definition of adjunction (or, more precisely: the property of having a left adjoint), and its consequences.
  After that we reviewed the proof of the Yoneda lemma, and the definition of the Yoneda embedding. We will start with the interpretation of the Yoneda embedding ("representing an object by how it is related to other objects"), together with the analogy to the Cayley theorem. We will also do another proof of the uniqueness of a left adjoint.
• 2015.1.5 (Mon) Finished the section on the Yoneda lemma, with emphases on: an analogy to the Cayley theorem (abstract "transformation" as a concrete function); and "representation" of an object by a Hom-functor. Hinted the use of algebraic semantics for giving a negative answer to a word problem.
  handout
• 2015.1.19 (Mon) Finished algeberaic semantics; made introduction to categorical semantics as its generalization, and as a scheme that unifies the Curry-Howard-Lambek correspondences and knot invariants. The next lecture will start with reduction/conversion of lambda terms. handout
• 2015.1.26 (Mon) We didn't quite finish the content of the handout; in the next lecture we will start with definition of interpretation of type derivation trees.
  NOTICE: the report assignment is postponed and it is not due in a week. handout
• 2015.2.2 (Mon) NOTICE: there won't be a lecture on this date.
• 2015.2.9 (Mon) The final (makeup) class. handout