% A simple example of the strengthening problem and two simple solutions % % The example is motivated by the `demote' in the lambda-a calculus. % Our calculus here is untyped 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. % Showing totality requires strengthening, as shown below. % Astonishingly, the most naive definition of strengthening works. % I wanted to structure a world, so to specify that some % hypotheses are not independent but related. So, discharging one related % hypothesis automatically discharges its related partner. But that % turns out unnecessary. % The strengthening problem has been discussed at POPL2008 with Bob Harper % and Karl Crary. Karl suggested an approach (outlined below) that % needed intentional equality. That turns out unnecessary. % I can't believe how simple the final solution is. % % There is the second solution, near the end of the file. It is round-about, % requiring us to define a different sort of terms, which are nevertheless % isomorphic to the original ones. The isomorphism has to be proven % constructively, too -- although it is boilerplate. 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. mark: type. % There are two marks for terms 0: mark. 1: mark. % Marked lambda-calculus terms exp: mark -> type. %name exp E. a: exp M -> exp M -> exp M. l: (exp M -> exp M) -> exp M. % A sample term t1 : exp 1 = a (l [x] (l [y] (a x y))) (l [x] x). % Let us illustrate the problem of the naive copying cp1: exp 1 -> exp 0 -> type. %mode cp1 +E1 -E2. 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 _). %{ If we uncomment the %total declaration, we get: 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'). Indeed, Twelf says that in the clause cp1-l, E' is in scope of both x and x' -- it depends on both hypotheses x and x'. The pattern match (E' x') assumes that E' does not depend on x. But there is no proof of that. So, we need strengthening: we need to prove to Twelf that E' really does not depend on x. Karl Crary suggested the following solution: first, introduce cp-total: cp E E -> type. When proving it, use a lemma foo: ({x}{y} cp x y -> cp (E x) (E' x y)) -> ({x}{y} exp-eq (E' x y) (E'' y)). Build exp-eq family to prove the lemma. As it turns out, a simpler approach suffices. }% % Astonishingly, proving strengthening is straightforward: the marks % in the type of terms do help. We observe from the definition of exp % that a term of the type exp 0 cannot have any subterm of the type exp 1. % We merely need to express this obvious fact in the form Twelf understands. % See the strength family. % Forward declaration of the new copying relation and the block declaration. cp2: exp 1 -> exp 0 -> type. %block cp2-l-bl : block {x:exp 1} {x':exp 0} {d:cp2 x x'}. % Strengthening: asserting that exp 0 cannot depend on any hypothesis of % the type exp 1. The following is the constructive proof. strength : (exp 1 -> exp 0) -> exp 0 -> type. %mode strength +H -E. -: strength ([x] E) E. % for E that is patently independent of x -: 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'). %block strength-bl : block {x':exp 0}. %worlds (strength-bl | cp2-l-bl) (strength _ _). %covers strength +H -E. %total {E} (strength E _). % Using strengthening is trivial, too. % 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''. %worlds (cp2-l-bl) (cp2 _ _). %total {E1} (cp2 E1 _). % Example %query 1 1 (cp2 t1 T). % T = a (l ([e:exp 0] l ([e1:exp 0] a e e1))) (l ([e:exp 0] e)). % The second, round-about solution. % It is deterministic, however. % Rather than transforming (exp 1) to (exp 0) directly, we introduce % terms (expi M) isomorphic to (exp M), transform (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 thus avoid strengthening altogether. % Marked lambda-calculus terms expi: mark -> type. %name expi _Ei. a2: expi M -> expi M -> expi M. l2: (expi M -> expi M) -> expi M. % Stating that (exp M) are isomorphic to (expi M). % We only need one direction however: 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. -: exp-expi (a E1 E2) (a2 E1' E2') <- exp-expi E2 E2' <- exp-expi E1 E1'. -: 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 _). % The main transformation % The source term is (expi 1) rather than (exp 1). cpaux: expi 1 -> exp 0 -> type. %mode cpaux +E1 -E2. cpa-a: cpaux (a2 E1 E2) (a E1' E2') <- cpaux E2 E2' <- cpaux E1 E1'. 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 _). % Putting it all together cpi: exp 1 -> exp 0 -> type. %mode cpi +E1 -E2. -: cpi E1 E2 <- exp-expi E1 E1' <- cpaux E1' E2. %worlds () (cpi _ _). %total {} (cpi _ _). % Example %query 1 2 (cpi t1 T).