| Creator |
|
|
|
|
|
| Language |
|
| Publisher |
|
|
|
| Date |
|
| Source Title |
|
| Vol |
|
| Publication Type |
|
| Access Rights |
|
| Related DOI |
|
|
|
| Related URI |
|
|
|
| Relation |
|
|
|
| Abstract |
Typed λμ-calculus is known to be strongly normalizing and weakly Church-Rosser, and hence confluent. In fact, Parigot formulated a parallel reduction to prove confluency of typed λμ-calculus by "Tait-...and- Martin-Löf" method. However, the diamond property does not hold for his parallel reduction. The confluency for type-free λμ-calculus cannot be derived from that of typed λμ-calculus and is not known. We analyzed granualities of the reduction rules. We consider a renaming and consecutive structural reductions as one step parallel reduction, and show that the new formulation of parallel reduction has the diamond property, which yields the correct proof of confluency of type free λμ-calculus. The diamond property of new parallel reduction is also shown for the call-by-value version of λμ-calculus contains the symmetric structural reduction rule.show more
|
Export Mendeley
trcs177
trcs177.ps