% 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!