<テクニカルレポート>
Parallel Reduction in Type Free λμ-Calculus

作成者
本文言語
出版者
発行日
雑誌名
出版タイプ
アクセス権
概要 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.続きを見る

本文情報を非表示

trcs177 pdf 202 KB 58  
trcs177.ps gz 57.3 KB 29  

詳細

レコードID
査読有無
関連情報
タイプ
登録日 2007.04.21
更新日 2017.01.20