- Recent Changes 新聞
- History 歷史
- Preferences 喜好
- Discussion 討論

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`

.