Parallel reduction in type free lambda/mu-calculus. (English) Zbl 0971.68019

Fidge, Colin (ed.), Computing: The Australasian Theory Symposium, CATS 2001. Proceedings of the 7th symposium, Bond Univ., Gold Coast, Australia, January 29-30, 2001. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 42, 15 p., electronic only (2001).
Summary: The typed lambda/mu-calculus is known to be strongly normalizing and weakly Church-Rosser, and hence becomes confluent. In fact, Parigot formulated a parallel reduction to prove confluence of the typed lambda/mu-calculus by ‘Tait-and-Martin-Löf’ method. However, the diamond property does not hold for his parallel reduction. The confluence for type-free lambda/mu-calculus cannot be derived from that of the typed lambda/mu-calculus and is not confirmed yet as far as we know. We analyze granularity of the reduction rules, and then introduce a new parallel reduction such that both renaming reduction and consecutive structural reductions are considered as one step parallel reduction. It is shown that the new formulation of parallel reduction has the diamond property, which yields a correct proof of the confluence for type free lambda/mu-calculus. The diamond property of the new parallel reduction is also applicable to a call-by-value version of the lambda/mu-calculus containing the symmetric structural reduction rule.
For the entire collection see [Zbl 0957.00045].


68N18 Functional programming and lambda calculus
Full Text: Link