Normal Form Simulation for McCarthy's Amb

This paper presents co-inductive operational theories of program refinement and equivalence, called whnf similarity and whnf simulation equivalence, for the λ-calculus extended with McCarthy's ambiguous choice operator amb. The associated whnf simulation co-induction proof principle is useful for establishing non-trivial equivalences and refinement relationships between programs. Whnf similarity is a pre-congruence and whnf simulation equivalence is a congruence and a conservative extension of the Lévy-Longo tree theory for the pure λ-calculus.