! ho.ax - specification axioms for higher-order forms ! (Many of these are FP-style higher-order functional forms.) ! uses: form.ax !/ fp function format in AL: (f ) -- always 1-argument function functional forms are used to combine functions into larger functions. !\ ! comp - composition of (single-argument) functions in right-to-left order ((comp) %arg %arg). ! empty function list is identity function ((comp %f \$f) %arg %res')< ((comp \$f) %arg %res), (%f %res %ref'). ! map (apply-to-all) - map a function to each element of a sequence ! (just one argument in this case -- gives sequence of results) ! ((map ) ) - where ( ) for each element ((map %f) () ()). ((map %f) (%elem \$elems) (%elem' \$elems'))< (%f %elem %elem'), ((map %f) (\$elems) (\$elems')). !/ old: (map %f () ()). (map %f (%elem \$elems) (%elem' \$elems'))< (%f %elem %elem'), (map %f (\$elems) (\$elems')). ! or ... (map (\$f) () ()). ! function may include "constant" args (map (\$f) (%elem \$elems) (%elem' \$elems'))< (\$f %elem %elem'), (map (\$f) (\$elems) (\$elems')). !\ ! constr - apply sequence of functions to same argument giving seq of results ((constr) %arg ()). ((constr %f \$f) %arg (%res \$res))< (%f %arg %res), ((constr \$f) %arg (\$res)). ! filter - apply boolean pred to each element of sequence, keeping true values ! ((filter ) ) - is subset of where is `t ! ( <`t/`f>) - true/false predicate on an expression ((filter %pred) () ()). ((filter %pred) (%elem \$elems) (%elem \$elems'))< (%pred %elem `t), ((filter %pred) (\$elems) (\$elems')). ((filter %pred) (%elem \$elems) (\$elems'))< (%pred %elem `f), ((filter %pred) (\$elems) (\$elems')). ! -- use higher-order form for the shared condition? !/ old: (filter %pred () ()). (filter %pred (%elem \$elems) (%elem \$elems'))< (%pred %elem `t), (filter %pred (\$elems) (\$elems')). (filter %pred (%elem \$elems) (\$elems'))< (%pred %elem `f), (filter %pred (\$elems) (\$elems')). ! or ... (filter (\$pred) () ()). ! pred may include "constant" args (filter (\$pred) (%elem \$elems) (%elem \$elems'))< (\$pred %elem `t), (filter (\$pred) (\$elems) (\$elems')). (filter (\$pred) (%elem \$elems) (\$elems'))< (\$pred %elem `f), (filter (\$pred) (\$elems) (\$elems')). ! -- \$pred may represent boolean function plus some "constant" parameters ! -- Is there another string-vs-expr var notation that is nicer here??? !\ ! repeat - repeat 0 or more function applications ((repeat %f) % %). ! 0 evaluations is identity function ((repeat %f) %arg %result')< ! n+1 evaluations ((repeat %f) %arg %result), ! n evaluations (%f %result %result'). ! one more evaluation ! partial - turn multi-argument function into a single argument function ! by including the initial arguments as part of the function ! ("partial evaluation") ((partial %f \$initial_args) %last_arg %res)< (%f \$initial_args %last_arg %res). ! min - get element from sequence with minimum function result value ! - function result is a natural number ((min %fnat) (%elem) %elem). ! if just one value, that's the min ((min %fnat) (% \$) %)< ! first element is new minimum (%fnat % %n0), ((min %fnat) (\$) %min), (%fnat %min %n1), (<=num %n0 %n1). ((min %fnat) (% \$) %min)< ! first element is not new minimum (%fnat % %n0), ((min %fnat) (\$) %min), (%fnat %min %n1), (<=num %n1 %n0). ! -- Note that definition is ambiguous if new element value same as min. ! Thus the function nondeterministically picks any minimum element. ! -- use higher-order form for the common conditions: (ax (((min %fnat) (% \$) %) (<=num %n0 %n1)) (((min %fnat) (% \$) %min) (<=num %n1 %n0)) `< (%fnat % n0) ((min %fnat) (\$) %min) (%fnat %min %n1) ). ! define_func - define a name for a (single-argument) function expression (%name %arg %res)< (define_func %name %fn_expr), (%fn_expr %arg %res). !/ ! generalize - generalize certain associative binary operators with an identity ! -- We generalize operator to >2 arguments and to a sequence of >=0 args. (%binop %arg1 %arg2 \$args %arg' %result')< ! >2 arguments (generalize %binop %id), (%binop %arg1 %arg2 \$args %result), ! >=2 arguments (%binop %result %arg' %result'). ! adding an argument (%binop () %id)< ! empty argument sequence (generalize %binop %id). (%binop (\$args %arg) %result')< ! adding arg to sequence (generalize %binop %id), (%binop (\$args) %result), (%binop %result %arg %result'). ! move these to their original function definitions?: (generalize concat ()). (generalize plus 0). (generalize times (s 0)). (generalize and `t). (generalize or `f). ! Binary operator and binary relation higher-order forms: ! 1 - turn binary op into single arg function with operands in a 2-elem seq ! ((1 ) ( ) ) ((1 %binop) (%arg1 %arg2) %result)< (%binop %arg1 %arg2 %result). ! - also turn binary relation into single arg relation: ((1 %binrel) (%arg1 %arg2))< (%binrel %arg1 %arg2). ! 1* - apply first arg to sequence of second args to get sequence of results ! ((1* ) ((1* %binop) %arg1 () ()). ((1* %binop) %arg1 (%arg2 \$args2) (%res \$res))< (%binop %arg1 %arg2 %res), ((1* %binop) %arg1 (\$args2) (\$res)). ! - also apply to binary relation: ((1* %binrel) %arg1 ()). ((1* %binrel) %arg1 (%arg2 \$args2))< (%binrel %arg1 %arg2), (1* %binrel) %arg1 (\$args2)). ! *1 - apply sequence of first args to second arg to get sequence of results ! ((*1 ) ) ((*1 %binop) () %arg2 ()). ((*1 %binop) (%arg1 \$args1) %arg2 (%res \$res))< (%binop %arg1 %arg2 %res), ((*1 %binop) (\$args1) %arg2 (\$res)). ! - also apply to binary relation: ((*1 %binrel) () %arg2). ((*1 %binrel) (%arg1 \$args1) %arg2)< (%binrel %arg1 %arg2), ((*1 %binrel) (\$args1) %arg2). ! _ - concatenate the (sequences) of a fn result sequence into a single sequence ! ((_ ) ... ) ! -- number of function input args is arbitrary but last elem must be result ((_ %fn) \$args %result*)< (%fn \$args %result), ! get function result (concat %result %result*). ! concatenate result subsequences ! 1*_ - apply 1* to binary operator and concatenate the results ! ((1*_ ) ) ((1*_ %binop) %arg1 %arg2s %concatenated_results)< ((_ (1* %binop) %arg1 %arg2s %concatenated_results). ! ??? This is probably not needed! ! **_ - binary operator cartesian product in flat sequence ! ((**_ ) ! ( .. .. ... .. )) ! -- note that the 2nd argument cycles faster ((**_ %binop) %args1 %args2 %results)< ((_ (*1 (1* %binop))) %args1 %args2 %results). ! filter1* - filter second arg sequence for a Boolean binary operator ! ((filter1* ) ) ((filter1* %binop) %arg1 () ()). ((filter1* %binop) %arg1 (%arg2 \$arg2s) (\$arg2s'))< (%binop %arg1 %arg2 `f), ! result is false - arg2 not included ((filter1* %binop) %arg1 (\$arg2s) (\$arg2s')). ((filter1* %binop) %arg1 (%arg2 \$arg2s) (%arg2 \$arg2s'))< (%binop %arg1 %arg2 `t), ! result is true - arg2 is included ((filter1* %binop) %arg1 (\$arg2s) (\$arg2s')). ! finite_set - define a finite set in a single expression (%set %elem)< (finite_set %set (\$1 %elem \$2)). ! example: ! (finite_set day (Sun Mon Tue Wed Thu Fri Sat)). ! valid - generating multiple valid expressions from a single expression % < (valid \$1 % \$2). ! all_valid - combine valid expressions into single expression (all_valid). (all_valid % \$)< % , (all_valid \$). ! -- all expressions in list are valid ! one_valid - assert that at least one expression in list is valid (one_valid \$1 % \$2)< % . ! -- (at least) one expression in list is valid ! axiom - represent an axiom in a single expression ! (axiom .. ) %conclu < (axiom %conclu \$conds), (all_valid \$conds). ! axiom_set - generate a set of axioms from a single expression (axiom \$axiom)< (axiom_set \$1 (\$axiom) \$2). ! ax - define multiple axioms with shared conditions ! (ax ( .. ) .. ( .. ) ! `< .. ) -- shared conditions (axiom %conclu \$conds \$shared_conds))< (ax \$ax1 (%conclu \$conds) \$ax2 `< \$shared_conds). ! -- no shared condition can be an `< atom ! eval - Lisp-like expression evaluation (from paper) (eval (quote %expr) %expr). ! value is unevaluated expression (eval %dec_sym %value)< ! value of decimal number symbol (dec_sym %dec_sym %value). (eval (%fn \$args) %result)< ! evaluate function on arguments (eval* (\$args) (\$results)), ! evaluate argument expressions (%fn \$results %result). ! evaluate function on argument results ! -- this works for functions that yield a single result at end of list