Abstract
Abstraction can be used very effectively to decompose and simplify termination arguments. If a symbolic computation is nonterminating, then there is an infinite computation with a top redex, such that all redexes are immortal, but all children of redexes are mortal. This suggests applying weakly-monotonic well-founded relations in abstraction-based termination methods, expressed here within an abstract framework for term-based proofs. Lexicographic combinations of orderings may be used to match up with multiple levels of abstraction. © Springer-Verlag 2004.
Cite
CITATION STYLE
Dershowitz, N. (2004). Termination by abstraction. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3132, 1–18. https://doi.org/10.1007/978-3-540-27775-0_1
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
