Termination of Narrowing: Automated Proofs and Modularity Properties
José Iborra López · 2010
ResumenEn 1936 Alan Turing demostró que el halting problem, esto es, el problema de decidir si un programa termina o no, es un problema indecidible para la inmensa mayoría de los lenguajes de programación.A pesar de ello, la terminación es un problema tan relevante que en las últimas décadas un gran número de técnicas han sido desarrolladas para demostrar la terminación de forma automática de la máxima cantidad posible de programas.Los sistemas de reescritura de términos proporcionan un marco teórico abstracto perfecto para el estudio de la terminación de programas.En este marco, la evaluación de un término consiste en la aplicación no determinista de un conjunto de reglas de reescritura.El estrechamiento (narrowing) de términos es una generalización de la reescritura que proporciona un mecanismo de razonamiento automático.Por ejemplo, dado un conjunto de reglas que definan la suma y la multiplicación, la reescritura permite calcular expresiones aritméticas, mientras que el estrechamiento permite resolver ecuaciones con variables.Esta tesis constituye el primer estudio en profundidad de las propiedades de terminación del estrechamiento.Las contribuciones son las siguientes.En primer lugar, se identifican clases de sistemas en las que el estrechamiento tiene un comportamiento bueno, en el sentido de que siempre termina.Muchos métodos de razonamiento automático, como el análisis de la semántica de lenguajes de programación mediante operadores de punto fijo, se benefician de esta caracterización.En segundo lugar, se introduce un método automático, basado en el marco teórico de pares de dependencia, para demostrar la terminación del estrechamiento en un sistema particular.Nuestro método es, por primera vez, aplicable a cualquier clase de sistemas.En tercer lugar, se propone un nuevo método para estudiar la terminación del estrechamiento desde un término particular, permitiendo el análisis de la terminación de lenguajes de programación.El nuevo método generaliza los métodos existentes de manera fundamental, gracias a lo cual se puede estudiar la terminación de lenguajes de programación lógicos a través de la terminación del estrechamiento, algo que hasta ahora no era posible con los métodos existentes.En cuarto lugar, se analiza detalladamente la modularidad de la terminación del estrechamiento.Esto es, si los sistemas A y B son terminantes, en qué casos el sistema unión es terminante.La modularidad tiene implicaciones directas en muchas de las aplicaciones del estrechamiento.En concreto desarrollamos el caso de la resolución de ecuaciones simbólicas cuando se combinan varios sistemas ecuacionales.Además, las técnicas automáticas de la segunda y tercera contribución han sido implementadas en nuestra herramienta de demostración de la terminación del estrechamiento, Narradar. ResumEn 1936 Alan Turing va demostrar que el halting problem, és a dir, el problema de decidir si un programa acaba o no, és un problema indecidible per a la immensa majoria dels llenguatges de programació.Tot i això, la terminació és un problema tan rellevant que en les últimes dècades s'ha desenvolupat una gran nombre de técniques per a demostrar la terminació de la màxima quantitat de programes possible de manera automàtica.Els sistemes de reescriptura de termes proporcionen un marc teòric abstracte perfecte per a la caracterizació de les propietats de terminació de programes.En aquest marc, l'avaluació d'un terme consisteix en l'aplicació no determinista d'un conjunt de regles de reescriptura.L'estretiment (narrowing) de termes és una generalització de la reescriptura que proporciona un mecanisme de raonament automàtic.Per exemple, donat un conjunt de regles que definisquen la suma i la multiplicació dels naturals, la reescriptura permet calcular expressions aritmètiques, mentre que l'estretiment permet resoldre equacions amb variables.Aquesta tesi constitueix el primer estudi en profunditat de les propietats de terminació de l'estretiment.Les contribucions són les següents.En primer lloc, s'identifiquen classes de sistemes en què l'estretiment té un comportament bo, en el sentit que sempre acaba.Molts mètodes de raonament automàtic, como l'anàlisi de les propietats de programes basat en una semàntica computada per mitjà de narrowing, es beneficien d'aquesta caracterització.En segon lloc, s'introdueix un mètode automàtic, basat en el marc teòric de parells de dependència, per a demostrar la terminació de l'estretiment en un sistema particular.El nostre mètode es, por primera volta, aplicable a qualsevol classe de sistemes.En tercer lloc, es proposa un nou mètode per l'estudi de la terminació de l'estretiment des d'un terme particular, cosa que permet l'anàlisi de la terminació de programes.El nostre mètode generalitza els mètodes existents de manera fonamental.Gràcies a això, es pot estudiar la terminació de llenguatges de programació lògics a través de la terminació de l'estretiment, un fet que fins ara no era possible amb els mètodes que hi havia.En quart lloc, s'analitza detalladament la modularitat de la terminació de l'estretiment.Això és, si els sistemes A i B són terminants, en què casos el sistema unió és terminant.La modularitat té implicacions directes en moltes de les aplicacions de l'estretiment.En concret, desenvolupem el cas de la resolució de equacions simbòliques quan es combinen diversos sistemes equacionals.A més, les tècniques automàtiques de la segona i tercera contribució han sigut implementades en la nostra eina de demostració de la terminació de l'estretiment, Narradar.First of all, I would like to thank María Alpuente for her help, guidance and patience during these years.It was a pleasure to work with her.I am also equally thankful to Santiago Escobar; from him I finally learnt the foundations of research during long blackboard sessions in the summer of 2007.Most of the work in this thesis is directly or indirectly due to them.Gracias María !Gracias Santi !During these years I was fortunate to have German Vidal at only two doors distance.He has devoted so much time to helping me when I struggled, that probably this thesis wouldn't exist if he hadn't been there.I was also privileged to be sharing the laboratory with Raúl Gutierrez.How many times has he helped with a technical question.have we sketched ideas over a blackboard, shared interesting references, or designed algorithms for our implementations on the way to lunch.He also kindly proofreaded parts of this thesis.