Author name cluster

Johannes Waldmann

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.

4 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

TCS Journal 2004 Journal Article

Deleting string rewriting systems preserve regularity

Dieter Hofbauer
Johannes Waldmann

A string rewriting system is called deleting if there exists a partial ordering on its alphabet such that each letter in the right-hand side of a rule is less than some letter in the corresponding left-hand side. We show that the rewrite relation induced by a deleting system can be represented as the composition of a finite substitution (into an extended alphabet), a rewrite relation of an inverse context-free system (over the extended alphabet), and a restriction (to the original alphabet). Here, a system is called inverse context-free if the length of the right-hand side of any rule does not exceed one. The decomposition result directly implies that deleting systems preserve regularity, and that inverse deleting systems preserve context-freeness. The latter result was already obtained by Hibbard (J. ACM 21(3) (1974) 446–453).

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 2000 Journal Article

The Combinator S

Johannes Waldmann

The combinator S has the reduction rule S xyz→xz(yz). We investigate properties of ground terms built from S alone. The first part of the paper shows that this term rewriting system admits no ground loops. This extends the known result of the absence of cycles. In the second part, we give a procedure that decides whether an S-term has a normal form. This algorithm makes use of rational tree languages. Finally we show that the set of normalizing S-terms is in itself a rational tree language, by explicitly giving its grammar. In all, this paper shows the surprisingly rich structures that are implied by a seemingly small rewrite rule.

Details DOI