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

<p>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, <em>��</em>_{<em><strong>G</strong></em>}, generated by an object equipped with a free group, <em><em><strong>G</strong></em></em>, 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 <em>βη</em>-normal forms together with a proof of correctness. All of this is facilitated by a natural automorphism <em>Φ</em> on the inclusion functor �� → ��_{<em><strong>G</strong></em>}, 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 <em>βη</em>-normal forms to free almost bi-cartesian closed categories [16] using these ideas.</p>