Explicit Substitution and Sorted Bigraphs
Citation:
Shane Thomas Ó Conchúir, Explicit Substitution and Sorted Bigraphs, [thesis], Trinity College (Dublin, Ireland). School of Computer Science & Statistics, 2009, pp.372Download Item:
Abstract:
This dissertation investigates the notions of sorting and explicit substitution in the framework of bigraphs. We present kind sortings which endeavour to add enough structure to bigraphs to allow faithful representations, within this framework, of both the nested grammar of models of formal calculi and the hierarchical structures encountered in context-aware systems and network topographies. We also explore Milner’s bigraphical representation of explicit substitutions. Pure, or unsorted, bigraphs are composed of a linking structure and a nesting structure, both self-reconfigurable, which respectively model mobile connectivity and mobile locality. They have a rich dynamic theory but limited applications. Sortings allow bigraphs to model more significant applications. We begin by defining kind sortings which allow us to refine the nesting structure with respect to a containment relation. We proceed by enriching the nesting structure with capacities and then proving that the sorting retains the rich dynamic theory of pure bigraphs. Applications of the sorting include: a better modelling of formal calculi with a sorted, ordered grammar with capacities e.g. the λ-calculus; an interpretation of basic types as sets of controls and of a type preorder as subset inclusion, allowing us to present bigraphical models of typed λ-calculi; the introduction of basic flow control for the reaction relation, allowing us to express simple algorithms; and an encoding of semi-structured data with an ordered tree structure and capacities e.g. XML data and contexts. Milner’s bigraphical encoding of his λ-calculus of explicit substitutions is indirectly studied. We contrast its notion of non-local substitution with the local substitution found in most explicit substitution (ES) calculi. We investigate properties of Milner’s calculus and discover that it satisfies many desirable properties of ES calculi. The set of properties it satisfies e.g. open confluence, full composition of substitutions, and preservation of strong normalisation, holds for few of these calculi. We attribute its properties to the non-local method of substitution which arises naturally from the bigraphical model. We present proofs of normalisation based on a novel simulation of non-local substitution with local substitution and characterise the set of strongly normalising terms of the calculus using an intersection type system. Finally, we refine Milner’s encoding and present models of the untyped, simply typed, and inter-section typed λ-calculi which have close static and dynamic correspondences with type derivations in the explicit substitution calculus. We use the results of our study of Milner’s calculus to reason about normalisation and confluence in these models, the last of which aims to model exactly the parallel compositions of terminating λ-terms.
Sponsor
Grant Number
Irish Research Council for Science, Engineering, and Technology: funded by the National Development Plan
Author: Ó Conchúir, Shane Thomas
Advisor:
Mac an Airchinnigh, MícheálQualification name:
Doctor of Philosophy (Ph.D.)Publisher:
Trinity College (Dublin, Ireland). School of Computer Science & StatisticsNote:
TARA (Trinity’s Access to Research Archive) has a robust takedown policy. Please contact us if you have any concerns: rssadmin@tcd.ieType of material:
thesisAvailability:
Full text availableMetadata
Show full item recordLicences: