Tesis doctoral de Beatriz Alarcón Jiménez
Maude is a declarative programming language based on rewriting logic that incorporates many features that in order to prove certain computational properties lead to difficulties. the task of proving termination of rewrite systems in indeed quite hard but applied to real programming languages, becomes more complicated due to these inherent features. therefore, methods for proving termination of such programs require specific techniques and a careful analysis. several papers have studied how to prove termination of (a subset of) maude programs. However, all of them follow a transformational approach where the original program is transformed until it reaches a rewrite system that can be managed with existing techniques and termination tools. in practice, the fact of transforming the original systems used to complicate the proof of termination since it introduces new symbols and rules in the system. in this thesis, we tackle the problem of proving termination of (a subset of) maude programs by means of direct methods. on the one hand, we pay attention to the strategy of maude. Maude is an eager language where the arguments of a function are always evaluated before the application of the function that uses them. This strategy (known as call by value) can lead to nontermination if programs are not written carefully. for this reason, maude (specifically) incorporates mechanisms to control the program execution such as syntactic annotations, which are associated to arguments of symbols. In rewriting, this strategy is known as innermost context-sensitive rewriting. on the other hand, maude also incorporates the possibility of declaring attributes. semantically, declaring a set of equational attributes for an operator is equivalent to declaring the corresponding equations for the operator; however, it avoids termination problems and leads to a more efficient evaluation. the effect of declaring equational attributes is to compute with equivalence classes modulo these equations. the dependency pair framework develops the idea of an incremental application of different termination techniques for solving termination problems. It has shown to be a powerful and efficient way to prove termination of rewriting automatically. In this thesis, we deal with termination of innermost context-sensitive rewriting and of rewriting modulo specific axioms by extending the dependency pair framework.
Datos académicos de la tesis doctoral «Towards a framework for proving termination of maude programs«
- Título de la tesis: Towards a framework for proving termination of maude programs
- Autor: Beatriz Alarcón Jiménez
- Universidad: Politécnica de Valencia
- Fecha de lectura de la tesis: 26/05/2011
Dirección y tribunal
- Director de la tesis
- Salvador Lucas Alba
- Tribunal
- Presidente del tribunal: María Alpuente frasnedo
- claude Marché (vocal)
- bernhard Gramlich (vocal)
- pierre Lescanne (vocal)