Decidable Approximations of Sets of Descendants and Sets of Normal Forms - extended versionReportar como inadecuado




Decidable Approximations of Sets of Descendants and Sets of Normal Forms - extended version - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 PROTHEO - Constraints, automatic deduction and software properties proofs INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

Abstract : We present here decidable approximations of sets of descendants and sets of normal forms of Term Rewriting Systems, based on specific tree automata techniques. In the context of rewriting logic, a Term Rewriting System is a program, and a normal form is a result of the program. Thus, approximations of sets of descendants and sets of normal forms provide tools for analysing a few properties of programs: we show how to compute a superset of results, to prove the sufficient completeness property, or to find a criterion for proving termination under a specific strategy, the sequential reduction strategy.

Keywords : term rewriting program verification normal forms descendants tree automata approximation sufficient completeness reachability termination





Autor: Thomas Genet -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados