| |
SPECIAL ISSUE:
Selected Papers of the Conference "Typed Lambda Calculi and Applications 2007" (in progress)
|
Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators
|
Abstract
The symmetric interaction combinators are an equally expressive variant of
Lafont's interaction combinators. They are a graph-rewriting model of
deterministic computation. We define two notions of observational equivalence
for them, analogous to normal form and head normal form equivalence in the
lambda-calculus. Then, we prove a full abstraction result for each of the two
equivalences. This is obtained by interpreting nets as certain subsets of the
Cantor space, called edifices, which play the same role as Boehm trees in the
theory of the lambda-calculus.
|
Publication date: December 22, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(4:6)2009
Hit Counts: 1258 |
 Creative Commons | |
