| 作成者 |
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 出版タイプ |
|
| アクセス権 |
|
| 関連DOI |
|
|
|
| 関連URI |
|
|
|
| 関連情報 |
|
|
|
| 概要 |
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.続きを見る
|
Mendeley出力
trcs177
trcs177.ps