Hello HOL users!
This email is a plea for anyone who can help me understand
computeLib.set_skip. Ideally I would like a simple description that could
be used as documentation for people who intend to use this function to good
effect.
Some initial information can be found below. Pointers to existing
documentation and/or responses from the author(s) of the code would be
especially welcome :)
Cheers,
Ramana
On Fri, May 17, 2013 at 11:22 AM, Anthony Fox <[email protected]> wrote:
> OK. I think I understand things a little better now. The complication is
> the interaction of computeLib.lazyfy_thm and computeLib.set_skip.
>
> The upshot is that not setting set_skip and a setting of NONE *are* the
> same. We get a benefit for COND just by using computeLib.lazyfy_thm.
>
> If you have a compset with
>
> COND_CLAUSES;
> val it =
> |- ∀t1 t2. ((if T then t1 else t2) = t1) ∧ ((if F then t1 else t2) =
> t2):
> thm
>
> as a rewrite and a set_skip of NONE then all arguments will be evaluated
> always. However, if we have
>
> computeLib.lazyfy_thm COND_CLAUSES;
> val it =
> |- (COND T = (λt1 t2. t1)) ∧ (COND F = (λt1 t2. t2)):
> thm
>
> then this rewrite fires on “T” or “F” and we only evaluate the “then” or
> “else” part. However, the “then/else” parts are evaluated when the
> condition is “x”.
>
> Now things get complicated...
>
> In both these cases (lazify and non-lazify) SOME i for i <= 1 are all
> equivalent. Here’s a table of what we get.
>
> | lazify | non-lazify
> | COND T | COND x | COND T | COND x
> NONE (not set) | ct | cte | cte | cte
> SOME i (i <= 1) | ct | c | ct | c
> SOME 2 | ct | ct | ct | ct
>
> So for COND, using lazify and no-skip is what we’re after for efficient
> symbolic evaluation. I suggest that this is what we’re after as the default
> for case constants as well. However, even if you use lazify_thm there may
> still be an advantage to setting the skip to SOME 1, i.e. we avoid doing
> evaluation on non-ground splits.
>
> Anthony
>
> On 17 May 2013, at 10:26, Anthony Fox <[email protected]> wrote:
>
> > I don’t really understand the workings of computeLib. It’s looking as if
> my initial understanding of the behaviour of set_skip is wrong. Will have
> to do some more experiments. - Anthony
> >
> > On 17 May 2013, at 09:34, Ramana Kumar <[email protected]>
> wrote:
> >
> >> Please go ahead and make this change then :)
> >> However, perhaps first it would be nice to add some documentation for
> set_skip, even if just in comments, because I'm confused about it:
> >> - Are there really 2 + |Z| possible settings for a constant? <not
> set>, NONE, and SOME i? I thought <not set> would be equivalent to one of
> the other settings.
> >> - What is the difference between NONE and SOME 0?
> >> - What does SOME (~n) mean?
> >>
> >
>
>
------------------------------------------------------------------------------
"Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE
Instantly run your Selenium tests across 300+ browser/OS combos.
Get unparalleled scalability from the best Selenium testing platform available
Simple to use. Nothing to install. Get started now for free."
http://p.sf.net/sfu/SauceLabs
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
