Filter
Top Products
94 CHAPTER 12. MATHEMATICAL THEORIES
num_INDUCTION = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)
num_RECURSION = |- !e f. ?fn. (fn 0 = e) /\ (!n. fn (SUC n) = f (fn n) n)
The latter is used to define most of the arithmetic operations, including the
comparisons:
ADD = |- (!n. 0 + n = n) /\ (!m n. SUC m + n = SUC (m + n))
MULT = |- (!n. 0 * n = 0) /\ (!m n. SUC m * n = m * n + n)
EXP = |- (!m. m EXP 0 = 1) /\ (!m n. m EXP SUC n = m * m EXP n)
LE = |- (!m. m <= 0 = m = 0) /\
(!m n. m <= SUC n = (m = SUC n) \/ m <= n)
LT = |- (!m. m < 0 = F) /\ (!m n. m < SUC n = (m = n) \/ m < n)
EVEN = |- (EVEN 0 = T) /\ (!n. EVEN (SUC n) = ~EVEN n)
ODD = |- (ODD 0 = F) /\ (!n. ODD (SUC n) = ~ODD n)
Numerals are prettyprinted forms of an internal binary representation using two
constants:
BIT0 = |- BIT0 n = n + n
BIT1 = |- BIT1 n = SUC(n + n)
The rather artificial definition of the second is because multiplication (which
uses numeral 1 in its definition) has not yet been defined. Now these constants are
sufficient to express any number in binary. For example, we implement 37 as:
NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 _0))))))
The reader may wonder why we use the constant NUMERAL at all, instead of just
using BIT0, BIT1 and 0. The reason is that in that case one number becomes a
subterm of another (e.g. 1 is a subterm of 2), which can lead to some surprising acci-
dental rewrites. Besides, the NUMERAL constant is a useful tag for the prettyprinter.
The parser and printer transformations established, the theory of natural num-
bers can now be developed as usual. Most of the arithmetic operations are defined
by primitive recursion, indicating a simple evaluation strategy for unary notation.
For example one can evaluate 3 + 5 as follows:
3 + 5
SUC 2 + 5
SUC (2 + 5)
SUC (SUC 1 + 5)
SUC (SUC (1 + 5))
SUC (SUC (SUC 0 + 5)))
SUC (SUC (SUC (0 + 5)))
SUC (SUC (SUC 5))
SUC (SUC 6)
SUC 7
8