Author name cluster

Alfons Geser

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

I&C Journal 2007 Journal Article

On tree automata that certify termination of left-linear term rewriting systems

Alfons Geser
Dieter Hofbauer
Johannes Waldmann
Hans Zantema

We present a new method for automatically proving termination of left-linear term rewriting systems on a given regular language of terms. It is a generalization of the match bound method for string rewriting. To prove that a term rewriting system terminates we first construct an enriched system over a new signature that simulates the original derivations. The enriched system is an infinite system over an infinite signature, but it is locally terminating: every restriction of the enriched system to a finite signature is terminating. We then construct iteratively a finite tree automaton that accepts the enriched given regular language and is closed under rewriting modulo the enriched system. If this procedure stops, then the enriched system is compact: every enriched derivation involves only a finite signature. Therefore, the original system terminates. We present two methods to construct the enrichment: roof heights for left-linear systems, and match heights for linear systems. For linear systems, the method is strengthened further by a forward closure construction. Using these methods, we give examples for automated termination proofs that cannot be obtained by standard methods.

Details DOI

MFCS Conference 2003 Conference Paper

Match-Bounded String Rewriting Systems

Alfons Geser
Dieter Hofbauer
Johannes Waldmann

Abstract We investigate rewriting systems on strings by annotating letters with natural numbers, so called match heights. A position in a reduct will get height h +1 if the minimal height of all positions in the redex is h. In a match-bounded system, match heights are globally bounded. Exploiting recent results on deleting systems, we prove that it is decidable whether a given rewriting system has a given match bound. Further, we show that match-bounded systems preserve regularity of languages. Our main focus, however, is on termination of rewriting. Match-bounded systems are shown to be linearly terminating, and–more interestingly–for inverses of match-bounded systems, termination is decidable. These results provide new techniques for automated proofs of termination.

Details

I&C Journal 2002 Journal Article

Relative Undecidability in Term Rewriting

Alfons Geser
Aart Middeldorp
Enno Ohlebusch
Hans Zantema

For a hierarchy of properties of term rewriting systems related to confluence we prove relative undecidability, i. e. , for implications X⇒Y in the hierarchy the property X is undecidable for term rewriting systems satisfying Y. For some of the implications either X or ¬X is semi-decidable, for others neither X nor ¬X is semi-decidable. We prove most of these results for linear term rewrite systems.

Details DOI

I&C Journal 2002 Journal Article

Relative Undecidability in Term Rewriting

Alfons Geser
Aart Middeldorp
Enno Ohlebusch
Hans Zantema

For a hierarchy of properties of term rewriting systems related to termination we prove relative undecidability: For implications X⇒Y in the hierarchy the property X is undecidable for term rewriting systems satisfying Y. For most implications we obtain this result for term rewriting systems consisting of a single rewrite rule.

Details DOI

TCS Journal 2000 Journal Article

On normalizing, non-terminating one-rule string rewriting systems

Alfons Geser

We prove that the one-rule string rewriting system 1010→010110 is normalizing, i. e. admits for every string a reduction to normal form, but non-terminating, i. e. there are infinite reductions as well. Moreover, we prove that this is the smallest such system. Whereas 1010→010110 is rightmost terminating, i. e. no infinite rightmost reductions exist, the normalizing system 12013→0160 is neither leftmost terminating nor rightmost terminating. In the discourse, we introduce a few methods to prove or disprove normalization for non-terminating string rewriting systems.

Details DOI

CSL Conference 1997 Conference Paper

Relative Undecidability in Term Rewriting

Alfons Geser
Aart Middeldorp
Enno Ohlebusch
Hans Zantema

Abstract For two hierarchies of properties of term rewriting systems related to confluence and termination, respectively, we prove relative undecidability: for implications X⇒Y in the hierarchies the property X is undecidable for term rewriting systems satisfying Y.

Details