1 2\chapter{Computing} 3 4This library provides a conversion that does rewrite and 5$\beta$-reduce any term, using a call by value strategy. 6 7%% Document CBV_CONV, from_list, add_clauses, new_rws 8 9\section{Strategy} 10 11The \ml{CBV\_CONV} conversion rewrites the equations in a call-by-value 12strategy, that is completely evaluates the arguments before the 13``function call'' (the application of a rewrite which left-hand side 14has this constant in its head). The reduction is weak, which means 15that reduction under abstractions are delayed as long as 16possible. However, when we know that an abstraction will never be 17applied, reductions are performed under it, so that we can actually 18reach the full normal form. 19 20The strategy is intentionally close to that of ML. This allows one to 21think \HOL\ has a programming language, and \ml{CBV\_CONV} is an 22evaluator which have the same complexity (with a large slow down factor, 23though) as usual compiled ML programs. 24 25The strategy differs from ML for abstractions: $\beta$-redexes are 26reduced in call by need. The usual call by value strategy can be 27achieved by replacing abstractions \verb#\x. e# by 28\verb#LET (\x. e)#, and reducing \ml{LET} with equation 29\verb#LET f x = f x#. 30 31The reason is to allow the evaluation of conditional expressions 32without evaluating both alternatives. We could use the weak reduction 33strategy to fake call by need: 34\begin{eqnarray*} 35\ml{COND'~T~x~y} & = & \ml{x()} \\ 36\ml{COND'~F~x~y} & = & \ml{y()} 37\end{eqnarray*} 38but this is a bit of overhead, and not very natural. Here, instead of 39rewriting equation \verb#COND T x y = x#, we use 40\verb#COND T = \x y. x#. The advantage of the second statement, is 41that only the condition is evaluated strictly, while in the first 42case, the two alternatives are also evaluated. Doing this 43transformation is not useful only in the case we need to evaluate 44arguments lazily, as shown above. It may be an improvement since 45$\beta$-reduction has been optimized, while pattern-matching is not a 46primitive notion in \HOL, and is slower. 47 48 49 50\section{Simplification sets} 51 52The \ml{compute} library has its own type of simplification sets, that 53can be as usual built from a list of theorems. These theorems must be 54conjunctions of possibly quantified equations, whose left-hand sides 55satisfy some condition to be defined below. Conjuncts not in the 56requested form are not used. 57 58Left-hand sides must be a constant applied to a list of 59patterns. Patterns are either a variable or a constant applied to 60other patterns. Abstractions cannot appear in patterns. 61\begin{eqnarray*} 62P & ::= & x \mid c~P_1 \ldots P_n 63\end{eqnarray*} 64This corresponds to the usual definition scheme by pattern-matching, 65slightly extended. Patterns need not be linear. If a variable occurs 66several times, it is checked that the instantiations are 67$\alpha$-convertibles. Beware, that only the weakly reduced forms are 68compared. For instance, reflexivity fails to solve the folowing example: 69\begin{verbatim} 70(\x. x) = (\x. (\y.y) x) 71\end{verbatim} 72 73 74Simplification sets are mutable objects: one creates an empty set and 75then adds lists of theorems to it. Function \ml{new\_rws} returns a 76new empty simplification set. Function \ml{add\_clauses} adds a list 77of theorems to a simplification set. It returns the list of rules that 78have been recognized, but it is mainly to check that everything was 79all right. Creation of a new simplification set and addition of a list 80of theorems can be combined using \ml{from\_list}. 81