Automatic proofs of termination of context-sensitive rewriting
Raúl Gutiérrez Gil · Dialnet (Universidad de la Rioja) · 2010
La idea de aplicar de forma incremental diferentes tecnicas de terminacion encapsuladas como procesadores con el objetivo de resolver problemas de terminacion se est'a mostrando como una t'ecnica eficiente y potente de probar la terminacion de la reescritura. Hoy en dia, el marco de pares de dependencia (que desarrolla esta idea) es la aproximacion mas exitosa para probar la terminacion de la reescritura. El marco de pares de dependencia utiliza la nocion de par de dependencia para descomponer un problema de terminacion en un conjunto de problemas de pares de dependencia. Estos problemas de pares de dependencia pueden ser tratados de manera independiente aplicando diferentes procesadores de pares de dependencia. Si conseguimos probar la finitud de todos los problemas de terminacion, entonces podemos asegurar que el sistema es terminante. Si conseguimos refutar la finitud de alguno de los problemas de terminacion, entonces podemos asegurar que el sistema es no-terminante. Este sencillo y a la par potente esquema es la base del estado del arte de las herramientas que prueban de forma automatica la terminiacion de la reescritura. La reescritura sensible al contexto [Luc98, Luc02] es una restriccion de la reescritura que prohibe las reducciones de algunas subexpresiones y que se ha demostrado que es util para modelar y analizar propiedades de los lenguajes de programacion a distintos niveles. En particular, la terminacion de la reescritura sensible al contexto es util para analizar y probar la terminacion de programas en varios lenguajes de programacion y variantes de sistemas de reescritura de terminos. En los ultimos quince anos se han desarrollado y programado muchas tecnicas para probar la terminacion de la reescritura sensible al contexto (fundamentalmente transformaciones y ordenes). Sin embargo, la definicion de par de dependencia sensible al contexto y de su marco comenzo solo hace unos cuatro anos, cuando se inicio el desarrollo de esta tesis. En esta tesis mostramos como desarrollar un marco de pares de dependencia para probar la terminacion de la reescritura sensible al contexto y mostramos resultados experimentales de las ventajas del marco de pares de dependencia sensible al contexto en el desarrollo de herramientas para probar automaticamente la terminacion de la reescitura sensible al contexto.