- -

Termination of Narrowing: Automated Proofs and Modularity Properties

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Termination of Narrowing: Automated Proofs and Modularity Properties

Show simple item record

Files in this item

dc.contributor.advisor Alpuente Frasnedo, María es_ES
dc.contributor.advisor Escobar Román, Santiago es_ES
dc.contributor.author Iborra López, José es_ES
dc.date.accessioned 2013-02-11T07:27:13Z
dc.date.available 2013-02-11T07:27:13Z
dc.date.created 2010-10-13T22:00:00Z es_ES
dc.date.issued 2013-02-11T07:27:08Z es_ES
dc.identifier.uri http://hdl.handle.net/10251/19251
dc.description.abstract 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 es_ES
dc.language Inglés es_ES
dc.rights Reserva de todos los derechos es_ES
dc.source Riunet es_ES
dc.subject Razonamiento automático es_ES
dc.subject Terminación es_ES
dc.subject Programación lógica es_ES
dc.subject Programación funcional es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Termination of Narrowing: Automated Proofs and Modularity Properties
dc.type Tesis doctoral es_ES
dc.identifier.doi 10.4995/Thesis/10251/19251 es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Iborra López, J. (2010). Termination of Narrowing: Automated Proofs and Modularity Properties [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/19251 es_ES
dc.description.accrualMethod Palancia es_ES
dc.type.version info:eu-repo/semantics/acceptedVersion es_ES
dc.relation.tesis 3392 es_ES


This item appears in the following Collection(s)

Show simple item record