Higher-order semantic labelling for inductive datatype systems
Makoto Hamana · 2007
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 frame-work 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 higher-order program scheme.