Abstract
We apply Leifer-Milner RPO approach to the λ-calculus, endowed with lazy and call by value reduction strategies. We show that, contrary to process calculi, one can deal directly with the λ-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 β 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 (call by value) 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 λ-calculus in Combinatory Logic.
Work supported by ART PRIN Project prot. 2005015824 (funded by MIUR).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S., Ong, L.: Full Abstraction in the Lazy Lambda Calculus. Information and Computation 105(2), 159–267 (1993)
Bonchi, F., Konig, B., Montanari, U.: Saturated Semantics for Reactive Systems. In: LICS (2006)
Bonchi, F., Gadducci, F., Konig, B.: Process Bisimulation via a Graphical Encoding. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 168–183. Springer, Heidelberg (2006)
Di Gianantonio, P., Honsell, F., Lenisa, M.: RPO, Second-order Contexts, and λ-calculus, Extended version (2008), www.dimi.uniud.it/pietro/papers/socl.pdf
Egidi, L., Honsell, F., Ronchi Della Rocca, S.: Operational, Denotational and Logical Descriptions: A Case Study. Fundamenta Inf. 16(2), 149–169 (1992)
Ehrig, H., König, B.: Deriving bisimulation congruences in the DPO approach to graph rewriting with borrowed contexts. Mathematical Structure in Computer Science 16(6), 1133–1163 (2006)
Gadducci, F., Montanari, U.: Observing Reductions in Nominal Calculi via a Graphical Encoding of Processes. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 106–126. Springer, Heidelberg (2005)
Hindley, R., Seldin, J.: Introduction to combinators and l-calculus. Cambridge University Press, Cambridge (1986)
Klin, B., Sassone, V., Sobocinski, P.: Labels from reductions: Towards a general theory. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 30–50. Springer, Heidelberg (2005)
Leifer, J.: Operational congruences for reactive systems, PhD thesis, University of Cambridge Computer Laboratory (2001)
Leifer, J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 243–258. Springer, Heidelberg (2000)
Milner, R.: Local bigraphs and confluence: Two conjectures. In: Proc. Express 2006. ENTCS, vol. 175, pp. 65–73 (2007)
Sassone, V., Sobocinski, P.: Deriving bisimulation congruences: 2-categories vs precategories. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 409–424. Springer, Heidelberg (2003)
Sassone, V., Sobocinski, P.: Reactive systems over cospans. In: LICS 2005, pp. 311–320. IEEE, Los Alamitos (2005)
Sewell, P.: From rewrite rules to bisimulation congruences. Theoretical Computer Science 274(1–2), 183–230 (2002)
Sobocinski, P.: Deriving process congruences from reduction rules, PhD thesis, University of Aarhus (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Di Gianantonio, P., Honsell, F., Lenisa, M. (2008). RPO, Second-Order Contexts, and λ-Calculus. In: Amadio, R. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2008. Lecture Notes in Computer Science, vol 4962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78499-9_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-78499-9_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78497-5
Online ISBN: 978-3-540-78499-9
eBook Packages: Computer ScienceComputer Science (R0)