% Illustration of the problem of proving totality or other meta-theoretical % property of a translation from one HOAS expression to another. % The two expressions have `bindings' of different types. % That is, we translate from ([e] EB e) to ([e'] EB' e') where % the type of e is not that same as the type of e'. % The problems of these sort occur in staging (where translation % changes the level of an expression and it translates under binding). % Or proving soundness and completeness of Kolmogorov translation % or any such translation between (hypothetical) logical judgments. % include util.elf % Let's consider a simple staged language, where each expression % is annotated with a numeric stage. The language % has three forms of expressions: natural literals, addition, and fix. % fix introduces binding -- and that's where the problem lurks. 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. % A few sample expressions e11 : exp (1 0) = fix ([e] e + (n 0)). % at level 1 e12 : exp 0 = fix ([e] e + (n 0)). % the same at level 0 % The most trivial type system: there is only one type, int. tp : type. %name tp T. int : tp. % The type checking relation. Could not be more trivial. % The typechecking of 'fix' requires hypothetical reasoning. % We assume that 'e' has the type of int, substitute it into the body % of fix. of : exp A -> tp -> type. %name of Q. %mode of +E *T. of-i : of (n _) int. of-+ : of (E1 + E2) int <- of E2 int <- of E1 int. of-f : of (fix E) int <- {e} of e int -> of (E e) int. %block bet : some {A:nat} block {e:exp A} {pt: of e int}. %worlds (bet) (of _ _). %covers of +E *T. % Now we write a function that downgrades the level of expression: % it takes an expression at level N+1 and returns the expression at % level N. The real downgrading happens for naturals (which are safely % downgraded to any level). For other forms of expressions, the downgrade % is homomorphism. % Doing this homomorphism under fix requires hypothetical reasoning. % Indeed, we have (fix [e:exp (1 N)] EB e) and we want to obtain % (fix [e':exp N] EB' e'). So, we conjure up the expressions (e) and % (e') and assume that (downgrade e e') holds. Under these assumptions % we downgrade (EB e). We get the downgraded expression, and we discharge % the hypothesis e'. % We must note that downgrade fails the input coverage -- and it shall % fail the output coverage. The latter is where the problem shows up later. % Let us consider the last line of dn-f: % downgrade (EB e) (EB' e'). % It says that the result of downgrading (EB e) depends % only on e'. But how do we know that? We assumed both (e) and (e') -- % but claim that the result of downgrading (EB e) depends on % (e') alone. What if we missed some branch of (EB e) when traversing % it and so failed to replace (e) with (e') in that branch? In that case, % the result of downgrading (EB e) will depend on both (e) and (e'). % Well, the downgrade does not have to be total. We define downgrade % in the way that the result of downgrading (EB e) must depend on (e') % alone. Otherwise, downgrade is not defined. % Forward family and block declaration downgrade : exp (1 N) -> exp N -> type. %block bed : some {A:nat} block {e:exp (1 A)} {e':exp A} {dn:downgrade e e'}. % Strengthening: asserting that exp N cannot depend on any hypothesis of % the type exp (1 N). The following is the constructive proof. strength : (exp (1 N) -> exp N) -> exp N -> type. %mode strength +H -E. -: strength ([x] E) E. % for E that is patently independent of x -: strength ([x] ((E1 x) + (E2 x))) (E1' + E2') <- strength E1 E1' <- strength E2 E2'. -: strength ([x] (fix [x'] (E x' x))) (fix E') <- {x'} strength (E x') (E' x'). %block strength-bl : some {N:nat} block {x':exp N}. %worlds (strength-bl | bed) (strength _ _). %covers strength +H -E. %total {E} (strength E _). %mode downgrade +E1 -E2. dn-n : downgrade (n N) (n N). % the only meaningful downgrade % homomorphism dn-+ : downgrade (E1 + E2) (E1' + E2') <- downgrade E2 E2' <- downgrade E1 E1'. % homomorphism too -- but under a binder dn-f : downgrade (fix EB) (fix EB') <- ({e:exp (1 A)} {e':exp A} downgrade e e' -> downgrade (EB e) (EB' e')). % <- strength ([e] (fix (EB' e))) EB''. %worlds (bed) (downgrade _ _). % %covers downgrade +E1 -E2. % A simple test, to see how it works. %query 1 1 (downgrade e11 R). % It does: the result is % R = fix ([e:exp 0] e + (n 0)). % now prove that downgrade is type preserving dn-pres : downgrade E1 E2 -> of E1 T -> of E2 T -> type. %block bedp : some {A:nat} block {e:exp (1 A)} {pt:of e int} {e':exp A} {dn:downgrade e e'} {pt':of e' int} {dnp:dn-pres dn pt pt'}. % Strengthening: asserting that of E T cannot depend on any hypothesis of % involving expression of the type exp (1 N). The following is the % constructive proof. 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. -: strength-of ([x] [p] P) P. % for P that is patently independent of x, p -: strength-of ([x] [p] (of-+ (E1 x p) (E2 x p))) (of-+ E1' E2') <- strength-of E1 E1' <- strength-of E2 E2'. -: strength-of ([x] [p] (of-f [x':exp N] [p'] (E x' p' x p))) (of-f E') <- {x':exp N} {p'} strength-of (E x' p') (E' x' p'). %block strength-of-bl : some {N:nat} {T:tp} block {x':exp N} {p':of x' T}. %worlds (strength-of-bl | bedp) (strength-of _ _). %covers strength-of +H -E. %total {E} (strength-of E _). %mode dn-pres +PD +PTI -PTO. - : dn-pres dn-n of-i of-i. - : dn-pres (dn-+ PE1 PE2) (of-+ PT1 PT2) (of-+ PT1' PT2') <- dn-pres PE1 PT1 PT1' <- dn-pres PE2 PT2 PT2'. - : 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''. %worlds (bedp) (dn-pres _ _ _). %covers dn-pres +PD +PTI -PTO. % OK, input coverage succeeds. %total {PD} (dn-pres PD _ _). % It is total!