The topos of labelled trees : a categorical semantics for SCCS

The work presented in this paper starts from the observation that labelled trees together with labeland parenthood-preserving morphisms form a topos: a slice category of the topos of sheaves over the poset (!, ) for the topology generated by the empty cover for 0. After a very well presented and easily accessible exposition of this idea two applications are elaborated. First, it is shown how the use of topos theory simplifies the interpretation of SCCS using labelled trees, in particular, the treatment of guarded recursion. Second, a new characterisation of bisimulation in terms of morphisms is presented: two trees S, T are bisimilar iff there are conflict-preserving morphisms f: S ! T and g: T ! S such that fgf = f and gfg = g. In elementary terms (distilled from Propositions 6.1 and 6.2), a morphism f: S !T is conflict-preserving if whenever x!a y in S and f(x) = f(x0) then x0 !a y0 for some y0 with f(y) = f(y0). The proof of the characterisation of bisimulation in terms of conflict-preserving morphisms makes essential use of the topos-theoretic view. The presentation is very understandable and does not require prior knowledge of topos theory.