Mathematical Semantics of Computer Systems, MSCS (4810-1168)
Handout for Lecture 13 (2017/1/23)
Ichiro Hasuo, Dept. Computer Science, Univ. Tokyo
http://www-mmm.is.s.u-tokyo.ac.jp/∼ichiro

Video recording of the lectures is available at: http://www-mmm.is.s.u-tokyo.ac.jp/videos/mscs2016

1

Cartesian Closed Categories as Models of Typed λ-Calculus

Definition. Interpretation J K of typed λ-calculus. Interpreting types, type derivation trees, typejudgments, and terms.
Definition. Substitution lemma: interpretation of s[t/x] is given by composition of arrows.
Theorem. Soundness of categorical semantics: if s =βη t, then JsK = JtK.

2Categorical Modeling of State-Based Dynamics by Coalgebras

Our principal reference is:[Jacobs 2012] Bart Jacobs, Introduction to Coalgebra: Towards Mathematics of States
and Observations. Draft of a book, available online. 2012
Definition. F -coalgebra, F -coalgebra morphism, the category Coalg(F ) of F -coalgebras.
Example. Exhibit coalgebras, coalgebra morphisms, for:
F = A × ( ); F = 1 + A × ( ); F = A × ( ) × ( ); F = 2 × ( )A (deterministic automata);
F = 2 × (P )A ∼= P(1 + A × ) (nondeterministic automata); and polynomial functors in general.
Definition. Final coalgebra.
Example. Final coalgebras for: F = A × ( ); F = 1 + A × ( ); F = A × ( ) × ( );Lemma. Lambek’s lemma. It follows that final coalgebras need not exist.
Compare with: algebra, initial algebra (understood as datatype). Consider F = 1 + ( ) (induction). This leads to our interests in coinduction.
Example. Coinduction as a definition principle. A = {0, 1}, F = A × ( ), for which a final
coalgebra is ⟨hd, tl⟩ : Aω → A × Aω . Consider various recursive definitions:()evens(σ) = hd(σ) : evens(tl(tl(σ)))(1)()
odds(σ) = hd(tl(σ)) : odds(tl(tl(σ)))(2)
ones = 1 : ones(3)
bad = bad(4)

Well-definedness is ensured once you express the definition as a coalgebra.
How about merge(a0 : a1 : . . . , b0 : b1 : . . . ) = a0 : b0 : a1 : b1 : . . .?
Example. Coinduction as a proof principle. To see odds = evens ◦ tail, we check that evens ◦ tailmakes the finality diagram for odds commute.
The examples might look easy... but imagine you want to implement the definitions and proofs
on proof assistants like Coq!
A structure result (cf. [Prop. 5.2, Jacobs 2012]):
Theorem. Let F : C → C. The forgetful functor U : Coalg(F ) → C creates colimits.

1□3

Lectures Remaining

Coalgebras and State-Based Transition Systems. We will follow [Jacobs 2012, Chapters 1-3]
• 2017.1.30 (Mon)

4

Final Report AssignmentDue: 23:59 JST, Friday 10 February, 2017
Submit to the lecturer’s mailbox (on the corridor), to the (oﬃcial) report box of the department,or by email to ichiro@is.s.u-tokyo.ac.jp
You can choose questions to answer. Each question is assigned points; and you are expected toanswer 100 points worth. However, in case you have not submitted some of the previous reportassignments, you can make it up by answering more.
1. (40) Prove the substitution lemma.
2. (30) Let f : A → B be an arrow in a Cartesian closed category C. It induces natural transformations: A × ( ) ⇒ B × ( ), and ( )B ⇒ ( )A . Show that the adjunctions A × ( ) ⊣ ( )Aand B × ( ) ⊣ ( )B are “compatible” with those natural transformations. (You first have toformalize what “compatibility” means.)
3. We are interested in the CCC structure of a presheaf category [Cop , Sets]. Here C is a smallcategory.
(a) (30) Prove that [Cop , Sets] has all small limits and colimits.
(Hint: they are computed “pointwise.”)(b) (40) The category [Cop , Sets] has exponentials, too. Let P, Q : Cop → Sets be presheaves;
QP be an exponential; and C ∈ C. Describe the set (QP )(C).
(Hint: this is an interesting one. Use the Yoneda lemma!)(c) (30) Specialize the above answer to the case when C is the following category with twoobjects and four arrows.
d //EVc

Here the identity arrows are implicit. Discuss the relationship with the notion of graphhomomorphism.
4. End is a notion that generalizes that of limit.
(a) (30) Describe its definition, and show that limits are special cases of ends.
(b) (40) Let C be a small category; and F, G : Cop → Sets be presheaves. Describe the set
Nat(F, G) of natural transformations as a limit.
5. (50) Let C be a small category and consider the presheaf category [Cop , Sets]. Prove that any
presheaf P : Cop → Sets is a colimit of a certain diagram that consists solely of representable
presheaves (i.e. those presheaves of the form yC = C( , C)).
(Hint: You have to find a suitable diagram. It is given by so-called the category of elements.)
6. (40) Let evens, odds and merge be the stream functions earlier in this handout. Use thecoinduction proof principle to prove, for each σ ∈ Aω ,merge(evens(σ), odds(σ)) = σ .
(Draw a suitable finality diagram)2