## Standardization and Böhm trees for $$\Lambda \mu$$-calculus.(English)Zbl 1284.68137

Blume, Matthias (ed.) et al., Functional and logic programming. 10th international symposium, FLOPS 2010, Sendai, Japan, April 19–21, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-12250-7/pbk). Lecture Notes in Computer Science 6009, 134-149 (2010).
Summary: $$\Lambda \mu$$-calculus is an extension of Parigot’s $$\lambda \mu$$-calculus which (i) satisfies the separation theorem: it is Böhm-complete, (ii) corresponds to CBN delimited control and (iii) is provided with a stream interpretation.
In the present paper, we study solvability and investigate Böhm trees for $$\Lambda \mu$$-calculus. Moreover, we make clear the connections between $$\Lambda \mu$$-calculus and infinitary $$\lambda$$-calculi. After establishing a standardization theorem for $$\Lambda \mu$$-calculus, we characterize solvability. Then, we study infinite $$\Lambda \mu$$-Böhm trees, which are Böhm-like trees for $$\Lambda \mu$$-calculus; this allows to strengthen the separation results that we established previously for $$\Lambda \mu$$-calculus and to shed a new light on the failure of separation in Parigot’s original $$\lambda \mu$$-calculus.
Our construction clarifies $$\Lambda \mu$$-calculus both as an infinitary calculus and as a core language for dealing with streams as primitive objects.
For the entire collection see [Zbl 1186.68003].

### MSC:

 68N18 Functional programming and lambda calculus 03B40 Combinatory logic and lambda calculus
Full Text: