Di Gianantonio, Pietro and Honsell, Furio and Lenisa, Marina - RPO, Second-order Contexts, and Lambda-calculus

lmcs:1120 - Logical Methods in Computer Science, August 6, 2009, Volume 5, Issue 3
RPO, Second-order Contexts, and Lambda-calculus

Authors: Di Gianantonio, Pietro and Honsell, Furio and Lenisa, Marina

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.

Source : oai:arXiv.org:0906.2727
DOI : 10.2168/LMCS-5(3:6)2009
Volume: Volume 5, Issue 3
Published on: August 6, 2009
Submitted on: August 13, 2008
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,F.3.2,F.4.1


Consultation statistics

This page has been seen 166 times.
This article's PDF has been downloaded 51 times.