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


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