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.

The topos of labelled trees : a categorical semantics for SCCS / S. Kasangian, S. Vigna. - In: FUNDAMENTA INFORMATICAE. - ISSN 0169-2968. - 32:1(1997), pp. 27-45.

The topos of labelled trees : a categorical semantics for SCCS

S. Kasangian;S. Vigna
1997

Abstract

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.
semantica della concorrenza
1997
Article (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/27915
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact