Berarducci trees observational equivalence infinitary lambda calculus Bohm out technique

摘要

We propose an extension of lambda calculus for which the Berarducci trees equality coincides with observational equivalence, when we observe rootstable or rootactive behavior of terms. In one direction the proof is an. adaptation of the classical Bohm out technique. In the other direction the proof is based on confluence for strongly converging reductions in this extension. (C) 2003 Elsevier Science B.V. All rights reserved. [References: 26]