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


If 𝒫 is a set of λ  -terms, the contextual equivalence M  ~ 𝒫 N  is defined by:

C[M  ] - → M  ∈ 𝒫 if and only if             ′
C[N ] - → N  ∈ 𝒫 for all contexts C[ ]  ,

where -→ denotes β  -reduction.

[Wadsworth, 1976] shows that ~ ℋ , where ℋ is the set of head normal forms, coincides with Böhm trees equality (up to infinite η  ’s). [Hyland, 1976] shows that ~ 𝒩 , where 𝒩 is the set of normal forms, coincides with Böhm trees equality (up to finite η  ’s).

The question is to find 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. ~ 𝒮𝒜X   , where X  is a set of λ  -terms and 𝒮 𝒜X  is the set of strongly active terms depending on X  ,
  5. ~ ℋ 𝒜 , where ℋ 𝒜 is the set of head active terms.

The set 𝒯 is defined in [Berarducci, 1996], and the sets 𝒮 𝒜 , 𝒮 𝒜X  , ℋ 𝒜 are defined in [Severi and de Vries, 2005, Kennaway et al., 2005].

References for # 18

[Berarducci, 1996]    Berarducci, A. (1996). Infinite λ  -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). Infinite rewriting: from syntax to semantics. In Processes, Terms and Cycles: Steps on the Road to Infinity: 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.

[Next]  [Previous]  [Up]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014