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 |
[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:
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.
| This article or section needs to recreate why you need a metric. |
[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.
| This article or section needs to show one such case.. |
[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.
