[CakeML-dev] Iterated bootstrap theorem?

[Yong Kiam]

Thanks for clarifying, I was thinking of:

1) There is a compiler in the logic, e.g. compile :ast -> bytes (ignoring
configurations)

2) Translate this compiler, to get some cakeml AST (in HOL) [..., val
compile = ... ]

3) Add new FFI/IO decls to the AST (as we do now) to get the full compiler
[..., val compile = ..., val main = ... ]

4) Define a new constant for the AST in 3),  |- cml_ast =  [..., val
compile = ..., val main = ... ]

5) Translate cml_ast to get the deeply embedded version of the AST: ``val
cml_ast  = [ ... ]``

6) Stick cml_ast onto the back of 2): [ ..., val compile = ..., val cml_ast
= [ ...], val main = print (compile cml_ast)]

7) Run the in-logic compiler on 6 (doesn't need to be the same as 1)

I think Q2 would be 4) and Q1 would be 2).

How does it speed things up (maybe?): 7) would run a "fast" version of the
compiler in the logic, but it produces a program that runs a "slow" version
of the bootstrap outside the logic.

RE: translation bottleneck, it won't get past it, because we still need to
translate the whole compiler anyhow. The main purpose would be to speedup
bootstrap compilation, but I am not sure if the "fast" in-logic compiler
exists though.

On Sat, Feb 11, 2017 at 6:56 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> This looks like an interesting idea. I haven't understood it fully.
> Let me try to clarify.
> Here are 2 questions I have about your 2-fold example, which I'll copy
> below:
>
> val prog2fold = process_topdecs`
> val (compile,conf) = ^Q1;
> val cml_ast = ^Q2;
> val main = print(compile conf cml_ast);`
>
> My questions are about what Q1 and Q2 should be.
>
> I assume the above program, prog2fold, is going to be used as input
> for proof-grounded evaluation of the compiler, i.e., we will produce a
> theorem like this by EVAL: |- compile ^prog2fold = <... some bytes
> ...>
>
> I guess Q2 is produced by translator (i.e., what is currently in
> compiler/bootstrap/translation). I understand that part, if so.
>
> Is Q1 also produced by the translator? i.e., we roughly have Q1 = Q2?
> Or what is it?
>
> I think this would be interesting if it provided a principled way to
> substantially increase the speed for bootstrapping. It also seems like
> it would interact interestingly with the eval primitive. It seems to
> have no effect on the translation-time bottleneck for bootstrap speed,
> though.
>
> On 11 February 2017 at 16:34, Yong Kiam <tanyongkiam at gmail.com> wrote:
> > Hi dev,
> >
> > This is more of a random question than anything. I was wondering if it is
> > possible to get a theorem about k-fold bootstrap of the compiler, i.e.
> using
> > the compiler to iterate compilation on itself once in the logic and k-1
> > times (outside the logic).
> >
> > Concretely, 1-fold bootstrap would be what we have right now, so the code
> > being compiled in the logic looks like:
> >
> > ...
> > val main str = print (compile conf str);
> >
> > A 2-fold bootstrap could look like:
> >
> > ...
> > val cml_ast = ... //from an iterated translation of the compiler AST in
> HOL
> > into a translated AST
> > val main = print(compile conf (cml_ast));
> >
> > i.e. the output is a program, that when run, compiles the compiler AST.
> >
> > My sense is that such a k-fold bootstrap theorem could probably be done
> with
> > what we have now (replace cml_ast with the appropriate n-1 th
> translation).
> > The corresponding top-level correctness theorem would have some weird
> nested
> > assumptions about each time the bootstrap is ran.
> >
> > One possible use of 2-fold bootstrap: one could evaluate in HOL using a
> fast
> > (but less optimizing) version of the compiler, then turn on all the
> > optimizations inside cml_ast. It probably doesn't matter for our
> bootstrap
> > speed though.
> >
> >
> > _______________________________________________
> > Developers mailing list
> > Developers at cakeml.org
> > https://lists.cakeml.org/listinfo/developers
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170211/7ad5cb45/attachment.html>