Submitted by Mariangiola Dezani-Ciancaglini
Statement. Find trees representing contextual equivalences
Problem Origin. Stated by Mariangiola Dezani, Paula Severi and Fer-Jan de Vries.
If is a set of -terms, the contextual equivalence is deﬁned by:
if and only if for all contexts ,
where denotes -reduction.
[Wadsworth, 1976] shows that , where is the set of head normal forms, coincides with Böhm trees equality (up to inﬁnite ’s). [Hyland, 1976] shows that , where is the set of normal forms, coincides with Böhm trees equality (up to ﬁnite ’s).
The question is to ﬁnd tree representations of -terms whose equalities coincide with the following contextual equivalences:
The set is deﬁned in [Berarducci, 1996], and the sets , , are deﬁned in [Severi and de Vries, 2005, Kennaway et al., 2005].
[Kennaway et al., 2005] Kennaway, J., Severi, P., Sleep, M., and de Vries, F. J. (2005). Inﬁnite rewriting: from syntax to semantics. In Processes, Terms and Cycles: Steps on the Road to Inﬁnity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 148–172. Springer-Verlag.
[Severi and de Vries, 2005] Severi, P. and de Vries, F. J. (2005). Order structures for Böhm-like models. In Computer Science Logic, volume 3634 of Lecture Notes in Computer Science, pages 103–116. Springer-Verlag.