Logo del repository
  1. Home
 
Opzioni

Coalgebraic semantics of self-referential behaviours

Peressotti, Marco
2017-04-03
  • doctoral thesis

Abstract
In this thesis, we investigate the semantics of systems which can refer to themselves, e.g., by ``passing around" systems of the same kind as values (hence potential observables). For this reason, we refer to these systems as self-referential. Instances of this scenario are higher-order calculi like the λ-calculus, the calculus of higher-order communicating systems (CHOCS), the higher-order π-calculus (HO-π), HOcore, etc. It is well known that higher-order systems pose unique challenges and are difficult to reason about. Many bisimulations and proof methods have been proposed also in recent works. This ongoing active effort points out that a definition of abstract self-referential behaviour is still elusive. We address these difficulties by providing an abstract characterisation of self-referential behaviours as self-referential endofunctors, i.e. functors whose definition depends on their own final coalgebra. The construction of these functors is not trivial, since they must be defined at once with their own final coalgebra and due to the presence of both covariant and contravariant dependencies (e.g. arising from higher-order inputs). We provide such a construction, where algebraic compact functors are the key technicality, like other works dealing with mixed-variance dependencies of some kind. Similarly defined endofunctors arise from considering as object systems (i.e, those which can be values) only certain subclasses of systems (usually via some syntactic restriction) or a syntactic representations (cf. higher-order process algebras): self-referential endofunctors are shown to be universal among them. Universality renders self-referential endofunctors a touchstone for similar behavioural functors and offers the mathematical structure for assessing soundness and completeness of other models via properties of the associated universal morphisms. As a further contribution, we provide a construction capturing infinite trace semantics by finality whereas the state of the art characterisations are weakly final. This result, together with existing accounts of finite traces, allows the definition of self-referential behaviours with respect to (in)finite trace semantics.
Archivio
http://hdl.handle.net/11390/1132904
Diritti
open access
Soggetti
  • Coinduction

  • Higher-order language...

  • Trace equivalence

  • Settore INF/01 - Info...

google-scholar
Get Involved!
  • Source Code
  • Documentation
  • Slack Channel
Make it your own

DSpace-CRIS can be extensively configured to meet your needs. Decide which information need to be collected and available with fine-grained security. Start updating the theme to match your nstitution's web identity.

Need professional help?

The original creators of DSpace-CRIS at 4Science can take your project to the next level, get in touch!

Realizzato con Software DSpace-CRIS - Estensione mantenuta e ottimizzata da 4Science

  • Impostazioni dei cookie
  • Informativa sulla privacy
  • Accordo con l'utente finale
  • Invia il tuo Feedback