Problem # 18

Submitted by Mariangiola Dezani-Ciancaglini
Date: 2001–2005
Statement. Find trees representing contextual equivalences $\text{[math]}$
Problem Origin. Stated by Mariangiola Dezani, Paula Severi and Fer-Jan de Vries.

If $𝒫$ is a set of $λ$ -terms, the contextual equivalence $M ~ 𝒫 N$ is deﬁned by:

[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 $𝒮 𝒜$ , $𝒮 𝒜X$ , $ℋ 𝒜$ 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 $D ∞$ -models of the lambda-calculus. SIAM Journal of Computing, 5(3):488–521.