Automatic proofs of termination of context-sensitive rewriting

• Autores: Raúl Gutiérrez Gil
• Directores de la Tesis: Salvador Lucas Alba (dir. tes.)
• Lectura: En la Universitat Politècnica de València ( España ) en 2010
• Idioma: inglés
• Tribunal Calificador de la Tesis: María Alpuente Frasnedo (presid.) , Albert Rubio Gimeno (secret.) , Bernhard Gramlich (voc.) , Aart Middeldorp (voc.) , Pierre Lescanne (voc.)
• Enlaces
  • Tesis en acceso abierto en: TESEO
• Resumen

  • La idea de aplicar de forma incremental diferentes técnicas de terminación encapsuladas como procesadores con el objetivo de resolver problemas de terminación se est'a mostrando como una t'ecnica eficiente y potente de probar la terminación de la reescritura. Hoy en día, el marco de pares de dependencia (que desarrolla esta idea) es la aproximación más exitosa para probar la terminación de la reescritura. El marco de pares de dependencia utiliza la noción de par de dependencia para descomponer un problema de terminación 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 terminación, entonces podemos asegurar que el sistema es terminante. Si conseguimos refutar la finitud de alguno de los problemas de terminación, 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 automática la terminiación de la reescritura.

    La reescritura sensible al contexto [Luc98, Luc02] es una restricción de la reescritura que prohíbe las reducciones de algunas subexpresiones y que se ha demostrado que es útil para modelar y analizar propiedades de los lenguajes de programación a distintos niveles. En particular, la terminación de la reescritura sensible al contexto es útil para analizar y probar la terminación de programas en varios lenguajes de programación y variantes de sistemas de reescritura de terminos. En los últimos quince años se han desarrollado y programado muchas técnicas para probar la terminación de la reescritura sensible al contexto (fundamentalmente transformaciones y órdenes). Sin embargo, la definición de par de dependencia sensible al contexto y de su marco comenzó sólo hace unos cuatro años, cuando se inició el desarrollo de esta tesis.

    En esta tesis mostramos como desarrollar un marco de pares de dependencia para probar la terminación 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 automáticamente la terminación de la reescitura sensible al contexto.