! eval.txt - predicates for expression evaluation involving decimal num symbols !/ (eval [] ) - evaluate expr to get natural num value (equation ( = []) - equality between two nat num exprs (constraints (....) ) - sel args given constraints (constraint ) - select arg tuples satisfying pred (bool_eval ( ) [] ) - eval Boolean expr (minimize ) - sel an arg tuple that minimizes expr (digit_char ) - set of decimal digit characters ('0' .. '9') (digit <1-digit_sym>) - set of symbols with 1 digit (0 .. 9) (decsym ) - symbol with 1 or more decimal digit characters (decconst (....) ) - concatenate digit syms to form const (dec>num ) - map decimal number symbol to natural number (num>dec ) - map nat num to dec sym (only 0 has leading 0) (iota <0..n>) - sequence of natural numbers 0-n given decimal symbol n (iota_d ) - seq of decimal symbol nums 0-n given dec or nat num n !\ ! eval - evaluate a natural number arithmetic expression ! (eval () [] ) ! E = E + T | T -- Expression ! T = T * P | P -- Term ! P = ( E ) | N -- Primary ! N = Const | Var -- Numeric value ! Const = constant formed by concatenating one or more decimal digit symbols ! Var = variable symbol _ represents th value in arg seq (eval ($E) $args %val)< (eval_E ($E) $args %val). ! -- Optional arguments are used for blending problem, but not for the ! SEND+MORE=MONEY problem. ! eval_E - evaluate an Expression: E = E + T | T (eval_E ($E + $T) $args %valE+T)< ! E = E + T (eval_E ($E) $args %valE), (eval_T ($T) $args %valT), (plus %valE %valT %valE+T). (eval_E ($T) $args %val)< ! E = T (eval_T ($T) $args %val). ! eval_T - evaluate a Term: T = T * P | P (eval_T ($T * $P) $args %valT*P)< ! T = T * P (eval_T ($T) $args %valT), (eval_P ($P) $args %valP), (times %valT %valP %valT*P). (eval_T ($P) $args %val)< ! T = P (eval_P ($P) $args %val). ! eval_P - evaluate a Primary: P = (E) | N (eval_P ($E) $args %val)< ! P = ( E ) (eval_E $E $args %val). (eval_P ($N) $args %val)< ! P = N (eval_N ($N) $args %val). ! eval_N - evaluate a Numeric value - constant or variable ! N = C | V (eval_N ($C) $args %val)< ! N = C (eval_C ($C) $args %val). (eval_N (%V) $args %val)< ! N = V (eval_V (%V) $args %val). ! eval_C - evaluate a Constant of >0 decimal digit symbols (eval_C ($C) $args %n)< (decconst ($C) %decsym), ! concat multiple decimal symbols into one (dec>num %decsym %n). ! get its natural number value ! eval_V - evaluate a Variable by getting its value from arg sequence ! -- Variable is symbol with underscore followed by digits: _ ! Digits define index of value in argument sequence. (eval_V (` ('_' $dc)) %args %val)< (dec>num (` ($dc)) %k), ! index of variable (select %k %args %val). ! equation - equality between two natural number expressions (equation ($E1 = $E2) $args)< (eval ($E1) $args %val), (eval ($E2) $args %val). ! both sides have the same natural number value ! constraints - select subset of argument tuples that satisfy some constraints ! (constraints ) (constraints () %args %args). ! all args satisfy if no constraints (constraints ($cnstrs %cnstr) %args %args')< ! multiple contraints (constraints ($cnstrs) %args %argsx), (constraint %cnstr %argsx %args'). ! testing single constraint ! constraint - select subset of arg tuples that satisfy a contraint predicate (constraint %pred () ()). ! no argument tuples (constraint %pred ($tuples %tuple) ($tuples'))< ! arg tuple not selected (constraint %pred ($tuples) ($tuples')), (bool_eval %pred %tuple `false). ! arg tuple doesn't satisfy predicate (constraint %pred ($tuples %tuple) ($tuples' %tuple))< ! tuple selected (constraint %pred ($tuples) ($tuples')), (bool_eval %pred %tuple `true). ! arg tuple satisfies predicate ! bool_eval - evaluate Boolean expression to get `true or `false ! (bool_eval ( ) [] ) ! -- predicate has a single relation =, !=, <, <=, >, >= on nums or bit exprs ! -- no logical operations (and, or, not) for now ! -- optional argument tuple (with vars _0, _1, _2, ...) may be present (valid (bool_eval ($expr1 %relop $expr2) $arg_tuple `true) (bool_eval ($expr1 %oppop $expr2) $arg_tuple `false))< ! opposite relop (eval ($expr1) $arg_tuple %val1), (eval ($expr2) $arg_tuple %val2), (in (%relop %oppop) ((= /=) (/= =) (< >=) (>= <) (<= >) (> <=)), ! -- pairing operators and their opposites (%relop %val1 %val2). ! get relation between the two values ! minimize - select [an] argument tuple that minimizes expression ! (minimize ) ! (Note that this works on bit exprs, such as character strings.) (valid (axioms ((minimize %expr (%tup) %val %tup)) ! single tuple is minimum ((minimize %expr ($tups %tup) %val %tup ) (<= %val %valm)) ! new min ((minumize %expr ($tups %tup) %valm %tupm) (<= %valm %val )) ! same min ! -- We non-deterministically get all minimum tuples if more than one. ))< (minimize %expr ($tups) %valm %tupm), ! min of existing tuples (eval %expr %tup %val). ! new tuple value ! digit_char - set of decimal digit characters: '0' .. '9' (finite_set digit_char "0123456789"). ! digit - set of single-digit symbols: 0 .. 9 (digit (` (%dc)))< (digit_char %dc). ! decsym - symbol with one or more decimal digits (ex: 317) (decsym (` (%dc))< ! symbol always has at least one digit (digit_char %dc). (decsym (` ($dc %dc))< ! adding a digit to the symbol (decsym (` ($dc))), ! (leading zero ok here) (digit_char %dc). ! decconst - concatenation of sequence of decimal symbols into one (decconst (%d) %d)< ! constant has at least one decimal symbol (decsym %d). (decconst ((` ($dc)) $d) (` ($dc $dcx)))< ! adding dec sym to constant (decsym (` ($dc))), ! digit characters are concatenated (decconst ($d) (` ($dcx))). ! dec>num - map a decimal digit symbol to its natural number value ! (Leading zero digits are ok.) (dec>num (` ()) (`z)). ! (invalid) null-digit symbol evaluates to zero (dec>num (` ($dc %dc)) %n')< ! appending a digit to the symbol (dec>num (` ($dc)) %n), (ord digit_char %dc %k), (times %n (`s `s `s `s `s `s `s `s `s `s `z) %10n), (plus %10n %k %n'). ! num>dec - map natural number to (unique) decimal symbol ! (No leading zero except for the number 0 itself.) (num>dec %num (` (%digit $digits)))< ! positive natural numbers (dec>num (` (%digit $digits)) %num)< (/= %digit '0'). ! 1st digit not zero (num>dec (`z) (` "0")). ! zero ! iota - sequence of natural numbers 0-n given decimal symbol n ! (See natnum.txt for iota where n is natural number.) ! (Note that we have "overloaded" this name.) (iota %dn %0..n)< (dec>num %dn %n), (iota %n %0..n). ! iota_d - generate sequence of decimal symbol natural numbers 0..N ! (iota_d (0 1 2 ... )) -- N >= 0, N may be pure nat num or dec sym (iota_d %N %d0-N)< (iota %N %0-N), ! generate pure natural numbers ((map num>dec) %0-N %d0-N). ! map pure nat num seq to decimal numbers