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...

• Type: Conference
• Year: 2007
• Where: PPDP
• Authors: Makoto Hamana
• Keywords: Attaches Algebraic Semantics, PPDP 2007, Semantics, Semantics General Terms