Proving Infinitary Normalization
| 详细信息 | 推荐本文 | |
- 作者：J枚rg Endrullis ; Clemens Grabmayer ; Dimitri Hendriks ; Jan Willem Klop ; Roel de Vrijer
- 刊名：Lecture Notes in Computer Science
- 出版时间：2009
- 出版年：2009
- 期刊代码：99_0302-9743
- 类别：cp
- 卷：5497
- 期：1
- 页码：64-82
- 数据来源：sp
摘要
We investigate the notion of ‘infinitary strong normalization’ (SN ∞ ), introduced in [6], the analogue of termination when rewriting infinite terms. A (possibly infinite) term is SN ∞ if along every rewrite sequence each fixed position is rewritten only finitely often. In [9], SN ∞ has been investigated as a system-wide property, i.e. SN ∞ for all terms of a given rewrite system. This global property frequently fails for trivial reasons. For example, in the presence of the collapsing rule tail(x:σ)→σ, the infinite term t =tail(0:t) rewrites to itself only. Moreover, in practice one usually is interested in SN ∞ of a certain set of initial terms. We give a complete characterization of this (more general) ‘local version’ of SN ∞ using interpretations into weakly monotone algebras (as employed in [9]). Actually, we strengthen this notion to continuous weakly monotone algebras (somewhat akin to [5]). We show that tree automata can be used as an automatable instance of our framework; an actual implementation is made available along with this paper.