Higher-order semantic labelling for inductive datatype systems

9 years 4 months ago
Higher-order semantic labelling for inductive datatype systems
We give a novel transformation for proving termination of higher-order rewrite systems in the format of Inductive Data Type Systems (IDTSs) by Blanqui, Jouannaud and Okada. The transformation called higher-order semantic labelling attaches algebraic semantics of the arguments to each function symbol. We systematically define the labelling and show that labelled systems give termination models in the framework of Fiore, Plotkin and Turi’s binding algebras. As applications, we give simple proofs of termination of the explicit substitution system λX and currying transformation via higher-order semantic labelling. Moreover, we prove a new result of modularity of termination of IDTSs by introducing the notion of solid IDTSs. We prove that termination is preserved under the disjoint union of an IDTS and a higherorder program scheme. Categories and Subject Descriptors F.4.2 [Grammars and Other Rewriting Systems]; D.3.1 [Programming Laguages]: Formal Definitions and Theory—syntax,seman...
Makoto Hamana
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where PPDP
Authors Makoto Hamana
Comments (0)