Reduction Strengths and Forces

Cases come up when it is desirable to have some redices contracted but not others. To this end, an option is provided for specifying the strength of a redex,  and a variant of the Reduce tactic allows for a force  to be specified for reducing with. Strengths are forces are drawn from a partial order. A redex is only contracted when the reduction force applied to it is equal or greater than its strength.

A strength is associated with a redex in two ways:

• The strength is directly associated with the reduction rule for the redex.
• The strength is associated with the canonical term that is the principal argument of the non-canonical term of the redex.

Strengths and forces are ML tokens. The current supported strengths, in increasing order of strength  , are

`1`

beta redices

`2`

other primitive redices

`3`

abstract redices recursive

`4`

abstract redices non-recursive

`6`

module projection funs with coercion arguments. For example, the redex grp_op(add_grp_of_rng(r)) which contracts to rng_plus(r) has this strength.

`7`

functions creating module elements from concrete parts.

`1`

quasi-canonical redices. An example is the set_car term from the sets_1 theory when it has list and product discrete-set constructors as its principal argument. These constructors can also be found in the sets_1 theory.

`9`

irreducible terms.

Contraction conversions that should be sensitive to the force of reduction can be added to the abstract redex table using the function

The token argument that the conversion c takes is for the force with which reduction is being attempted.

Strengths can be associated with canonical terms using the function

The basic conversion for reducing with force F is ForceRedexC  ( F:tok). The conversion AbRedexC  always reduces with maximum force.