On the Relation between Sized-Types Based Termination and Semantic Labelling

We investigate the relationship between two independently developed termination techniques for rst and higher-order rewrite systems. On the one hand, sized-types based termination uses types annotated with size expressions and Girard's reducibility candidates. On the other hand, semantic labelling transforms a rewrite system by annotating each function symbol with the semantic of its arguments. First, we introduce a simplied version of sized-types based termination for the simply-typed lambda-calculus. Then, we give new proofs of the correctness of sized-types based termination by using semantic labelling both in the rst and in the higher-order case. As a consequence, we show that size-based termination can be easily extended to non-constructor systems with pattern symbols interpreted by monotone and strictly extensive functions.

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Frédéric Blanqui, Cody Roux
• Keywords: Artificial Intelligence, CSL 2009, Rewrite System, Sized-types Based Termination, Termination Uses Types