Titlebook: Rewriting Techniques and Applications; 12th International C Aart Middeldorp Conference proceedings 2001 Springer-Verlag Berlin Heidelberg 2

ODIUM

Dependency Pairs for Equational Rewritingrary non-collapsing equations (satisfying a certain linearity condition). With the proposed approach, it is now possible to perform automated termination proofs for many systems where this was not possible before. In other words, the power of dependency pairs can now also be used for rewriting modulo equations.

CAB

Termination Proofs by Context-Dependent Interpretationsofs by interpretations that can avoid this drawback of the traditional approach. A number of simple examples illustrate how to achieve tight or even optimal bounds on the derivation height. The method is general enough to capture cases where simplification orderings fail.

减去

Relating Accumulative and Non-accumulative Functional Programs of functional programs, namely restricted 2-modular tree transducers, to which it can be applied. Moreover, since we get macro tree transducers as transformation result and since we also give the inverse transformation algorithm, we have a new characterization for the class of functions induced by macro tree transducers.

爵士乐

繁忙

脱水

噱头

Omnipotent

Opponent

Beta Reduction Constraintsconstraints to describe beta reduction steps between partially known lambda terms. We show that beta reduction constraints can be expressed in an extension of CLLS by group parallelism. We then extend a known semi-decision procedure for CLLS to also deal with group parallelism and thus with beta-red

间接

From Higher-Order to First-Order Rewritingof higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty theory (that is, ε = 0). This class includes of course the λ-calculus. Our technique does not rely on a particular substitution calculus but on a set of abstract properties to be verified by the substitut