Proving Infinitary Normalization Export

@incollection{endrullis-grabmayer-hendriks-klop-de-vrijer-09, abstract = {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.}, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan and de Vrijer, Roel}, booktitle = {Types for Proofs and Programs}, citeulike-article-id = {6089237}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-02444-3_5}, citeulike-linkout-1 = {http://www.springerlink.com/content/t7txxgj577q28058}, doi = {10.1007/978-3-642-02444-3_5}, journal = {Types for Proofs and Programs}, keywords = {infinitary-rewriting, master-project, normalization, rewriting}, pages = {64--82}, posted-at = {2009-11-09 15:44:24}, priority = {2}, publisher = {Springer Berlin / Heidelberg}, series = {Lecture Notes in Computer Science}, title = {Proving Infinitary Normalization}, url = {http://dx.doi.org/10.1007/978-3-642-02444-3_5}, year = {2009} }

TY - CHAP ID - endrullis-grabmayer-hendriks-klop-de-vrijer-09 L3 - citeulike-article-id:6089237 N2 - 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. JF - Types for Proofs and Programs SE - Lecture Notes in Computer Science EP - 82 TI - Proving Infinitary Normalization PB - Springer Berlin / Heidelberg T2 - Types for Proofs and Programs SP - 64 KW - infinitary-rewriting KW - master-project KW - normalization KW - rewriting AU - Endrullis, Jörg AU - Grabmayer, Clemens AU - Hendriks, Dimitri AU - Klop, Jan AU - de Vrijer, Roel PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-642-02444-3_5 ER -