|
|
JAIST Repository >
b. 情報科学研究科・情報科学系 >
b10. 学術雑誌論文等 >
b10-1. 雑誌掲載論文 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/5032
|
| タイトル: | Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems |
| 著者: | Khasidashvili, Zurab
Ogawa, Mizuhito
Oostrom, Vincent van |
| 発行日: | 2001-01-10 |
| 出版者: | Academic Press(Elsevier) |
| 誌名: | Information and Computation |
| 巻: | 164 |
| 号: | 1 |
| 開始ページ: | 118 |
| 終了ページ: | 151 |
| DOI: | 10.1006/inco.2000.2888 |
| 抄録: | We study perpetuality of reduction steps, as well as perpetuality of redexes, in orthogonal rewrite systems. A perpetual step is a reduction step which retains the possibility of infinite reductions. A perpetual redex is a redex which, when put into an arbitrary context, yields a perpetual step. We generalize and refine existing criteria for the perpetuality of reduction steps and redexes in orthogonal Term Rewriting Systems and the λ-calculus due to Bergstra and Klop and others. We first introduce Context-sensitive Conditional Expression Reduction Systems (CCERSs) and define a concept of orthogonality (which implies confluence) for them. In particular, several important λ-calculi and their extensions and restrictions can naturally be embedded into orthogonal CCERSs. We then define a perpetual reduction strategy which enables one to construct minimal (w.r.t. Levy's permutation ordering on reductions) infinite reductions in orthogonal fully-extended CCERSs. Using the properties of the minimal perpetual strategy, we prove 1. perpetuality of any reduction step that does not erase potentially infinite arguments, which are arguments that may become, via substitution, infinite after a number of outside steps, and 2. perpetuality (in every context) of any safe redex, which is a redex whose substitution instances may discard infinite arguments only when the corresponding contracta remain infinite. We prove both these perpetuality criteria for orthogonal fully-extended CCERSs and then specialize and apply them to restricted λ-calculi, demonstrating their usefulness. In particular, we prove the equivalence of weak and strong normalization (which equivalence is here called uniform normalization) for various restricted λ-calculi, most of which cannot be derived from previously known perpetuality criteria. |
| Rights: | NOTICE: This is the author's version of a work accepted for publication by Academic Press(Elsevier). Zurab Khasidashvili, Mizuhito Ogawa, Vincent van Oostrom, Information and Computation, 164(1), 2001, 118-151, http://dx.doi.org/10.1006/inco.2000.2888 |
| URI: | http://hdl.handle.net/10119/5032 |
| 資料タイプ: | author |
| 出現コレクション: | b10-1. 雑誌掲載論文 (Journal Articles)
|
このアイテムのファイル:
| ファイル |
記述 |
サイズ | 形式 |
|---|
| C2249.pdf | | 530Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|
