TY - GEN
T1 - Edifices and full abstraction for the symmetric interaction combinators
AU - Mazza, Damiano
PY - 2007/1/1
Y1 - 2007/1/1
N2 - The symmetric interaction combinators are a variant of Lafont's interaction combinators. They are a graph-rewriting model of parallel deterministic computation. We define a notion analogous to that of head normal form in the λ-calculus, and make a semantical study of the corresponding observational equivalence. We associate with each net a compact metric space, called edifice, and prove that two nets are observationally equivalent iff they have the same edifice. Edifices may therefore be compared to Böhm trees in infinite η-normal form, or to Nakajima trees, and give a precise topological account of phenomena like infinite η-expansion.
AB - The symmetric interaction combinators are a variant of Lafont's interaction combinators. They are a graph-rewriting model of parallel deterministic computation. We define a notion analogous to that of head normal form in the λ-calculus, and make a semantical study of the corresponding observational equivalence. We associate with each net a compact metric space, called edifice, and prove that two nets are observationally equivalent iff they have the same edifice. Edifices may therefore be compared to Böhm trees in infinite η-normal form, or to Nakajima trees, and give a precise topological account of phenomena like infinite η-expansion.
U2 - 10.1007/978-3-540-73228-0_22
DO - 10.1007/978-3-540-73228-0_22
M3 - Conference contribution
AN - SCOPUS:38149094365
SN - 9783540732273
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 305
EP - 320
BT - Typed Lambda Calculi and Applications - 8th International Conference,TLCA 2007, Proceedings
PB - Springer Verlag
T2 - 8th International Conference on Typed Lambda Calculi and Applications,TLCA 2007
Y2 - 26 June 2007 through 28 June 2007
ER -