Typing Reflection in Higher-Order Psi-Calculi
Authors
Bojesen, Bjarke Bredow ; Lybech, Stian ; Bendixen, Alexander Rønning
Term
4. term
Education
Publication year
2021
Submitted on
2021-06-14
Abstract
This thesis examines Higher-Order Ψ-calculi (HOΨ), a general framework for modeling many variants of the π-calculus, a formal language for describing communication in concurrent systems. In HOΨ, each concrete calculus is obtained by choosing a few parameters: terms/channels M, N; conditions φ; assertions Ψ; and an entailment relation Ψ ⊩ φ that states in which environments Ψ a condition φ holds, for example when two channels are considered equivalent. We review the syntax and labelled semantics, and we present three reduction semantics: (1) a fully compositional variant using structural congruence, which does not capture every internal (τ) step; (2) a variant that matches the τ-labelled transitions exactly by using reduction contexts instead of structural rules; and (3) a variant that is broader than the τ-transition relation and is defined via an evaluation relation rather than structural congruence. Higher-order mobility (sending processes as data) can be seen as a restricted form of reflection, the ability to treat code as data, compute on it, modify it, and run it again. We connect these ideas by showing that the HOΨ framework can represent the Reflective Higher-Order (ρ) calculus of Meredith and Radestock. We define a generic type system for HOΨ based on the largest of the three reduction semantics, thereby covering all τ-steps. The system provides general typing rules for processes, while leaving the typing of terms, conditions, and assertions as parameters, reflecting that these sets are also parameters in HOΨ. We prove subject reduction (types are preserved by computation), but not a general safety theorem, because what counts as a type error depends on the chosen parameters; safety must therefore be established separately for each instantiation. Finally, we attempt to type reflective features by instantiating the generic type system for the ρ-calculus encoding. The example indicates what restrictions are needed to make reflection typable, such as adding type information to entailment to obtain type-aware channel equivalence.
Denne afhandling undersøger Higher-Order Ψ-kalkyler (HOΨ), et generelt rammeværk til at modellere mange varianter af π-kalkylen, et formelt sprog til at beskrive kommunikation i samtidige systemer. I HOΨ får man en konkret kalkyle ved at vælge få parametre: termer/kanaler M, N; betingelser φ; påstande Ψ; og en entailment-relation Ψ ⊩ φ, der angiver i hvilke omgivelser Ψ en betingelse φ gælder, fx hvornår to kanaler er ækvivalente. Vi gennemgår syntaks og mærket semantik og præsenterer tre reduktionssemantikker: (1) en fuldt kompositionel variant, der bruger strukturel kongruens, men som ikke dækker alle interne (τ-)skridt; (2) en variant der matcher præcist de τ-mærkede overgange ved at bruge reduktionskontekster i stedet for strukturelle regler; og (3) en variant der er bredere end τ-overgangsrelationen og som defineres via en evalueringsrelation frem for direkte ved strukturel kongruens. Højere-ordens mobilitet (at sende processer som data) ses som en begrænset form for refleksion, dvs. evnen til at behandle kode som data, beregne på den, ændre den og køre den igen. Vi forbinder disse idéer ved at vise, at HOΨ kan repræsentere den refleksive højere-ordens (ρ) kalkyle af Meredith og Radestock. Vi definerer et generisk typesystem for HOΨ baseret på den største af de tre reduktionssemantikker, så alle τ-skridt er dækket. Systemet giver generelle typeregler for processer, men kræver, at typer for termer, betingelser og påstande angives som parametre, i tråd med at disse selv er parametre i HOΨ. Vi beviser typebevarelse (subject reduction), men ikke en generel sikkerhedssætning, fordi hvad der tæller som en typefejl afhænger af den valgte instans; sikkerhed må derfor vises separat for hver instans. Til sidst forsøger vi at typebestemme refleksion ved at instantiere typesystemet til repræsentationen af ρ-kalkylen. Eksemplet peger på hvilke begrænsninger der kræves for at gøre refleksion typbar, fx at tilføje typeinformation til entailment for at få typebevidst kanalækvivalens.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords