Combinatory logic and lambda calculus (03B40) Limits and colimits (products, sums, directed limits, pushouts, fiber products, equalizers, kernels, ends and coends, etc.) (18A30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Abstract: First, we extend Leifer-Milner RPO theory, by giving general conditions to obtain IPO labelled transition systems (and bisimilarities) with a reduced set of transitions, and possibly finitely branching. Moreover, we study the weak variant of Leifer-Milner theory, by giving general conditions under which the weak bisimilarity is a congruence. Then, we apply such extended RPO technique to the lambda-calculus, endowed with lazy and call by value reduction strategies. We show that, contrary to process calculi, one can deal directly with the lambda-calculus syntax and apply Leifer-Milner technique to a category of contexts, provided that we work in the framework of weak bisimilarities. However, even in the case of the transition system with minimal contexts, the resulting bisimilarity is infinitely branching, due to the fact that, in standard context categories, parametric rules such as the beta-rule can be represented only by infinitely many ground rules. To overcome this problem, we introduce the general notion of second-order context category. We show that, by carrying out the RPO construction in this setting, the lazy observational equivalence can be captured as a weak bisimilarity equivalence on a finitely branching transition system. This result is achieved by considering an encoding of lambda-calculus in Combinatory Logic.
Recommendations
- RPO, Second-order Contexts, and Lambda-calculus
- Efficient Bisimilarities from Second-Order Reaction Semantics for π-Calculus
- scientific article; zbMATH DE number 1330448
- The theory of contexts for first order and higher order abstract syntax
- Simulation in the call-by-need lambda-calculus with letrec
Cites work
- Algebra and Coalgebra in Computer Science
- Deriving bisimulation congruences in the DPO approach to graph rewriting with borrowed contexts
- From rewrite rules to bisimulation congruences
- Full abstraction in the lazy lambda calculus
- scientific article; zbMATH DE number 5604126 (Why is no real title available?)
- scientific article; zbMATH DE number 92599 (Why is no real title available?)
- scientific article; zbMATH DE number 1956527 (Why is no real title available?)
- scientific article; zbMATH DE number 1759615 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- Local bigraphs and confluence: two conjectures (extended abstract)
- Process Bisimulation Via a Graphical Encoding
- Processes, Terms and Cycles: Steps on the Road to Infinity
- RPO, Second-Order Contexts, and λ-Calculus
Cited in
(9)- Counterpart semantics for a second-order -calculus
- Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs
- Finitely Branching Labelled Transition Systems from Reaction Semantics for Process Calculi
- RPO, Second-order Contexts, and Lambda-calculus
- Reactive Systems, Barbed Semantics, and the Mobile Ambients
- On the semantics of second order lambda calculus: From bruce-meyer-mitchell models to hyperdoctrine models and vice-versa
- RPO, Second-Order Contexts, and λ-Calculus
- Reactive systems, (semi-)saturated semantics and coalgebras on presheaves
- On generic context lemmas for higher-order calculi with sharing
This page was built for publication: RPO, Second-Order Contexts, and λ-Calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458369)
