On the relation between size-based termination and semantic labelling

TL;DR

This paper explores the connection between size-based termination and semantic labelling, providing new proofs and extensions for size-based termination techniques in rewriting systems.

Contribution

It introduces a simplified SBT for the simply-typed lambda-calculus and demonstrates its correctness using semantic labelling, extending SBT to more complex systems.

Findings

SBT can be proven correct via semantic labelling techniques.

SBT is extendable to systems with matching on defined symbols.

New proofs unify size-based termination with semantic labelling methods.

Abstract

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