En 1936 Alan Turing demostro que el halting problem, esto es, el problema de decidir
si un programa termina o no, es un problema indecidible para la inmensa mayoria de
los lenguajes de programacion. A pesar de ello, la terminacion es un problema tan
relevante que en las ultimas decadas un gran numero de tecnicas han sido desarrolladas
para demostrar la terminacion de forma automatica de la maxima cantidad posible de
programas. Los sistemas de reescritura de terminos proporcionan un marco teorico
abstracto perfecto para el estudio de la terminacion de programas. En este marco, la
evaluaci on de un t ermino consiste en la aplicacion no determinista de un conjunto de
reglas de reescritura.
El estrechamiento (narrowing) de terminos es una generalizacion de la reescritura
que proporciona un mecanismo de razonamiento automatico. Por ejemplo, dado un
conjunto de reglas que denan la suma y la multiplicacion, la reescritura permite calcular
expresiones aritmeticas, mientras que el estrechamiento permite resolver ecuaciones
con variables. Esta tesis constituye el primer estudio en profundidad de las
propiedades de terminacion del estrechamiento. Las contribuciones son las siguientes.
En primer lugar, se identican clases de sistemas en las que el estrechamiento tiene
un comportamiento bueno, en el sentido de que siempre termina. Muchos metodos
de razonamiento automatico, como el analisis de la semantica de lenguajes de programaci
on mediante operadores de punto jo, se benefician de esta caracterizacion.
En segundo lugar, se introduce un metodo automatico, basado en el marco teorico
de pares de dependencia, para demostrar la terminacion del estrechamiento en un
sistema particular. Nuestro metodo es, por primera vez, aplicable a cualquier clase
de sistemas.
En tercer lugar, se propone un nuevo metodo para estudiar la terminacion del
estrechamiento desde un termino particular, permitiendo el analisis de la terminacion
de lenguajes de programacion. El nuevo metodo generaliza los / Iborra López, J. (2010). Termination of Narrowing: Automated Proofs and Modularity Properties [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/19251
| Identifer | oai:union.ndltd.org:upv.es/oai:riunet.upv.es:10251/19251 |
| Date | 11 February 2013 |
| Creators | Iborra López, José |
| Contributors | Alpuente Frasnedo, María, Escobar Román, Santiago, Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació |
| Publisher | Universitat Politècnica de València |
| Source Sets | Universitat Politècnica de València |
| Language | English |
| Detected Language | Spanish |
| Type | info:eu-repo/semantics/doctoralThesis, info:eu-repo/semantics/acceptedVersion |
| Source | Riunet |
| Rights | http://rightsstatements.org/vocab/InC/1.0/, info:eu-repo/semantics/openAccess |
Page generated in 0.0022 seconds