Filter
Top Products
78 CHAPTER 9. DERIVED RULES
!n. (m / SUC n) * SUC n = m
We allow variables to be repeated in patterns (in the jargon, ‘nonlinear’ pat-
terns); this does in theory introduce an element of nondeterminacy but this is
resolved by always traversing the term to be matched top-down and picking the
first match. For example:
|- (!x. P (SUC x) x) = !x. 0 < x ==> P x (PRE x)
matched against:
!n. (m / SUC n) * (n + 1) = m
will yield
|- (!n. (m / SUC n) * (n + 1) = m) =
(!n. 0 < n ==> (m / n) * (PRE n + 1) = m)
rather than
|- (!n. (m / SUC n) * (n + 1) = m) =
(!n. 0 < n ==> (m / SUC(PRE n)) * (PRE n + 1) = m)
Second, as well as binding instances, first-order matchable parts of the term are
used to resolve more variables. The implementation reflects this: in a first pass, all
first order parts are dealt with (in first order matches, all the term is dealt with).
Then the new variable assignments are used to keep the overall match deterministic.
For example:
|- C x y ==> P x y
(where C is a constant and so not eligible itself as a higher order pattern) will
deterministically match:
C a b ==> (a + b = 27)
whereas the respective consequents could not be matched deterministically.
Note, by the way, that even beta-conversion can be implemented as a higher
order rewrite rule, and hence conveniently thrown into a bunch of rewrites instead
of being called separately.
#BETA_THM;;
it : thm = |- !f y. (\x. f x) y = f y
But note that rewrites with the following theorem go into an infinite loop at any
beta-redex because of higher order matching!
#ETA_AX;;
it : thm = |- !t. (\x. t x) = t