! natnum.txt - utility predicates for natural numbers in successor notation
!/ predicates:
(num ) - set of natural numbers in successor notation
(plus ) - sum of natural numbers
(times ) - product of natural numbers
(length ) - length of a sequence as a natural number
(ord ) - ordinal number of a finite set element
((< num) ) - < order of natural numbers (see relation.txt: <= > ..)
(iota <0..n>) - sequence of numbers from 0-n
We represent natural numbers 0,1,2,... as (`z), (`s `z), (`s `s `z), ....
(We use `z instead of `0 to make distinct from bit-atom `0.)
!\
! num - set of natural numbers in successor notation
(num (`z)). ! zero is a natural number
(num (`s $n))< ! successor of n is a natural number,
(num ($n)). ! if n is a natural number
! plus - addition of natural numbers
(plus %n (`z) %n)< (num %n). ! n + 0 = n
(plus %1 (`s $2) (`s $3))< ! n1 + n2+1 = n3+1
(plus %1 ($2) ($3)). ! if n1 + n2 = n3
! times - multiplication of natural numbers
(times %n (`z) (`z))< (num %n). ! n * 0 = 0
(times %1 (`s $2) %3')< ! n1 * n2+1 = n3'
(times %1 ($2) %3), ! if n1 * n2 = n3
(plus %3 %1 %3'). ! and n3 + n1 = n3'
! length - length of a sequence
(length () (`z)). ! empty sequence has length zero
(length (% $) (`s $l))< ! adding element increments length
(length ($) ($l)).
! select - select the ith element of a sequence (indexed from 0)
(select %k ($1 % $2) %)<
(length ($1) %k).
! ord - ordinal number of a finite set element
(ord %setname %elem %n)<
(finite_set %setname ($1 %elem $2)), ! (set elems must be unique)
(length ($1) %n).
! -- may not be needed in some cases?
! (< num) - < on natural numbers
((< num) (`z) (`s $n))< (num ($n)).
((< num) (`s $n1) (`s $n2))< ((< num) ($n1) ($n2)).
! see relation.txt for other relational operations <= > >= /= =
! iota - sequence of natural numbers from 0 thru n (APL function name)
! (iota <0..n>)
(iota (`z) ((`z))).
(iota (`s $n) ($0..n (`s $n)))<
(iota ($n) ($0..n)).
! -- see eval.txt for versions where and <0..n> are decimal symbols