Università degli Studi di Udine OpenUniud - Archivio istituzionale delle tesi di dottorato
 

OpenUniud - Archivio istituzionale delle tesi di dottorato >
Udine Thesis Repository >
01 - Tesi di dottorato >

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10990/820

Autori: Peressotti, Marco
Supervisore afferente all'Università: MICULAN, MARINO
Centro di ricerca: DIPARTIMENTO DI SCIENZE MATEMATICHE, INFORMATICHE E FISICHE - DMIF
Titolo: Coalgebraic semantics of self-referential behaviours
Abstract (in inglese): 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.
Parole chiave: Coinduction; Higher-order languages; Trace equivalence
MIUR : Settore INF/01 - Informatica
Lingua: eng
Data: 3-apr-2017
Corso di dottorato: Dottorato di ricerca in Informatica
Ciclo di dottorato: 28
Università di conseguimento titolo: Università degli Studi di Udine
Luogo di discussione: Udine
Citazione: Peressotti, M. Coalgebraic semantics of self-referential behaviours. (Doctoral Thesis, Università degli Studi di Udine, 2017).
In01 - Tesi di dottorato

Full text:

File Descrizione DimensioniFormatoConsultabilità
peressotti - thesis - 2017-03-03.pdfTesi1,1 MBAdobe PDFVisualizza/apri


Tutti i documenti archiviati in DSPACE sono protetti da copyright. Tutti i diritti riservati.


Segnala questo record su
Del.icio.us

Citeulike

Connotea

Facebook

Stumble it!

reddit


 

  ICT Support, development & maintenance are provided by CINECA. Powered on DSpace SoftwareFeedback CINECA