Algebraic Notions of Termination

in: Universität Augsburg Technical Report, Institute of Computer Science, University of Augsburg, October 2006

Abstract:
Five algebraic notions of termination are formalised, analysed and compared: well-foundedness or Noetherity, Löb's formula, absence of infinite iteration, absence of divergence and normalisation. The study is based on modal semirings, which are additively idempotent semirings with forward and backward modal operators. To reason about infinite behaviour, semirings are extended to divergence semirings, divergence Kleene algebras and omega algebras. The resulting notions and techniques are used in calculational proofs of classical theorems of rewriting theory. These applications show that modal semirings are powerful tools for reasoning algebraically about the finite and infinite behaviour of programs and state transition systems.

Downloads:

• Algebraic Notions of Termination  -  (tr-2006-23_des_moe_str.pdf, 710 KB)