exponential EVAL with option_case_compute

[SOwens]

optionScript adds the following to the compset:

lazyfy_thm option_case_compute;
val it =
|- option_case = (λe f x. if IS_SOME x then f (THE x) else e):
thm

For programs like:

case do_lots_of_work of
| NONE => ...
| SOME answer => ...

do_lots_of_work is the x above, and is duplicated. For a recursive function where the recursion is in the do_lots_of_work, this leads to exponential blowup of EVAL. I'm not sure what the right general solution is, but for now I've re-written my functions to use this alternate option_case instead.

val eval_option_case_def = Define (eval_option_case NONE = λf1 f2. f1) ∧ (eval_option_case (SOME x) = λf1 f2. f2 x);

val eval_option_case_thm = Q.store_thm ("eval_option_case_thm",
!opt f1 f2. option_case f1 f2 opt = eval_option_case opt f1 f2,
rw [] >>
cases_on opt >>
rw [eval_option_case_def]);

val eval_option_case_cong = Q.store_thm ("eval_option_case_cong",
∀M M' u f. (M = M') ∧ ((M' = NONE) ⇒ (u = u')) ∧ (∀x. (M' = SOME x) ⇒ (f x = f' x)) ⇒ (eval_option_case M u f = eval_option_case M' u' f'),
metis_tac [optionTheory.option_case_cong, eval_option_case_thm]);

DefnBase.add_cong eval_option_case_cong;

val _ = set_skip the_compset eval_option_case (SOME 1);

[acjf3]

I guess there must have been some reason for having computeLib.lazyfy_thm there but I don't know what it is?

You could try:

computeLib.del_consts [optionSyntax.option_case_tm]

followed by

computeLib.add_funs [optionTheory.option_case_def]

or

computeLib.add_funs [optionTheory.option_case_compute]

Both seem to avoid computing "x" twice.

[konrad-slind]

As I recall, it was also intended to prevent re-computation of
sub-expressions.
But I never understood it.

Konrad.

On Thu, Oct 25, 2012 at 1:15 PM, acjf3 notifications@github.com wrote:

I guess there must have been some reason for having computeLib.lazyfy_thm
there but I don't know what it is?

You could try:

computeLib.del_consts [optionSyntax.option_case_tm]

followed by

computeLib.add_funs [optionTheory.option_case_def]

or

computeLib.add_funs [optionTheory.option_case_compute]

Both seem to avoid computing "x" twice.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/97#issuecomment-9788051.

[acjf3]

I guess it all comes down to where the "do_lots_of_work" is located. Using optionTheory.option_case_def or optionSyntax.option_case_tm will give problems when you have something of the form:

case x of
| NONE => do_lots_of_work
| SOME answer => do_lots_of_work

Scott's eval_option_case seems to avoid that problem.Doesn't this issue relate to

http://sourceforge.net/tracker/?func=detail&aid=601916&group_id=31790&atid=403400

which dates from 2002.

[konrad-slind]

Yes, that discussion on the issue tracker seems apropos. I suppose that
doing a little extra work would fix the problem. You'd need recognizers
and destructors defined for each datatype. Then the executable definition
for a case term would look like

case f1 ... fn ob =
let x = ob
in if is_C1 x then f1 (destC1 x)
else ...

I already have some infrastructure set up for defining recognizers and
destructors
for datatypes, and have added slots into the TypeBase for them.

Konrad.

On Thu, Oct 25, 2012 at 2:30 PM, acjf3 notifications@github.com wrote:

I guess it all comes down to where the "do_lots_of_work" is located. Using
optionTheory.option_case_def or optionSyntax.option_case_tm will give
problems when you have something of the form:

case x of
| NONE => do_lots_of_work
| SOME answer => do_lots_of_work

Scott's eval_option_case seems to avoid that problem.Doesn't this issue
relate to

http://sourceforge.net/tracker/?func=detail&aid=601916&group_id=31790&atid=403400

which dates from 2002.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/97#issuecomment-9790822.

[acjf3]

So you'd have to automatically apply these "evaluation" rewrites to everything prior to definitions being added to "the_compset"? If you just add these "recognizers" rewrites directly then you are still left with the problem that each of the cases with 0-ary constructors will always evaluate.

It's a shame that the arguments are the wrong way around in the first place. I guess it's a bit late now. Another option could be to automatically generate the "right" function at the same time and automatically apply the rewrite

X_case f1 f2 ... fn D = eval_X_case D f1 f2 ... fn

prior to adding stuff to the_compset. The rewrites for eval_X_case would be as Scott outlined, which should be more efficient than a (potentially long) sequence of if-then-else statements. This approach has the disadvantage that users could be left with instances of eval_X_case, which would be confusing, considering that they wouldn't pretty-print properly and other tool support wouldn't work. I suppose pretty-printing (and other) support could be added progressively, until the current version is made redundant. Is there any advantage to the current ordering?

[konrad-slind]

The pattern-match translation used by Define would have to be changed. Not
sure
if that's a real problem.

The order of the args to a case-definition was motivated (I think) by the
notion that
these are degenerate prim. rec. definitions, and so the function
represented by
the case is specified once the parameter function for each case is supplied.

Konrad.

On Thu, Oct 25, 2012 at 4:03 PM, acjf3 notifications@github.com wrote:

So you'd have to automatically apply these "evaluation" rewrites to
everything prior to definitions being added to "the_compset"? If you just
add these "recognizers" rewrites directly then you are still left with the
problem that each of the cases with 0-ary constructors will always evaluate.

It's a shame that the arguments are the wrong way around in the first
place. I guess it's a bit late now. Another option could be to
automatically generate the "right" function at the same time and
automatically apply the rewrite

X_case f1 f2 ... fn D = eval_X_case D f1 f2 ... fn

prior to adding stuff to the_compset. The rewrites for eval_X_case would
be as Scott outlined, which should be more efficient than a (potentially
long) sequence of if-then-else statements. This approach has the
disadvantage that users could be left with instances of eval_X_case, which
would be confusing, considering that they wouldn't pretty-print properly
and other tool support wouldn't work. I suppose pretty-printing (and other)
support could be added progressively, until the current version is made
redundant. Is there any advantage to the current ordering?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/97#issuecomment-9794104.

[acjf3]

I see. I think supporting the alternative argument order is probably the right way to go, although it could involve a fair amount of work (incompatibility problems).

The only other possibility that comes to mind is a version of set_skip that works for the last argument. The computeLib code is a bit of a mystery to me, so I don't really know how feasible that is...

[mn200]

Someone really does need to get their head around CBV_CONV, but changing the case constants to flip the order of arguments is probably quite doable. Backwards compatibility could be helped by using a new name for the underlying constant and then overloading things like option_case to the new form (flipping arguments). That way both the nice case notation and the use of bare option_case n sf optval would continue to work.

[mn200]

If someone has the time to look at this, the stumbling block is now the pattern-matching analysis that is done inside TFL (and the parsing of case expressions). The build goes as far as gcdTheory, where there is the first instance of a complicated function definition. I’m hoping that it will be sufficient to fix Pmatch.sml.

[konrad-slind]

Define calls Functional.mk_functional on functions with patterns.
I think that Pmatch is only called on case expressions on right-hand sides.
(But I could be wrong, it's been a while since I thought about this.)

I will have a quick look tonight and let you know how I get on.

Cheers,
Konrad.

On Wed, Nov 14, 2012 at 5:44 PM, Michael Norrish
notifications@github.comwrote:

If someone has the time to look at this, the stumbling block is now the
pattern-matching analysis that is done inside TFL (and the parsing of case
expressions). The build goes as far as gcdTheory, where there is the
first instance of a complicated function definition. I’m hoping that it
will be sufficient to fix Pmatch.sml.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/97#issuecomment-10391340.

[mn200]

You will need to

git checkout features/case-const-argflip

to see the changes I’ve made (they’re on a separate branch).

If you have outstanding uncommitted work in your repository, maybe make a fresh clone to do the work. Any commits and pushes you then make will go to the right place.

[mn200]

Ramana, I have no idea what the ot0 calls after various case definitions mean. I’ve ignored them for the moment.

[xrchz]

Is ot0 not defined in the same file somewhere? I would guess it's
ultimately a call to something in OpenTheoryMap that records the OpenTheory
name of the constant.

On Thu, Nov 15, 2012 at 12:39 AM, Michael Norrish
notifications@github.comwrote:

Ramana, I have no idea what the ot0 calls after various case definitions
mean. I’ve ignored them for the moment.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/97#issuecomment-10392827.

[mn200]

Yeah, of course. But the calls are of the form

ot0 "case" "option_case"

or similar and I'm worried that OpenTheory is expecting its case constants to have arguments ordered the old way

[mn200]

This feature is basically done, bar the shouting. The remaining question is best answered by people that use EVAL heavily. Should we do a set_skip or a lazyfy for case constants so that branches don’t get evaluated before they’re needed? I see that this is not done for COND at the moment (why not?).

It doesn’t seem like there’s a lot of point to switching the argument order if we don’t then use the opportunity gained to control evaluation of these case-constants, but I’m happy to be told how best that control should be achieved.

[xrchz]

Yes, the standard library has the arguments to option_case in the original
order.
I'm not sure what the best approach is for dealing with things like this.
One idea is in this email message
http://www.gilith.com/pipermail/opentheory-users/2011-September/000119.html.
When the change is as simple as flipping arguments, maybe the importer
should just do it on the fly... although dealing with partial applications
might be messy...

On Sat, Nov 17, 2012 at 8:23 PM, Michael Norrish
notifications@github.comwrote:

Yeah, of course. But the calls are of the form

ot0 "case" "option_case"

or similar and I'm worried that OpenTheory is expecting its case constants
to have arguments ordered the old way

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/97#issuecomment-10478486.

[acjf3]

"Should we do a set_skip or a lazyfy for case constants..."

You just need set_skip and this applies for COND as well. For conditionals we have the theorems:

COND_CLAUSES: |- !t1 t2. ((if T then t1 else t2) = t1) /\ ((if F then t1 else t2) = t2)
COND_ID: |- !b t. (if b then t else t) = t

with

set_skip the_compset boolSyntax.conditional NONE

This means that the arguments are evaluated depending on the condition (they are both evaluated when the condition doesn't evaluate to T or F). This is what we want for case statements as well.

For example:

if 1 + 2 = 3 then X else Y

will not evaluate Y and

if 1 + 2 = 2 then X else Y

will not evaluate X but

if 1 + 2 = n then X else Y

will evaluate X and Y.

If you want to avoid evaluation in the last example then you would have

set_skip the_compset COND (SOME 1)

I wouldn't recommend this because we often want to do symbolic evaluation.

Anyhow, lazify isn't needed at any point.

[mn200]

It should now be possible to get an efficient handling of case constants by using set_skip as necessary. As with conditional expressions, this isn’t turned on by default. As of my merge/close commit, everything builds successfully at -selftest 2.

[xrchz]

Yes this will break OpenTheory stuff because the constant has flipped
arguments in the standard library... one way around it would be to also
define the flipped arg constant in HOL4 and rewrite it away whenever it's
seen, or I suppose it should be possible to map a constant to an arbitrary
term (although OpenTheoryMap isn't set up that way at the moment) and map
the standard library constant to some combinator applied to the HOL4
constant.

On Sun, Nov 18, 2012 at 7:23 AM, Michael Norrish
notifications@github.comwrote:

Yeah, of course. But the calls are of the form

ot0 "case" "option_case"

or similar and I'm worried that OpenTheory is expecting its case constants
to have arguments ordered the old way

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/97#issuecomment-10478486.