CARIBOO : A Multi-Strategy Termination Proof Tool Based on Induction
Olivier Fissore, Isabelle Gnaedig, Claude Kirchner · 2003
1 A termination proof tool for rule-based programs CARIBOO is a termination proof tool for rule-based programming languages, where a program is a rewrite system and query evaluation consists in rewriting a ground expression [3]. It applies to languages such as ASF+SDF, Maude, Cafe-OBJ, or ELAN. By contrast with most of the existing tools, which prove in general termination of standard rewriting (rewriting without strategy) on the free term algebra, our proof tool, named CARIBOO (for Computing AbstRaction for Induction Based termination prOOfs), allows proving termination under specific reduction strategies, which becomes of special interest when the computations diverge for standard rewriting. It deals in particular with: the innermost strategy, specially useful when the rule-based formalism expresses functional programs, and central in the evaluation process of ELAN, local strategies on operators, provided in OBJ-like languages, and allowing to control evaluation strategies in a very fine local way, the outermost strategy, useful to avoid evaluations known to be non terminating for the standard strategy, to make strategy computations shorter, and used for interpreters and compilers using call by name. 2 Proving termination by explicit induction