Macquarie University
01whole.pdf (655.15 kB)

The game semantics of free cartesian closed categories: a syntactic derivation

Download (655.15 kB)
posted on 2023-11-22, 04:33 authored by Ruben Henner Zilibowitz

It is well known that cartesian closed categories (CCCs) model typed lambda calculus with products. We explore how the game semantics of free CCCs can be derived from the syntax of a typed lambda calculus with products and invertible constants. The categorical model for this is a free CCC, 𝓕G, generated by an object equipped with a free group, G, of automorphisms. This appears to be a novel approach that has the benefit of simplicity while also being generalisable. Along the way we give an algorithm for computing long βη-normal forms together with a proof of correctness. All of this is facilitated by a natural automorphism Φ on the inclusion functor 𝓕 → 𝓕G, where 𝓕 is the free CCC generated by an object. A solution to the problem of totality of composition of strategies [1] is hinted at using our machinery. We also claim conjecturally that it is possible to generalise long βη-normal forms to free almost bi-cartesian closed categories [16] using these ideas.


Table of Contents

1. Introduction -- 2. Games -- 3. Syntax -- 4. Conclusion -- A. βγ reduction -- References

Awarding Institution

Macquarie University

Degree Type

Thesis MRes


Master of Research

Department, Centre or School

School of Mathematical and Physical Sciences

Year of Award


Principal Supervisor

Ross Street

Additional Supervisor 1

Richard Garner


Copyright: The Author Copyright disclaimer:




54 pages

Former Identifiers

AMIS ID: 247465

Usage metrics

    Macquarie University Theses