Bisimulation in Untyped Lambda Calculus:

Abstract

On the basis of an operational bisimulation account of Böhm tree equivalence, a novel operationally-based development of the Böhm tree theory is presented, including an elementary congruence proof for Böhm tree equivalence. The approach is also applied to other sensible and lazy tree theories. Finally, a syntactic proof principle, called bisimulation up to context, is derived from the congruence proofs. It is used to give a simple syntactic proof of the least fixed point property of fixed point combinators. The paper surveys notions of bisimulation and trees for sensible λ-theories based on reduction to head normal forms as well as for lazy λ-theories based on weak head normal forms.