MOVES Seminar, 29 August 2008
Automatic Termination Analysis of Context-Sensitive Term Rewrite Systems
Fabian Emmes
Abstract:
Context-sensitive rewrite systems (a generalized form of term rewrite systems) are used to model the evaluation of lazy programming languages.
This talk demonstrates a contemporary approach to prove if these systems are terminating (i.e., will never compute infinitely many consecutive steps). In contrast to the traditional approach of transforming these systems to ordinary term rewrite systems, we show how one can use dependency pair techniques directly on context-sensitive rewrite systems. Many ideas used in the dependency pairs framework also hold for, or can be extended to, these systems. In particular techniques that transform the dependency pairs become much more powerful in the contextsensitive setting. Concluding the talk it is shown that this new approach to handle contextsensitive termination analysis yields much better results in practice then any other published approach.
Fabian Emmes
Abstract:
Context-sensitive rewrite systems (a generalized form of term rewrite systems) are used to model the evaluation of lazy programming languages.
This talk demonstrates a contemporary approach to prove if these systems are terminating (i.e., will never compute infinitely many consecutive steps). In contrast to the traditional approach of transforming these systems to ordinary term rewrite systems, we show how one can use dependency pair techniques directly on context-sensitive rewrite systems. Many ideas used in the dependency pairs framework also hold for, or can be extended to, these systems. In particular techniques that transform the dependency pairs become much more powerful in the contextsensitive setting. Concluding the talk it is shown that this new approach to handle contextsensitive termination analysis yields much better results in practice then any other published approach.
