CBV_CONV
computeLib.CBV_CONV : compset -> conv
Call by value rewriting.
The conversion CBV_CONV expects a simplification set and a term. Its
term argument is rewritten using the equations added in the
simplification set. The strategy used is somewhat similar to ML's, that
is call-by-value (arguments of constants are completely reduced before
the rewrites associated to the constant are applied) with weak reduction
(no reduction of the function body before the function is applied). The
main differences are that beta-redexes are reduced with a call-by-name
strategy (the argument is not reduced), and reduction under binders is
done when it occurs in a position where it cannot be substituted.
The simplification sets are mutable objects, this means they are
extended by side-effect. The function new_compset will create a new
set containing reflexivity (REFL_CLAUSE), plus the supplied rewrites.
Theorems can be added to an existing compset with the function
add_thms.
This function (add_thms) scans the supplied theorems using
BODY_CONJUNCTS. Let thm be one such element. If thm is of the form
P1 ⇒ P2 ⇒ ... ⇒ t for possibly-zero implications, then proccess t.
If t is an equation, add it as a reduction rule. If t is of the form
¬t', then add the rule t ⇔ F, otherwise add the rule t ⇔ T. If
there is at least one implication then also add P1 ⇒ P2 ⇒ ... ⇒ t ⇔ T.
It is also possible to add conversions to a simplification set with
add_conv. The only restriction is that a constant (c) and an arity
(n) must be provided. The conversion will be called only on terms in
which c is applied to n arguments.
Two theorem "preprocessors" are provided to control the strictness of
the arguments of a constant. lazyfy_thm has pattern variables on the
left hand side turned into abstractions on the right hand side. This
transformation is applied on every conjunct, and removes prenex
universal quantifications. A typical example is COND_CLAUSES:
(COND T a b = a) /\ (COND F a b = b)
Using these equations is very inefficient because both a and b are
evaluated, regardless of the value of the boolean expression. It is
better to use COND_CLAUSES with the form above
(COND T = \a b. a) /\ (COND F = \a b. b)
The call-by-name evaluation of beta redexes avoids computing the unused branch of the conditional.
Conversely, strictify_thm does the reverse transformation. This is
particularly relevant for LET_DEF:
LET = \f x. f x --> LET f x = f x
This forces the evaluation of the argument before reducing the
beta-redex. Hence the usual behaviour of LET.
It is necessary to provide rules for all the constants appearing in the
expression to reduce (all also for those that appear in the right hand
side of a rule), unless the given constant is considered as a
constructor of the representation chosen. As an example,
reduceLib.num_compset creates a new simplification set with all the
rules needed for basic boolean and arithmetical calculations built in.
Example
- val rws = computeLib.new_compset [computeLib.lazyfy_thm COND_CLAUSES];
> val rws = <compset> : compset
- computeLib.CBV_CONV rws ``(\x.x) ((\x.x) if T then 0+0 else 10)``;
> val it = |- (\x. x) ((\x. x) (if T then 0 + 0 else 10)) = 0 + 0 : thm
- computeLib.CBV_CONV reduceLib.num_compset
``if 100 - 5 * 5 < 80 then 2 EXP 16 else 3``;
> val it = |- (if 100 - 5 * 5 < 80 then 2 ** 16 else 3) = 65536 : thm
Failing to give enough rules may make CBV_CONV build a huge result, or
even loop. The same may occur if the initial term to reduce contains
free variables.
val eqn = bossLib.Define `exp n p = if p=0 then 1 else n * (exp n (p-1))`;
val _ = computeLib.add_thms [eqn] rws;
- computeLib.CBV_CONV rws ``exp 2 n``;
> Interrupted.
- computeLib.set_skip rws ``COND`` (SOME 1);
> val it = () : unit
- computeLib.CBV_CONV rws ``exp 2 n``;
> val it = |- exp 2 n = if n = 0 then 1 else 2 * exp 2 (n - 1) : thm
The first invocation of CBV_CONV loops since the exponent never
reduces to 0. Below the first steps are computed:
exp 2 n
if n = 0 then 1 else 2 * exp 2 (n-1)
if n = 0 then 1 else 2 * if (n-1) = 0 then 1 else 2 * exp 2 (n-1-1)
...
The call to set_skip means that if the constants COND appears
applied to one argument and does not create a redex (in the example, if
the condition does not reduce to T or F), then the forthcoming
arguments (the two branches of the conditional) are not reduced at all.
Failure
Should never fail. Nonetheless, using rewrites with assumptions may cause problems when rewriting under abstractions. The following example illustrates that issue.
- val th = ASSUME “0 = x”;
- val tm = Term`\(x:num). x = 0`;
- val rws = from_list [th];
- CBV_CONV rws tm;
This fails because the 0 is replaced by x, making the assumption
0 = x. Then, the abstraction cannot be rebuilt since x appears free
in the assumptions.