Continuous functions on streams
Richard Garner – 6 May 2020
A few weeks ago, I explained how models and comodels of an algebraic theory T can encode programs and their associated environments. This week I will explain how co-S-models in the category of T-models provide a way of translating T-environments into S-environments.In particular, I consider the case where S and T are the free theories generated by an A-ary, respectively B-ary operation. In this case, co-S-models in T-models encode a simple kind of automaton translating streams of B's into streams of A's. Our novel result is that the terminal co-S-model in T-models (describing possible behaviours of such automata) is exactly the set of continuous functions between Baire spaces B^N->A^N; this realises the old idea of Brouwer that continuous = computable, and extends prior work of Hancock, Ghani and Pattinson.
Back