|
|
|
|
|
Notation:
|
|
|
|
|
|
```wiki
|
|
|
m,n,k: natural numbers
|
|
|
a,b,c: types of kind Nat
|
|
|
```
|
|
|
|
|
|
|
|
|
When overlapping, earlier rules take precedence (as in Haskell multi-equation definitions).
|
|
|
(NOTE: The rules involving constants but no computation could be generalized
|
|
|
to work for variables as well, as long as we know that the variables
|
|
|
are in the acceptable ranges. Such information could be computed
|
|
|
from the \<= model, perhaps.)
|
|
|
|
|
|
|
|
|
Top-level interactions for `TypeNat`:
|
... | ... | @@ -30,14 +25,16 @@ Top-level interactions for +. |
|
|
|
|
|
```wiki
|
|
|
(m + n ~ k) <=> {m + n == k}
|
|
|
|
|
|
(m + a ~ n) <=> a ~ {n - m} -- n >= m
|
|
|
(a + m ~ n) <=> a ~ {n - m} -- n >= m
|
|
|
(0 + a ~ b) <=> a ~ b
|
|
|
(a + 0 ~ b) <=> a ~ b
|
|
|
(a + b ~ 0) <=> (a ~ 0, b ~ 0)
|
|
|
|
|
|
(a + b ~ a) <=> (b ~ 0)
|
|
|
(a + b ~ b) <=> (a ~ 0)
|
|
|
|
|
|
(a + a ~ b) <=> (2 * a ~ b)
|
|
|
(a + b ~ 0) <=> (a ~ 0, b ~ 0) -- XXX: Drop this, follows from <= rules?
|
|
|
|
|
|
(a + m ~ b) <=> (m + a ~ b) -- simple normalization cuts down on some rules
|
|
|
```
|
|
|
|
... | ... | @@ -46,15 +43,16 @@ Top-level interactions for \*. |
|
|
|
|
|
```wiki
|
|
|
(m * n ~ k) <=> {m * n == k}
|
|
|
(m * a ~ n) <=> a ~ {n / m} -- m `divides` n
|
|
|
(a * m ~ n) <=> a ~ {n / m} -- m `divides` n
|
|
|
(m * a ~ n) <=> a ~ { n / m } -- m `divides` n, False otherwise
|
|
|
|
|
|
(0 * a ~ b) <=> b ~ 0
|
|
|
(a * 0 ~ b) <=> b ~ 0
|
|
|
(1 * a ~ b) <=> a ~ b
|
|
|
(a * 1 ~ b) <=> a ~ b
|
|
|
(m * a ~ a) <=> a ~ 0 -- 2 <= m
|
|
|
|
|
|
(a * b ~ 1) <=> (a ~ 1, b ~ 1)
|
|
|
(a * a ~ b) <=> a ^ 2 ~ b
|
|
|
(m * a ~ a) <=> a ~ 0 -- 2 <= m
|
|
|
|
|
|
(a * m ~ b) <=> (m * a ~ b) -- simple normalization cuts down on some rules
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -62,11 +60,14 @@ Top-level interactions for `^` |
|
|
|
|
|
```wiki
|
|
|
(m ^ n ~ k) <=> {m ^ n == k}
|
|
|
(m ^ a ~ n) <=> a ~ {log m n} -- log (base m) of n exists
|
|
|
(a ^ m ~ n) <=> a ~ {root m n} -- m-th root of n exists
|
|
|
|
|
|
(m ^ a ~ n) <=> a ~ {log m n} -- log (base m) of n exists, False otherwise
|
|
|
(1 ^ a ~ b) <=> b ~ 1
|
|
|
(m ^ a ~ a) <=> False -- m /= 1
|
|
|
|
|
|
(a ^ m ~ n) <=> a ~ {root m n} -- m-th root of n exists, False otherwise
|
|
|
(a ^ 0 ~ b) <=> b ~ 1
|
|
|
(a ^ 1 ~ b) <=> a ~ b
|
|
|
(a ^ m ~ a) <=> (a <= 1) -- 2 <= m
|
|
|
(1 ^ a ~ b) <=> b ~ 1
|
|
|
(m ^ a ~ a) <=> False -- m /= 1
|
|
|
|
|
|
``` |
|
|
\ No newline at end of file |