Studies with the Zero Prover

Studies with the Zero Prover(s)

The Basic Version
The Non-Reconstructing Optimization
A Rudimentary Timing Study (Examples & Times)
The Timing Functions

Preliminary Conclusion

In the presence of more straightforward techniques of optimization (use of "as" to avoid reconstruction, use of "_" to avoid bindings), when applied to a simple method like this, the benefits of using raise/handle to avoid term reconstruction are minimal. (In fact, it complicates the code slightly and made for typically--but minimally-- longer execution times.) Even when the data item is rather large (a score or more arithmetic operators) and features lots of terms which would not be simplified by the procedure--where we figured to get the benefit--the "optimized" version was still slightly slower.

Maybe I need to consider a "bigger/more complicated" procedure, or maybe my examples are too wimpy...