TY - JOUR

T1 - Parallel reduction in type free λμ-calculus

AU - Baba, Kensuke

AU - Hirokawa, Sachio

AU - Fujita, Ken Etsu

PY - 2001/1

Y1 - 2001/1

N2 - The typed λμ-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 λμ-calculus by "Tait-and-Martin-Löf" method. However, the diamond property does not hold for his parallel reduction. The confluence for type-free λμ-calculus cannot be derived from that of the typed λμ-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 λμ-calculus. The diamond property of the new parallel reduction is also applicable to a call-by-value version of the λμ-calculus containing the symmetric structural reduction rule.

AB - The typed λμ-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 λμ-calculus by "Tait-and-Martin-Löf" method. However, the diamond property does not hold for his parallel reduction. The confluence for type-free λμ-calculus cannot be derived from that of the typed λμ-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 λμ-calculus. The diamond property of the new parallel reduction is also applicable to a call-by-value version of the λμ-calculus containing the symmetric structural reduction rule.

UR - http://www.scopus.com/inward/record.url?scp=18944407167&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=18944407167&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)80878-8

DO - 10.1016/S1571-0661(04)80878-8

M3 - Conference article

AN - SCOPUS:18944407167

VL - 42

SP - 52

EP - 66

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

T2 - Computing: The Australasian Theory Symposium (CATS 2001)

Y2 - 29 January 2001 through 30 January 2001

ER -