Many logic systems admit a weakening principle: a derived conclusion continues to hold when more assumptions are added. Strengthening is the opposite: proving that the established conclusion holds given fewer assumptions. Strengthening certainly is not generally valid and has to be proven case-by-case. It seems strengthening is often needed when proving meta-theoretical properties such as totality of non-surjective endomorphisms of higher-order terms.

The article on Twelf Wiki <http://twelf.plparty.org/wiki/Strengthening> shows an example of the need for strengthening and describes one solution, which relies on defining term equality. In this article we demonstrate simpler examples requiring strengthening, and two surprisingly trivial solutions. Quite literally, one solution deals with the problem head-on, whereas the second one avoids the problem in a round-about way. The examples are inspired by staging calculi. At the end we describe the real development, which gives perhaps the first formal proof of type preservation of primitive reductions in an expressive staged calculus with escapes, run and cross-staged persistence. The type-preservation proof used both of our solutions and required two strengthening lemmas. Throughout we use Twelf – properly: we use the higher-order abstract syntax (HOAS) for higher-order terms, without ever resorting to concrete syntax for “variables”. The complete code is available at <http://okmij.org/ftp/Computation/staging/> .

The simplest example requiring strengthening

Perhaps the simplest example to illustrate the need of strengthening is based on lambda-calculus with terms marked by either 1 or 0. The challenge is to implement a function that converts terms marked by 1 into those marked by 0 – and show its totality.

Our calculus is elementary: we define two marks, 0 and 1

mark: type.
0: mark.
1: mark.

and marked terms, built of applications and abstractions:

exp: mark -> type.              %name exp E.
a: exp M -> exp M -> exp M.
l: (exp M -> exp M) -> exp M.

Here is a sample term, marked with 1:

t1 : exp 1 = a (l [x] (l [y] (a x y))) (l [x] x).

(in Haskell notation, it is (\x -> \y -> x y) (\x -> x) ). The definition of exp makes it clear that all subterms of a marked term have the same mark.

Our goal is to write a transformation taking a term marked by 1 and producing a term marked by 0:

cp1: exp 1 -> exp 0 -> type.
%mode cp1 +E1 -E2.

It is almost like copying terms and hence straightforward:

cp1-a: cp1 (a E1 E2) (a E1' E2')
         <- cp1 E2 E2'
         <- cp1 E1 E1'.
cp1-l: cp1 (l E1) (l E1')
         <- ({x}{x'} cp1 x x' -> cp1 (E1 x) (E1' x')).
%block cp1-l-bl : block {x:exp 1} {x':exp 0} {D:cp1 x x'}.
%worlds (cp1-l-bl) (cp1 _ _).
%total {E1} (cp1 E1 _).  %% Does not pass!

The clause cp1-a inductively handles applications. To transform an abstraction, we assume a term x marked with 1, a term x' marked with 0, and assume that x' is the result of transforming x, see cp1 x x'. Under those assumptions, we transform the body of the abstraction, cp1 (E1 x) (E1' x'). The notation (E1' x') means that E1' is a higher-order term applied to x'. That is, E1' is of the type exp 0 -> exp 0. The block declaration cp1-l-bl lists our set of assumptions; the regular worlds declaration asserts that cp1 is performed given no assumptions, or one set assumption cp1-l-bl, or two sets of such assumptions (with the different x and x' across the sets), etc.

Our transformation procedure is obviously total: we can take any 1-marked term, and, in finite time, always deliver the corresponding 0-marked term. We wish to state this formally, hence the %total assertion. Twelf verifies it first by checking that the transformation is terminating. It then checks that all pattern-matching is exhaustive: we have not missed a case. Alas, the totality check fails and Twelf reports an error:

Totality: Output of subgoal not covered
Output coverage error --- missing cases:
{E1:exp 1 -> exp 1} {E2:exp 1 -> exp 0 -> exp 0}
   |- {x:exp 1} {x':exp 0} cp1 x x' -> cp1 (E1 x) (E2 x x').

In the clause cp1-l, we have introduced three assumptions: x, x' and cp1 x x'. By writing (E1' x') we asked the Twelf system to “factor out” the dependence on x'. Implicitly we stated that the result of transforming (E1 x) depends only on x' but not on x or cp1 x x' (more formally, the independence is seen from the fact E1' is used outside of the scope of x introduced via the universal quantification {x} in cp1-l). Twelf can see that the assumption cp1 x x' cannot possibly enter the set of terms because the definition of the type family exp (with constructors a and l) shows that no term can contain anything of the type cp1. But terms may occur in terms, and so the result of transforming the body of the abstraction generally depends on both x and x'. We have not handled that general case, and so our transformation is not total.

Twelf’s complaint is quite insightful: (E1 x) is the body of the abstraction that includes some term x (“the variable”). We transform the body replacing all those occurrences of x with x' – and so the result should include only x' but no x. Thus Twelf demands the proof that we indeed replaced all those x with x'.

Upon consideration, we can see that the result of transforming (E1 x) cannot really depend on, or contain, x. After all, x is an expression marked by 1 and the result of transforming (E1 x) is an expression marked by 0. Any sub-expression of a marked expression is marked with the same mark. Alas, Twelf cannot see this proof by itself and we have to write it down explicitly. The reason Twelf cannot see that proof by itself is because Twelf tracks the dependencies (so-called subordination) using only the names of the type families (e.g., exp) but not their parameters (e.g., exp 0 or exp 1).

Astonishingly, the most trivial way of writing this independence proof works. We state that whenever a term marked by 0 appears to depend on a term marked by 1, it actually doesn’t. Or, constructively, we assert the following proposition

strength : (exp 1 -> exp 0) -> exp 0 -> type.
%mode strength +H -E.

For any implication exp 1 -> exp 0, we can always constructively produce exp 0. Here is the proof, the detailed procedure of producing that exp 0 term:

-: strength ([x] E) E.
-: strength ([x] (a (E1 x) (E2 x))) (a E1' E2')
   <- strength E1 E1'
   <- strength E2 E2'.
-: strength ([x] (l [x'] (E x' x))) (l E')
   <- {x':exp 0} strength (E x') (E' x').

The first clause handles the case when E patently does not contain anything of the type exp 1. The rest of the clauses do straightforward induction on terms; the last clause requires hypothetical reasoning to examine the body of the abstraction, and for that we introduce the assumption x' of the type exp 0. Perhaps it is because of that hypothetical reasoning that Twelf cannot see the strengthening property on its own. We assert that so defined procedure is total, i.e., it is a constructive proof of the strength proposition:

%block strength-bl : block {x':exp 0}.
%worlds (strength-bl | cp2-l-bl) (strength _ _).
%covers strength +H -E.
%total {E} (strength E _).

The label cp2-l-bl describes the set of assumptions of the improved cp2 procedure below (in the actual code, it is defined in a forward declaration). Twelf has verified the totality of strength, and so we can use it to write the improved transformation procedure, cp2:

cp2: exp 1 -> exp 0 -> type.
%mode cp2 +E1 -E2.
cp2-a: cp2 (a E1 E2) (a E1' E2')
         <- cp2 E2 E2'
         <- cp2 E1 E1'.
cp2-l: cp2 (l E1) E1''
         <- ({x}{x'} cp2 x x' -> cp2 (E1 x) (E1' x x'))
         <- strength ([x] (l (E1' x))) E1''.
%block cp2-l-bl : block {x:exp 1} {x':exp 0} {d:cp2 x x'}.
%worlds (cp2-l-bl) (cp2 _ _).
%total {E1} (cp2 E1 _).

The only difference from cp1 is in the clause cp2-l: by writing (E1' x x') we state that the result of transforming the body of the abstraction may depend not only on x' but also on x. We build the transformed abstraction under that additional assumption: ([x:exp 1] (l (E1' x))). Using strengthening, we then prove that (l (E1' x)) does not actually depend on x. Now the totality assertion succeeds: cp2 is the total transformation of 1-marked terms.

The complete code is available at <http://okmij.org/ftp/Computation/staging/strengthen.elf>

A more realistic example: type preservation

We have encountered the problem of strengthening in staged calculi, e.g., when proving type preservation. We outline the problem and the solution; please see the complete code <http://okmij.org/ftp/Computation/staging/translation-problem.elf> for the full details.

We introduce a simple staged language, where each expression is annotated with the numeric stage label A. The language has three forms of expressions: natural literals, addition, and fix (i.e., recursive functions).

exp : nat -> type.              %name exp E.
n : nat -> exp A.               %prefix 110 n.
+ : exp A -> exp A -> exp A.    %infix left 154 +.
fix : (exp A -> exp A) -> exp A.

We introduce a trivial type system with only one type, int, and the equally simple type-checking relation of E T:

of : exp A -> tp -> type.       %name of Q.
%mode of +E *T.

Please see the code for details. As in the previous section we write the procedure to downgrade the level of an expression

downgrade : exp (1 N) -> exp N -> type.
%mode downgrade +E1 -E2.

We are not that interested in proving downgrade is total. Rather, we wish to prove a meta-theorem that downgrade is type preserving: if the original expression was typed, the downgraded expression shall be typed too. We state that property as a constructive proposition:

dn-pres : downgrade E1 E2 -> of E1 T -> of E2 T -> type.
%mode dn-pres +PD +PTI -PTO.

That is, given any downgradeable expression E1 and its type derivation of E1 T (the evidence that E1 is typed), we produce the typing derivation for the corresponding downgraded expression E2. The most interesting case is the following:

- : dn-pres (dn-f PEH) (of-f PTH) PTH''
        <- ({e:exp (1 A)} 
            {pt:of e int}
            {e':exp A}
            {dn:downgrade e e'}
            {pt':of e' int}
            dn-pres dn pt pt' ->
            dn-pres (PEH e e' dn) (PTH e pt) (PTH' e pt e' pt'))
        <- strength-of ([e] [pt] (of-f  (PTH' e pt))) PTH''.

Here, dn-f PEH of the type downgrade (fix E1) (fix E2) is the derivation of downgrading (fix E1) into (fix E2). We assume a term e of the type exp (1 A), and further assume it is typed (the assumption pt:of e int). Likewise we assume a typed term e' that is the result of downgrading e. Finally, we assume that the downgrading from e to e' was type preserving. Under those assumptions, we obtain the type derivation of the body of the downgraded fix, by inductively invoking dn-pres. The resulting type derivation (PTH' e pt e' pt') generally depends not only on the assumption e' and its typeability pt' – but also on e and pt, which are in scope and could in principle occur in type derivations. We must thus prove that we can remove the latter dependency. Again, the formal statement of that proposition is surprisingly simple:

strength-of : ({e:exp (1 N)} of e T -> of (E:exp N) T) -> 
              of (E:exp N) T -> type.
%mode strength-of +H -P.

We assert that the typing derivation of E T for an expression E at the level N cannot depend on any N+1-level expression e and the typing derivation of the latter. Our proof is again constructive: from the corresponding implication we produce its conclusion without assuming the hypotheses. The complete code has all details.

Other examples

The need for strengthening does occur (although not frequently) in other circumstances. Here are the example from Twelf distribution. One is “Representation of Mini-ML expressions in Mini-ML*” by David Swasey, file exercises/opt-eval/opt-rep1.elf. It defines a transformation from one higher-order language to another. Proving meta-theoretical properties of that translation (totality, type preservation, etc) requires strengthening.

The second, indirect solution

The second solution to strengthening is, too, trivial, albeit round-about. We use the same problem as in Section 1: in lambda-calculus whose terms are marked with 0 or 1, implement a function that converts terms marked by 1 into those marked by 0 – and show its totality.

Rather than transforming exp 1 to exp 0 directly, we introduce terms expi M isomorphic to exp M, turn exp 1 to expi 1 and then transform expi 1 to exp 0. The advantage is that terms exp M cannot appear in expi M and vice versa, so exp M cannot depend on assumptions of the type {x:expi M} and vice versa. We avoid strengthening altogether.

Here are a few details: we define intermediary, also marked, terms

expi: mark -> type.             %name expi _Ei.
a2: expi M -> expi M -> expi M.
l2: (expi M -> expi M) -> expi M.

that are clearly isomorphic to the terms exp M of the original calculus. We can state the isomorphism formally; however, we only need one direction of it: given any term exp M, we can always obtain the corresponding expi M:

exp-expi: exp M -> expi M -> type.
%mode exp-expi +E1 -E2.

We show only the more complex case of transforming abstractions:

-: exp-expi (l E1) (l2 E1')
   <- {e:exp M} {e2:expi M}
      exp-expi e e2 ->
      exp-expi (E1 e) (E1' e2).
%block bl-exp-expi : 
       some {M:mark} 
       block {e:exp M} {e2:expi M} {t:exp-expi e e2}.
%worlds (bl-exp-expi) (exp-expi _ _).
%total {E} (exp-expi E _).

Now Twelf verifies the totality assertion without any complaints that E1' could depend (that is, include) the assumption e, which is also present in the LF context. Twelf now sees that E1' cannot include e. Compared to Section 1, converting an expression of the type exp M gives us the term of the type expi M. The latter terms can only be constructed by l2 and a2; neither constructor can take any argument of the type exp M or contain exp M elsewhere. Strengthening is no longer needed.

The label-changing transformation now takes expi 1 rather than exp 1 as the source a term:

cpaux: expi 1 -> exp 0 -> type.
%mode cpaux +E1 -E2.

Here is the interesting case

cpa-l: cpaux (l2 E1) (l E1')
       <- ({x:expi 1}{x':exp 0} cpaux x x' -> cpaux (E1 x) (E1' x')).
%block bl-cpaux : block {x:expi 1} {x':exp 0} {t:cpaux x x'}.
%worlds (bl-cpaux) (cpaux _ _).
%total {E1} (cpaux E1 _).

Again, Twelf accepts the totality assertion without complaint because clearly no term of the type expi M may appear in the term exp M – in fact, expi was not even defined when exp was introduced. Thus (E1' x') cannot depend on x.

What remains is a mere composition of the two above transformations

cpi: exp 1 -> exp 0 -> type.
%mode cpi +E1 -E2.
-: cpi E1 E2 <- exp-expi E1 E1' <- cpaux E1' E2.
%worlds () (cpi _ _).
%total {} (cpi _ _).

The desired transformation now includes two steps: transforming the source expression into the isomorphic form, and changing the mark of the latter. Albeit indirect, the solution avoids strengthening altogether.

A real example: type-preservation in an expressive staged calculus

The file <http://okmij.org/ftp/Computation/staging/lambda-am1.elf> is the formalization of the two-level call-by-value calculus lambda-a1v based on lambda-a of Taha and Nielsen’s “Environment Classifiers” (POPL03). The calculus supports manipulation and splicing in of the open code, running of the closed code, and cross-staged persistence. The lambda-a1v calculus has been introduced in the paper Closing the Stage: From Staged Code to Typed Closures written with Yukiyoshi Kameyama and Chung-chieh Shan (PEPM08).

The file includes (maybe the first) formal proof that any non-value term can be decomposed into a pre-value and the context. This is quite challenging given that the calculus supports the evaluation under lambda and so the context can cross the arbitrary number of dependent binders: variable binders include classifiers that must be bound, too, at that point.

In our staged calculus, all terms are marked by their stage, present and future. This is quite like the examples in the earlier Sections. There is also an operation to demote a term, which takes a future-stage-marked term and changes its mark so the term can be evaluated at the present stage. Demotion is how a future-stage computation can be run. Demotion rebuilds a term as it traverses it, changing the marks along the way. The only special case is handling a cross-staged persistent (CSP) value. The latter is a present-stage expression that was “lifted” to the future stage, i.e., was encapsulated unevaluated. The demotion operation merely removes the encapsulation, splicing CSP into the demoted code.

The type-preservation proof is at the end of the development. The most complex part is proving that demotion is type preserving, in particular, that demoting an abstraction (l [x:exp (1q AL)] Body) from the future stage (marked by (1q AL)) to the present, marked as qt, stage yielding (l [x':exp qt] Body') is type preserving. As in the simpler examples earlier, the proof proceeds by introducing assumptions {x:exp (1q AL)}, {x':exp qt} and that x' is the result of demoting x. The challenge is to prove that Body' does not actually depend on x. That is no longer as simple as before: a future-stage expression exp (1q AL) could actually occur in the demoted expression – because of CSP. For example, consider the following future-stage term

(l [x:exp (1q AL)] (csp (AL > x)))

where AL > x is future-stage-x marked by classifier AL (in the PEPM08 paper, we write (l [x^AL] %(<x>^AL)). An attempt to run such future-stage computations does not type in MetaOCaml; accordingly, the lambda-a1v calculus rejects such expressions as mis-typed, due to a special typing rule of CSP. Our preservation proof must take into account that the demoted expression is typed and so possible CSPs are restricted in form. Only then strengthening can be proven.

In our proof, we had to use both approaches to proving strengthening described in this article. We had to prove a direct strengthening lemma

strength-tp-dem : csp-ok1 E ->
                  ({x:exp (1q AL)} of x TV -> of E T) -> 
                  of E T -> type.
%mode strength-tp-dem +CS +H -P.

asserting that the typing of a present-stage expression (of (E:exp qt) T) cannot depend on a future-stage expression exp (1q AL) and the latter’s typing derivation (of (_:exp (1q AL)) T) – provided that E is the result of a demotion. We also use the indirect approach and introduce a CSP restriction predicate csp-ok1 isomorphic to the predicate csp-ok. The latter may occur in typing derivations but the former may not. Finally, we had to prove the strengthening lemma for csp-ok1.