! ELC13_utilities.txt - Utility Functions for Emerging Languages Camp 2013 !/ This file gives axioms for various utility functions used in examples for the 2013 Emerging Languages Camp presentation on axiomatic language. The following utility functions are defined: == - identical expressions all_valid - all expressions in list are valid one_valid - one expression in list is valid seq_set - set is sequence of elements of other set `number - set of natural numbers `plus - addition of natural numbers `times - multiplication of natural numbers bitseq and char -> charstr examples below) (%seqset ())< (seq_set %seqset %set). (%seqset (% \$))< (seq_set %seqset %set), (%set %), (%seqset (\$)). ! -- Natural Numbers in Successor Notation and their Addition & Multiplication ! `number - set of natural numbers (in successor notation) (`number (`0)). ! zero is a natural number (`number (`s \$n))< (`number (\$n)). ! if n is a nat num, succ(n) is too ! `plus - addition of natural numbers (`plus %n (`0) %n)< (`number %n). (`plus %1 (`s \$2) (`s \$3))< (`plus %1 (\$2) (\$3)). ! `times - multiplication of natural numbers (`times %n (`0) (`0))< (`number %n). (`times %1 (`s \$2) %3')< (`times %1 (\$2) %3), (`plus %1 %3 %3'). ! -- Ordering of Natural Numbers -- ! num - map decimal digit character string to natural number (dec>num () (`0)). (dec>num (\$digits %digit) %num')< (dec>num (\$digits) %num), (`times %num (`s `s `s `s `s `s `s `s `s `s `0) %10num), (digit %digit %dignum), (`plus %10num %dignum %num'). ! num>dec - map natural number to decimal digit string (num>dec (`0) "0"). ! number zero represented by single zero digit (num>dec %num (%digit \$digits))< (dec>num (%digit \$digits) %num), (< '0' %digit). ! otherwise, leading digit is non-zero ! decnum - map decimal digit symbol to its natural number (decnum (` (%d \$d)) %num)< (dec>num (%d \$d) %num). ! -- Boolean Operations on `true/`false -- ! `and - "and" operation on `true/`false values (`and `false `false `false). (`and `false `true `false). (`and `true `false `false). (`and `true `true `true). ! `or - "or" operation on `true/`false values (`or `false `false `false). (`or `false `true `true). (`or `true `false `true). (`or `true `true `true).