[Next]  [Previous]  [Up]

#### Problem # 18

Submitted by Mariangiola Dezani-Ciancaglini
Date: 2001–2005
Statement. Find trees representing contextual equivalences
Problem Origin. Stated by Mariangiola Dezani, Paula Severi and Fer-Jan de Vries.

[PRINT this PROBLEM]

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:

1. where is the set of weak head normal forms,
2. , where is the set of top normal forms,
3. , where is the set of strongly active terms,
4. , where is a set of -terms and is the set of strongly active terms depending on ,
5. , where is the set of head active terms.

The set is deﬁned in [Berarducci, 1996], and the sets , , are deﬁned in [Severi and de Vries, 2005, Kennaway et al., 2005].

##### References for # 18

[Berarducci, 1996]    Berarducci, A. (1996). Inﬁnite -calculus and non-sensible models. In Ursini, A. and Aglianò, P., editors, Logic and Algebra (Pontignano, 1994), pages 339–377. Dekker.

[Hyland, 1976]    Hyland, M. (1976). A syntactic characterization of the equality in some models for the lambda calculus. J. London Math. Soc. (2), 12(3):361–370.

[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.

[Wadsworth, 1976]    Wadsworth, C. P. (1976). The relation between computational and denotational properties for Scott’s -models of the lambda-calculus. SIAM Journal of Computing, 5(3):488–521.

[Next]  [Previous]  [Up]
Last modified: July 21, 2014