On the relation between size-based termination and semantic labelling

Details On the relation between size-based termination and semantic labelling On the relation between size-based termination and semantic labelling

2009-06-23

arxiv.org/abs/0906.4173v1

18th EACSL Annual Conference on Computer Science Logic (2009)

Computer Science

Logic in Computer Science

Scientific paper

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

Affiliated with

Also associated with

No associations

Rating

On the relation between size-based termination and semantic labelling does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On the relation between size-based termination and semantic labelling, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the relation between size-based termination and semantic labelling will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-708111