We investigate the relationship between two independently developed termination techniques. On the one hand, sized-types based termination (SBT) uses types annotated with size expressions and Girard's reducibility candidates, and applies on systems using constructor matching only. On the other hand, semantic labelling transforms a rewrite system by annotating each function symbol with the semantics of its arguments, and applies to any rewrite system. First, we introduce a simplified version of SBT for the simply-typed lambda-calculus. Then, we give new proofs of the correctness of SBT using semantic labelling, both in the first and in the higher-order case. As a consequence, we show that SBT can be extended to systems using matching on defined symbols (e.g. associative functions). © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Blanqui, F., & Roux, C. (2009). On the relation between sized-types based termination and semantic labelling. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5771 LNCS, pp. 147–162). https://doi.org/10.1007/978-3-642-04027-6_13
Mendeley helps you to discover research relevant for your work.