Numeric termination metrics

Sometimes, a proof proceeds not by a direct induction on some assumption, but by induction on some size function computed from an assumption. To mechanize such a proof in STELF, you must make the size function explicit in the statement of the theorem.

This tutorial presents an example of such a proof. We show a fragment of a proof of confluence for a λ-calculus with typed η-expansion. The proof inducts on the size of a reduction derivation. Moreover, the proof uses %reduces to tell the termination checker that addends are subterms of their sum. In general, a %reduces declaration is necessary whenever the computation of a numeric termination metric uses an auxiliary relation like addition or maximum. See the tutorial on structural termination metrics for another approach to termination metrics.

Language Definition

The syntax, typing judgement, and reduction relation for the language are straightforward:

%% Syntax
%sort tp %.
%name tp %.
%term o tp %.
%term arrow %pi tp %-> tp %-> tp %.
%sort exp %.
%name exp %.
%term lam %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.
%% Static Semantics
%sort of {_ exp} {_ tp} %.
%term of_lam %pi (of (lam T1 E) (arrow T1 T2)) %<- ({x exp} %pi (of x T1) %-> (of (E x) T2)) %.
%term of_app %pi (of (app E1 E2) T2) %<- (of E1 (arrow T1 T2)) %<- (of E2 T1) %.
%% Dynamic Semantics
%sort reduce {_ exp} {_ exp} %.
%term reduce_id reduce E E %.
%term reduce_lam
  %pi (reduce (lam T E) (lam T E'))
  %<- ({x exp} %pi (of x T) %-> (reduce (E x) (E' x))) %.
%term reduce_app %pi (reduce (app E1 E2) (app E1' E2')) %<- (reduce E1 E1') %<- (reduce E2 E2') %.
%term reduce_beta
  %pi (reduce (app (lam T E1) E2) (E1' E2'))
  %<- ({x exp} %pi (of x T) %-> (reduce (E1 x) (E1' x)))
  %<- (reduce E2 E2') %.
%term reduce_eta %pi (reduce E (lam T1 ([x] app E' x))) %<- (of E (arrow T1 T2)) %<- (reduce E E') %.

The judgement reduce defines a parallel, reflexive reduction relation with typed η-expansion.

Facts about numbers

In the proof below, we induct on the size of a reduction derivation. To get this induction to go through, we require some facts about addition on natural numbers.

First, we define addition:

%sort nat %.
%name nat %.
%term 0 nat %.
%term s %pi nat %-> nat %.
%define 1 nat s 0 %.
%sort sum {_ nat} {_ nat} {_ nat} %.
%term sum_0 sum 0 N N %.
%term sum_s %pi (sum (s N1) N2 (s N3)) %<- (sum N1 N2 N3) %.

For the proof below, we need a way to tell STELF’s termination checker that summands are subterms of their sum. We do that by proving a lemma with a %reduces declaration.

We prove the lemma for the second summand first. Note that all arguments of this lemma are inputs; the only “output” is the fact that the %reduces holds:

%sort sum_reduces2 {N1 nat} {N2 nat} {N3 nat} {_ sum N1 N2 N3} %.
%mode sum_reduces2 %in %in %in %in %.
%term _ sum_reduces2 _ _ _ sum_0 %.
%term _ %pi (sum_reduces2 (s N1) N2 (s N3) (sum_s D)) %<- (sum_reduces2 N1 N2 N3 D) %.
%worlds () (sum_reduces2 _ _ _ _) %.
%total D (sum_reduces2 _ _ _ D) %.
%reduces <= N2 N3 (sum_reduces2 N1 N2 N3 _) %.

The easiest way to prove the lemma for the first summand is to commute the addition and appeal to the previous lemma. We state commutativity as

%sort sum_commute {_ sum N1 N2 N3} {_ sum N2 N1 N3} %.
%mode sum_commute %in %out %.
%worlds () (sum_commute _ _) %.

but elide its proof.

%sort sum_reduces1 {N1 nat} {N2 nat} {N3 nat} {_ sum N1 N2 N3} %.
%mode sum_reduces1 %in %in %in %in %.
%term _
  %pi (sum_reduces1 N1 N2 N3 Dsum)
  %<- (sum_commute Dsum Dsum')
  %<- (sum_reduces2 N2 N1 N3 Dsum') %.
%worlds () (sum_reduces1 _ _ _ _) %.
%total {} (sum_reduces1 _ _ _ _) %.
%reduces <= N1 N3 (sum_reduces1 N1 N2 N3 _) %.

Proof of confluence

We now show part of the proof of the diamond property for this notion of reduction. The proof requires a metric computing the size of a reduction derivation.

Definition of the metric

%sort reduce_metric {_ reduce E E'} {_ nat} %.
%term reduce_metric_id reduce_metric reduce_id 1 %.
%term reduce_metric_lam
  %pi (reduce_metric (reduce_lam D) (s N))
  %<- ({x exp} {d of x T} reduce_metric (D x d) N) %.
%term reduce_metric_app
  %pi (reduce_metric (reduce_app D2 D1) (s N))
  %<- (reduce_metric D1 N1)
  %<- (reduce_metric D2 N2)
  %<- (sum N1 N2 N) %.
%term reduce_metric_beta
  %pi (reduce_metric (reduce_beta D2 D1) (s N))
  %<- ({x exp} {d of x T} reduce_metric (D1 x d) N1)
  %<- (reduce_metric D2 N2)
  %<- (sum N1 N2 N) %.
%term reduce_metric_eta %pi (reduce_metric (reduce_eta D _) (s N)) %<- (reduce_metric D N) %.

Excerpt of the proof

%sort diamond {N1 nat} {N2 nat} {D1 reduce E E1} {D2 reduce E E2} {_ reduce_metric D1 N1} {_ reduce_metric D2 N2} {_ reduce E1 E'} {_ reduce E2 E'} %.
%mode diamond %in %in %in %in %in %in %out %out %.
%term _ diamond _ _ reduce_id D _ _ D reduce_id %.
%term _ diamond _ _ D reduce_id _ _ reduce_id D %.
%term _
  %pi (diamond (s N1) (s N2) (reduce_lam D1) (reduce_lam D2) (reduce_metric_lam DM1) (reduce_metric_lam DM2) (reduce_lam D1') (reduce_lam D2'))
  %<- ({x exp} {d of x T} diamond N1 N2 (D1 x d) (D2 x d) (DM1 x d) (DM2 x d) (D1' x d) (D2' x d)) %.
%term _
  %pi (diamond (s N1) (s N2) (reduce_app (%the (reduce E2 E21) D21) (%the (reduce E1 E11) D11)) (reduce_app (%the (reduce E2 E22) D22) (%the (reduce E1 E12) D12)) (reduce_metric_app (%the (sum N11 N21 N1) Dsum1) (%the (reduce_metric D21 N21) DM21) (%the (reduce_metric D11 N11) DM11)) (reduce_metric_app (%the (sum N12 N22 N2) Dsum2) (%the (reduce_metric D22 N22) DM22) (%the (reduce_metric D12 N12) DM12)) (reduce_app D21' D11') (reduce_app D22' D12'))
  %<- (sum_reduces1 N11 N21 N1 Dsum1)
  %<- (sum_reduces2 N11 N21 N1 Dsum1)
  %<- (sum_reduces1 N12 N22 N2 Dsum2)
  %<- (sum_reduces2 N12 N22 N2 Dsum2)
  %<- (diamond N11 N12 D11 D12 DM11 DM12 D11' D12')
  %<- (diamond N21 N22 D21 D22 DM21 DM22 D21' D22') %.
%% fill in remaining cases
%block bind [t tp] {x exp} {d of x t}%.
%worlds (bind) (diamond _ _ _ _ _ _ _ _) %.
%terminates [N1 N2] (diamond N1 N2 _ _ _ _ _ _) %.

The reduce_app against reduce_app case illustrates why we need to know that summands are subterms of their sum: the inductive calls are on the summands that add up to the size of the overall derivation. If we elided the calls to sum_reduces*, the case would not termination-check, because STELF would not be able to tell that, for example, N11 < (s N1).

In other cases, which we have elided, the termination metric gets smaller but the reduction derivations themselves do not.

Cleanup

We would like an overall theorem:

%sort diamond/clean {_ reduce E E1} {_ reduce E E2} {_ reduce E1 E'} {_ reduce E2 E'} %.
%mode diamond/clean %in %in %out %out %.
%worlds (bind) (diamond/clean _ _ _ _) %.