<学術雑誌論文>
Parallel Reduction in Type Free Lambda-mu-Calculus

作成者
本文言語
出版者
発行日
収録物名
開始ページ
終了ページ
出版タイプ
アクセス権
関連DOI
関連URI
関連情報
概要 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 type...d 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.続きを見る

本文ファイル

pdf BHF01 pdf 152 KB 406  

詳細

レコードID
査読有無
登録日 2010.12.21
更新日 2020.11.27

この資料を見た人はこんな資料も見ています