Numeric termination metrics

From The Twelf Project

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 Twelf, 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.

Contents 1 Language Definition 2 Facts about numbers 3 Proof of confluence 3.1 Definition of the metric 3.2 Excerpt of the proof 3.3 Cleanup

[edit] Language Definition

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

% Syntax

tp  : type.  %name tp T.
o	: tp.
arrow	: tp -> tp -> tp.

exp : type.  %name exp E.
lam	: tp -> (exp -> exp) -> exp.
app	: exp -> exp -> exp.

% Static Semantics

of : exp -> tp -> type.
of_lam	: of (lam T1 E) (arrow T1 T2)
	   <- ({x:exp} of x T1 -> of (E x) T2).
of_app	: of (app E1 E2) T2
	   <- of E1 (arrow T1 T2)
	   <- of E2 T1.

% Dynamic Semantics

reduce : exp -> exp -> type.

reduce_id	: reduce E E.
reduce_lam	: reduce (lam T E) (lam T E')
		   <- ({x:exp} of x T -> reduce (E x) (E' x)).
reduce_app	: reduce (app E1 E2) (app E1' E2')
		   <- reduce E1 E1'
		   <- reduce E2 E2'.
reduce_beta	: reduce (app (lam T E1) E2) (E1' E2')
		   <- ({x:exp} of x T -> reduce (E1 x) (E1' x))
		   <- reduce E2 E2'.
reduce_eta	: 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.

[edit] 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:

nat : type.  %name nat N.

0 : nat.
s : nat -> nat.

1 : nat = s 0.

sum : nat -> nat -> nat -> type.

sum_0		: sum 0 N N.
sum_s		: sum (s N1) N2 (s N3)
		   <- sum N1 N2 N3.

For the proof below, we need a way to tell Twelf'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:

sum_reduces2 : {N1:nat} {N2:nat} {N3:nat} sum N1 N2 N3 -> type.
%mode sum_reduces2 +X1 +X2 +X3 +X4.

-: sum_reduces2 _ _ _ sum_0.
-: 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 elide the proof of commutativity:

ERROR: option 'name' deprecated or invalid

sum_commute : sum N1 N2 N3 -> sum N2 N1 N3 -> type.
%mode sum_commute +D1 -D2.
%worlds () (sum_commute _ _).

sum_reduces1 : {N1:nat} {N2:nat} {N3:nat} sum N1 N2 N3 -> type.
%mode sum_reduces1 +X1 +X2 +X3 +X4.

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

[edit] 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.

[edit] Definition of the metric

reduce_metric : reduce E E' -> nat -> type.

reduce_metric_id	: reduce_metric reduce_id 1.
reduce_metric_lam	: reduce_metric (reduce_lam D) (s N)
			   <- ({x:exp} {d:of x T} reduce_metric (D x d) N).
reduce_metric_app	: reduce_metric (reduce_app D2 D1) (s N)
			   <- reduce_metric D1 N1
			   <- reduce_metric D2 N2
			   <- sum N1 N2 N.
reduce_metric_beta	: 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.
reduce_metric_eta	: reduce_metric (reduce_eta D _) (s N)
			   <- reduce_metric D N.

[edit] Excerpt of the proof

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' -> type.
%mode diamond +X1 +X2 +X3 +X4 +X5 +X6 -X7 -X8.

-: diamond _ _ reduce_id D _ _ D reduce_id.
-: diamond _ _ D reduce_id _ _ reduce_id D.

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

-: diamond 
    (s N1)
    (s N2)
    (reduce_app
       (D21 : reduce E2 E21)
       (D11 : reduce E1 E11))
    (reduce_app 
       (D22 : reduce E2 E22)
       (D12 : reduce E1 E12)) 
    (reduce_metric_app
       (Dsum1 : sum N11 N21 N1)
       (DM21 : reduce_metric D21 N21)
       (DM11 : reduce_metric D11 N11))
    (reduce_metric_app
       (Dsum2 : sum N12 N22 N2)
       (DM22 : reduce_metric D22 N22)
       (DM12 : reduce_metric D12 N12))
    (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 : some {t:tp} block {x:exp} {d:of x t}.
%worlds (bind) (diamond _ _ _ _ _ _ _ _).
%terminates [N1 N2] (diamond N1 N2 _ _ _ _ _ _).

See Twelf's output

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

[edit] Cleanup

We would like an overall theorem:

diamond/clean : reduce E E1
    	       -> reduce E E2
  	       -> reduce E1 E'
	       -> reduce E2 E' -> type.
%mode diamond/clean +X1 +X2 -X3 -X4.
%worlds (bind) (diamond/clean _ _ _ _ _ _ _ _).

It is simple to prove this theorem using the above if we prove an effectiveness lemma for reduce_metric.

---

Read more Twelf tutorials and other Twelf documentation.