EtnaNova_ELEM_supplement.stl
package logic_syntax_analysis_pak2; -- second part of logic_syntax_analysis_pak -- This package is a supplement to the main package 'logic_syntax_analysis_pak', -- separated out only because that other file was becoming uncomfortably large. -- The processes found here handle monotone and algebraic inference, and several utilities -- as seen in the header below. -- It is also used as a repository for obsolete versions of inference and related codes. -- This file also includes (at its end) the package 'algebraic_parser', an auxiliary package for simple algebraic parsing, -- useful for communicating with external provers which use only a simple algebraic language, but possibly -- with operator signs and precedences different from those meeting the standard SETL syntactic conventions. var monotonicity_props := {}; -- maps an operator into its declared monotonicity properties var var_generator := 0; -- used to generate VRXn_ variables var alg_of := {}, alg_role_of := {}; -- globals used in algebraic standardization (made visible for testing only) var sub_from_addn := {},reversal_from_addn := {},zero_from_addn := {},one_from_addn := {},mult_from_addn := {}; var ring_from_addn := {}; -- globals used in algebraic standardization (visible for testing only) var mismatched_args,mismatched_symbvars,mismatched_expn; -- substitution mismatches for diagnosis -- *********** Monotonicity-based inference *********** procedure monotone_infer(node); -- prepare to deduce a formula by monotone inference -- called from 'check_a_monot_inf' in top-level package procedure test_monotone_infer; -- test of the monotone_infer procedure -- *********** Algebraic inference *********** procedure find_algebraic_nodes(tree); -- finds the algebraic nodes in a tree, and returns them procedure standardize_subtree(tree,plus_op); procedure re_nest(flattened_tree); -- reconvert a standardized (flattened) tree to its ordinary 'nested' form procedure canorder_subtree(tree); -- sorts the terms and factors of a standardized (flattened) subtree and performs cancellations procedure generate_algebraic_identity(tree); -- generates identity of tree with standardized form procedure find_ring_members(tree); -- collects the ring membership assertions at the top conjuctive level of a tree procedure post_alg_roles(stg); -- adds an algebraic set to alg_of and alg_role_of maps -- *********** Miscellaneous tree searching and transformation routines *********** procedure find_setformers_and_quants(tree); -- finds the setformer and quantifier nodes in a tree, and returns them procedure find_fnc_symbs(node); -- find the function symbols in a tree procedure dequantify(tree,substitution_tup); -- general substitution for quantified variables procedure replace_fcn_symbol(expn,symbol,symbvars,symbdef); -- at each occurrence of a symbol in expn, finds the arguments of symbol, -- and substitutes them in symbdef for the indicated free variables of symbdef -- replacing the symbol occurrence by this substituted form -- *********** Test Collection *********** procedure test_find_fnc_symbs; -- test of the find_fnc_symbs procedure procedure test_replace_fcn_symbol; -- test of the replace_fcn_symbol procedure procedure test_dequantify; -- test of the dequantify procedure -- *********** Obsolete code *********** procedure monotone_inference(node1,node2); -- obsolete procedure test_monotone_inference; -- test of the monotone_inference procedure -- obsolete -- calculates conditions for value defined by node 1 to include value defined by node 2 end logic_syntax_analysis_pak2; package body logic_syntax_analysis_pak2; -- second part of logic_syntax_analysis_pak use string_utility_pak,parser,sort_pak; -- standard Setl utilities use logic_parser_globals; -- global variables for logic parser and other basic packages use logic_parser_aux; -- auxiliary routines for logic basic routines use logic_syntax_analysis_pak; -- use the main package of inferencing routines var difference_quintuples := {},monot_var_ctr := 0; -- globals used by 'monotone_inference_in' var all_fnc_symbs := {}; -- globals used in 'find_fnc_symbs' var debug_flag := false; -- debugging print switch const builtin_fcns:= {"CAR", "CDR","ast_arb","ast_if_expr","ast_if", "ast_range", "ast_domain","ast_nelt"}; -- the definitions of these are considered to be 'built-in' -- **************************************************** -- *********** Monotonicity-based inference *********** -- **************************************************** -- This group of routines handle prof by monotonicity. Inferencing of this kind assumes that the -- monotonicity properties of some of the operators and other constructions found in the -- formulae which are being processed are known, at least in part. The routines seen below are prepared to handle -- inferences involving formulae of the form e1 incs e2, e1 •incin e2, e1 •imp e2, e1 = e2, and e1 •eq e2. -- Analysis of a formula of one of these forms always produces a stronger collection of simpler clauses, which -- can then replace the original clause in the ELEM step used to complete the desired inference. -- Examples of formulae which can easily be verified by monotone inference are -- #pow(Un(a + b)) incs #pow(Un(c)) and Un(a + b) = Un(a) + Un(b) -- and -- {e(x): x in a | P(x)} + {e(x): x in a | Q(x)} = {e(x): x in a | Q(x) or P(x)} -- The first two of these evidently depend on prior knowledge of the monotonicity properties of -- pow, Un, and cardinality. These are made known to the Ref system by special declarations, which invoke the -- 'post_monotone' routine seen below. -- The general action of the family of routines in this 'monotonicity' set are most easily understood -- by considering one of them, namely monotone_infer_ast_incs, whhich handles formulae of the form e1 incs e2. -- In this case, we traverse the syntax trees of e1 and e2 downward in parallel as long as the lead operators of the nodes encountered -- are identical, have known monotonicity properties, and none bind any variables. -- When there are identical lead operators, we propagate a incs a' to corresponding arguments of increasing -- monotonicity, but a' incs a to corresponding arguments of decreasing monotonicity. -- For operator arguments of indeterminate monotonicity, monotone_infer_ast_eq is called. -- When there are different lead operators, we demand inclusion of the expression values represented by the subtrees, -- except in the following cases: -- (i) a incs b + c is treated as the conjunct (a incs b) & (a incs c) -- (ii) a * b incs c is treated as the conjunct (a incs c) & (b incs c) -- Consider, for example the first inclusion seen above. Assuming that the monotonicity of the operators -- pow, Un, and cardinality have been declared, parallel traversal of the parse trees of -- #pow(Un(a + b)) and #pow(Un(c)) reduces this inclusion to a + b incs c, which is therefore the clause generated -- for handling by the concluding ELEM deduction. For more examples of formulae which can be handled by monotone inference, -- see the routine 'test_monotone_infer' below. procedure monotone_infer(node); -- deduce a formula by monotone inference -- this converts a node of any of the special cases that can be handled into a collection -- of simpler clauses to be verified by ELEM reasoning. If the clause cannot be handled, -- node is returned. --print("monotone_infer: ",node); if not is_tuple(node) then return node; end if; [n1,n2,n3] := node; --print("monotone_infer: ",n1," ",unparse(n2)," ",unparse(n3)); case n1 when "ast_eq" => return disjoin_really(disjoin_many({node,monotone_infer_ast_eq(n2,n3)})(2)); when "ast_incs" => return disjoin_really(disjoin_many({node,monotone_infer_ast_incs(n2,n3)})(2)); when "DOT_INCIN" => return disjoin_really(disjoin_many({node,monotone_infer_ast_incs(n3,n2)})(2)); when "DOT_IMP" => return disjoin_really(disjoin_many({node,monotone_infer_ast_imp(n2,n3)})(2)); when "DOT_EQ" => return disjoin_really(disjoin_many({node,monotone_infer_ast_equiv(n2,n3)})(2)); otherwise => return node; end case; end monotone_infer; procedure monotone_infer_ast_incs(n1,n2); -- deduce an inclusion by monotone inference -- We traverse the two syntax trees downward as long as the lead operators of the nodes encountered -- are identical, have known monotonicity properties, and none bind any variables. -- When there are identical lead operators, we propagate a incs a' to corresponding arguments of increasing -- monotonicity, but a' incs a to corresponding arguments of decreasing monotonicity. -- For operator arguments of indeterminate monotonicity, monotone_infer_ast_eq is called. -- When there are different lead operators, we demand inclusion of the expression values represented by the subtrees, -- except in the following cases: -- (i) a incs b + c is treated as the conjunct (a incs b) & (a incs c) -- (ii) a * b incs c is treated as the conjunct (a incs c) & (b incs c) -- (iii) n1 and n2 are both setformer nodes, of forms like {e(x): x in s | P(x)}. In this case we form the conjunct -- ((s incs s') or monotone_infer_ast_incs(s,s')) & (FORALL x in s | e(x) = e'(x)) & (FORALL x in s' | P'(x) •imp P(x)), -- omitting any conjunct which is evident by blobbing. -- If both templates apply, the disjunction of both these sets of clauses should be formed. --print("monotone_infer_ast_incs: ",unparse(n1)," ",unparse(n2)); if is_string(n1) and is_string(n2) then return if n1 = n2 then "TRUE" else ["ast_incs",n1,n2] end if; end if; [blob_1,blob_2] := blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]]); -- call special 'common blobbing' function if blob_1 = blob_2 then return "TRUE"; end if; -- check for more general equality evident by blobbing if is_string(n2) then if n1(1) = "ast_add" then return disjoin_many({["ast_incs",n1,n2],monotone_infer_ast_incs(n1(2),n2),monotone_infer_ast_incs(n1(3),n2)}); else return ["ast_incs",n1,n2]; end if; end if; if is_string(n1) then if b1 = "ast_add" then return disjoin_many({["ast_incs",n1,n2],conjoin_many({monotone_infer_ast_incs(a2,n2),monotone_infer_ast_incs(a3,n2)})}); else return ["ast_incs",n1,n2]; end if; end if; [a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2; -- otherwise decompose the two trees if a1 = "ast_genset_noexp" then -- convert to form with expression iter_var := a2(2)(2); n1 := [a1,a2,a3,a4] := ["ast_genset",iter_var,a2,a3]; end if; if b1 = "ast_genset_noexp" then -- convert to form with expression iter_var := b2(2)(2); n2 := [b1,b2,b3,b4] := ["ast_genset",iter_var,b2,b3]; end if; if a1 = b1 then -- identical lead operators case a1 when "ast_if_expr" => -- inclusion of conditional expressions cond := monotone_infer_ast_equiv(a2,b2); return disjoin_many({["ast_incs",n1,n2], if cond /= "TRUE" then conjoin_many({cond,monotone_infer_ast_incs(a3,b3),monotone_infer_ast_incs(a4,b4)}) else monotone_infer_ast_incs(a3,b3) end if}); when "ast_add","ast_mult" => -- commutative expressions return disjoin_many({["ast_incs",n1,n2], conjoin_many({monotone_infer_ast_incs(a2,b2),monotone_infer_ast_incs(a3,b3)}), conjoin_many({monotone_infer_ast_incs(a2,b3),monotone_infer_ast_incs(a3,b2)})}); when "ast_sub" => -- set difference return disjoin_many({["ast_incs",n1,n2],conjoin_many({monotone_infer_ast_incs(a2,b2),monotone_infer_ast_incs(b3,a3)})}); when "ast_pow","ast_nelt" => -- SETL builtin monadics; both of these are monotone return disjoin_many({monotone_infer_ast_incs(a2,b2),["ast_incs",n1,n2]}); -- test arguments for equality when "ast_genset" => -- setformer -- setformer pairs are treated in a special way if their sequences itseq of iterators are of the same -- length. if #(itlist1 := a3(2..)) /= #(itlist2 := b3(2..)) then return ["ast_eq",n1,n2]; end if; conds := {}; -- condition for inclusion of variable bounds; will be collected. varlist_1 := varlist_2 := genvarlist := iterlimit_list := []; for [itop1,itvar1,itlimit1] = itlist1(j) loop -- work over the two iterator lists in parallel [itop2,itvar2,itlimit2] := itlist2(j); freevars1 := find_free_vars(itlimit1); -- get the free variables in the iterators freevars2 := find_free_vars(itlimit2); subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1}; subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2}; if subst_map1 /= {} then -- replace the indicated variables by their generated forms itlimit1 := substitute(itlimit1,subst_map1); end if; if subst_map2 /= {} then -- replace the indicated variables by their generated forms itlimit2 := substitute(itlimit2,subst_map2); end if; varlist_1 with:= itvar1; -- extend the lists of iterator and generated variables varlist_2 with:= itvar2; genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; if itop1 /= itop2 then if itop1 = "DOT_INCIN" then -- convert to member of powerset itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1]; end if; if itop2 = "DOT_INCIN" then -- convert to member of powerset itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2]; end if; end if; --print("itlimits: ",itlimit1," ",itlimit2); conds with:= monotone_infer_ast_incs(itlimit1,itlimit2); iterlimit_list with:= itlimit1; -- collect the (first) list of iteration limits end loop; -- now demand that the substituted expressions are equal, -- and the second substituted condition implies the first subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j)}; subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j)}; conds with:= monotone_infer_ast_eq(substitute(a2,subst_map1),substitute(b2,subst_map2)); --print("conds::: ",{unparse(cond): cond in conds}); if a4(1) = "ast_null" then a4 := ["TRUE"]; end if; if b4(1) = "ast_null" then b4 := ["TRUE"]; end if; --print("a4: ",a4," ",b4); conds with:= monotone_infer_ast_imp(substitute(b4,subst_map1),substitute(a4,subst_map2)); --print("conds: ",{unparse(cond): cond in conds}); return conjoin_many(conds); when "ast_of" => -- function application mprops_of_args := monotonicity_props(a2); if mprops_of_args = OM then -- demand equality if a2 /= b2 or #(a_list := a3(2..)) /= #(b_list := b3(2..)) then return ["ast_incs",n1,n2]; end if; return disjoin_many({monotone_infer_ast_eq(n1,n2),["ast_incs",n1,n2]}); end if; -- otherwise check the argument lists for identity in positions which are not monotone, but for inclusion in such posns. a_list := a3(2..); b_list := b3(2..); incposns := {j: arg = a_list(j) | mprops_of_args(j) > 0}; decposns := {j: arg = a_list(j) | mprops_of_args(j) < 0}; --print("incposns,decposns: ",incposns," ",decposns); if incposns = {} and decposns = {} then -- arguments must be equal return disjoin_many({monotone_infer_ast_eq(n1,n2),["ast_incs",n1,n2]}); end if; -- but if there are increasing and/or arguments, then collect inclusions and reversed inclusions -- for them, and identities for the others conditions := {if j in incposns then monotone_infer_ast_incs(argj,b_list(j)) elseif j in decposns then monotone_infer_ast_incs(b_list(j),argj) else monotone_infer_ast_eq(argj,b_list(j)) end if: argj = a_list(j)}; return disjoin_many(conditions with ["ast_incs",n1,n2]); otherwise => -- otherwise check the argument lists for identity in positions which are not monotone, but for inclusion in such posns. return disjoin_many({["ast_incs",n1,n2], conjoin_many({monotone_infer_ast_eq(a2,b2),monotone_infer_ast_eq(a3,b3)})}); end case; end if; -- if one of the operators is a conditional then check for evaluability if b1 = "ast_if_expr" then -- interchange and redecompose [n1,n2] := [n2,n1]; [a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2; end if; if a1 = "ast_if_expr" and monotone_infer_ast_equiv(a2,"TRUE") = "TRUE" then -- use first branch return monotone_infer_ast_incs(a3,n2); end if; -- if one of the operators is a union then see if either of its arguments includes the other --print("different lead ops incs: ",[n1,n2]); if a1 = "ast_add" then -- interchange and redecompose to put union operator in the second position [n1,n2] := [n2,n1]; [a1,a2,a3,a4] := n1; [b1,b2,b3] := n2; end if; if b1 = "ast_add" then -- have a union operator in the second position --print("ast_add case incs"); conditions := {["ast_incs",n1,n2],monotone_infer_ast_incs(n1,b2),monotone_infer_ast_incs(n1,b3)}; -- two possible conditions which would force inclusion if a1 = "ast_of" then -- we have a function application; see if there is a position in which the function is additive -- and the corresponding argument is a sum, apply additivity mprops_of_args := monotonicity_props(a2); alist := a3(2..); -- the list of arguments addposns := {j: arg = alist(j) | mprops_of_args(j) = 2}; -- at such argument positions apply additivity for arg = alist(j) | j in addposns and is_tuple(arg) and arg(1) = "ast_add" loop -- loop over all qualifying positions a31 := a3; a31(j + 1) := arg(2); -- transform using additivity: build new arguments a32 := a3; a32(j + 1) := arg(3); newf1 := [a1,a2,a31]; newf2 := [a1,a2,a32]; newsum := ["ast_add",newf1,newf2]; --print("newf1 incs: ",unparse(newsum)); conditions with:= monotone_infer_ast_incs(newsum,n2); -- try this inclusion as an alternative end loop; return disjoin_many(conditions); end if; -- setformers are treated in a special way if their sequences itseq of iterators contain -- a limiting expression which is a union, or if their condition part is a disjunction. -- such positions are treated as 'additive arguments' if a1 = "ast_genset" then conds := {}; -- conditions for inclusion derived from additivity; will be collected. varlist := genvarlist := []; itlist := a3(2..); for [itop,itvar,itlimit] = itlist(j) | itlimit(1) = "ast_add" and itop = "ast_in" loop -- work over the iterator list finding the 'additive' positions [-,itlimit_a,itlimit_b] := itlimit; ilj_a := [itop,itvar,itlimit_a]; ilj_b := [itop,itvar,itlimit_b]; iters_a := a3; iters_a(j + 1) := ilj_a; iters_b := a3; iters_b(j + 1) := ilj_b; setf_a := [a1,a2,iters_a,a4]; setf_b := [a1,a2,iters_b,a4]; newsum := ["ast_add",setf_a,setf_b]; --print("ast_genset incs: ",unparse(newsum)); conds with:= monotone_infer_ast_incs(newsum,n2); -- apply additivity as an alternative end loop; if is_tuple(a4) and a4(1) = "ast_or" then -- condition part of setformer is [-,cond_a,cond_b] := a4; setf_a := [a1,a2,a3,cond_a]; setf_b := [a1,a2,a3,cond_b]; newsum := ["ast_add",setf_a,setf_b]; conds with:= monotone_infer_ast_incs(newsum,n2); -- apply additivity as an alternative end if; return conjoin_many(conds); end if; end if; -- if one of the operators is a union then check the other for additivity and an argument which is a union return ["ast_incs",n1,n2]; end monotone_infer_ast_incs; procedure monotone_infer_ast_eq(n1,n2); -- deduce an equality by monotone inference -- We traverse the two syntax trees downward as long as the lead operators of the nodes encountered -- are identical and none bind any variables. -- When there are different lead operators, we demand equality of the subtrees, -- except in the following cases: -- when there is a + operator in one node n1 but not the other n2, and the nodes have -- one of the following forms: -- (i) f(a1,a2..) and b + c, where the operator f must be additive in at least one of its -- arguments (say the first), which must have the form a11 + a12. In this case, generate the -- disjunction of conjunctions ((f(a11,a2,..) = b) & (f(a12,a2,..) = c)) or vice-versa. -- Note: conjuncts should be tested for 'trivial equality by blobbing', and omitted if this is the case. -- (ii) n1 and n2 are both setformer nodes, of forms like {e(x): x in s | P(x)}. In this case we form the conjunct -- ((s = s') or monotone_infer_ast_eq(s,s')) & (FORALL x in s | e(x) = e'(x)) & (FORALL x in s | P(x) •eq P'(x)), -- again omitting any conjunct which is evident by blobbing. -- (iii) One of the nodes, say the second, has the form b + c, and the other is a setformer of the form -- (a) {e(x): x in s + t | P(x)}, or (b) {e(x): x in s | P(x) or Q(x)} (or both). In these cases we form conjuncts -- Case (a) (({e(x): x in s | P(x)} = b) & ({e(x): x in t | P(x)} = c)) or vice-versa -- Case (b) (({e(x): x in s | P(x)} = b) & ({e(x): x in s | P(x)} = Q(x))) or vice-versa -- If both templates apply, the disjunction of both these sets of clauses should be formed. --print("\nmonotone_infer_ast_eq: ",unparse(n1),"\nn2: ",unparse(n2)); if is_string(n1) or is_string(n2) then return if n1 = n2 then "TRUE" else ["ast_eq",n1,n2] end if; end if; --print("blob_tree([both_,n1,n2]): ",blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]])," ",n1," ",n2); [blob_1,blob_2] := blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]]); -- call special 'common blobbing' function if blob_1 = blob_2 then return "TRUE"; end if; -- check for more general equality directly evident by blobbing --print("not by blobbing"); [a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2; -- otherwise decompose the two trees if a1 = "ast_genset_noexp" then -- convert to form with expression iter_var := a2(2)(2); n1 := [a1,a2,a3,a4] := ["ast_genset",iter_var,a2,a3]; end if; if b1 = "ast_genset_noexp" then -- convert to form with expression iter_var := b2(2)(2); n2 := [b1,b2,b3,b4] := ["ast_genset",iter_var,b2,b3]; end if; if a1 = b1 then case a1 when "ast_if_expr" => -- equality of conditional expressions cond := monotone_infer_ast_equiv(a2,b2); return disjoin_many({["ast_eq",n1,n2], if cond /= "TRUE" then conjoin_many({cond,monotone_infer_ast_eq(a3,b3),monotone_infer_ast_eq(a4,b4)}) else monotone_infer_ast_eq(a3,b3) end if}); when "ast_add","ast_mult" => -- commutative expressions return disjoin_many({["ast_eq",n1,n2], conjoin_many({monotone_infer_ast_eq(a2,b2),monotone_infer_ast_eq(a3,b3)}), conjoin_many({monotone_infer_ast_eq(a2,b3),monotone_infer_ast_eq(a3,b2)})}); when "ast_sub" => -- set difference return disjoin_many({["ast_eq",n1,n2],conjoin_many({monotone_infer_ast_eq(a2,b2),monotone_infer_ast_eq(a3,b3)})}); when "ast_genset" => -- two setformers to be tested for equality -- setformer pairs are treated in a special way if their sequences itseq of iterators are of the same -- length. if (nil1 := #(itlist1 := a3(2..))) /= #(itlist2 := b3(2..)) then return ["ast_eq",n1,n2]; end if; conds := {}; -- condition for equality of variable bounds; will be collected. varlist_1 := varlist_2 := genvarlist := iterlimit_list := []; --print("itlist1(j): ",itlist1(1)); first_genvar := "VRX" + (var_generator + 1) + "_"; for [itop1,itvar1,itlimit1] = itlist1(j) loop -- work over the two iterator lists in parallel [itop2,itvar2,itlimit2] := itlist2(j); freevars1 := find_free_vars(itlimit1); -- get the free variables in the iterators freevars2 := find_free_vars(itlimit2); subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1}; subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2}; if subst_map1 /= {} then -- replace the indicated variables by their generated forms itlimit1 := substitute(itlimit1,subst_map1); end if; if subst_map2 /= {} then -- replace the indicated variables by their generated forms itlimit2 := substitute(itlimit2,subst_map2); end if; varlist_1 with:= itvar1; -- extend the lists of iterator and generated variables varlist_2 with:= itvar2; genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; if itop1 /= itop2 then if itop1 = "DOT_INCIN" then -- convert to member of powerset itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1]; end if; if itop2 = "DOT_INCIN" then -- convert to member of powerset itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2]; end if; end if; conds with:= monotone_infer_ast_eq(itlimit1,itlimit2); iterlimit_list with:= itlimit1; -- collect the (first) list of iteration limits end loop; -- now demand that the substituted expressions are equal, and the substituted conditions are equivalent -- on all the sets subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j)}; subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j)}; --print("conds::: ",{unparse(cond): cond in conds}); if a4(1) = "ast_null" then a4 := "TRUE"; end if; if b4(1) = "ast_null" then b4 := "TRUE"; end if; --print("a4: ",a4," ",b4); if nil1 = 1 then -- if there is just 1 iterator, capture the conditon that the bound variable belongs to the limit set conds with:= ["DOT_IMP",["ast_in",first_genvar,iterlimit_list(1)], monotone_infer_ast_eq(substitute(a2,subst_map1),substitute(b2,subst_map2))]; conds with:= ["DOT_IMP",["ast_in",first_genvar,iterlimit_list(1)], monotone_infer_ast_equiv(substitute(a4,subst_map1),substitute(b4,subst_map2))]; --print("just 1 iterator: "); else conds with:= monotone_infer_ast_eq(substitute(a2,subst_map1),substitute(b2,subst_map2)); conds with:= monotone_infer_ast_equiv(substitute(a4,subst_map1),substitute(b4,subst_map2)); end if; --print("conds: ",{unparse(cond): cond in conds}); -- The iteration bounds which appear in itseq are treated roughly as additive arguments -- if 'In' appears, but as monotone arguments as '•incin' appears. -- for the lead expressions we generate -- for the conditions we generate return conjoin_many(conds); when "ast_pow","ast_nelt" => -- SETL bulitin monadics --print("builtin: ",unparse(n1)," ",unparse(n2)); return disjoin_many({monotone_infer_ast_eq(a2,b2),["ast_eq",n1,n2]}); -- test arguments for equality when "ast_of" => -- "DOT_EQ" if a2 /= b2 or #(a_list := a3(2..)) /= #(b_list := b3(2..)) then return ["ast_eq",n1,n2]; end if; --print("otherwise check: ",a_list," ",b_list," ",conjoin_many({monotone_infer_ast_eq(aj,b_list(j)): aj = a_list(j)})); -- otherwise check the argument lists for identity return disjoin_many({conjoin_many({monotone_infer_ast_eq(aj,b_list(j)): aj = a_list(j)}),["ast_eq",n1,n2]}); otherwise => return ["ast_eq",n1,n2]; end case; end if; -- if one of the operators is a conditional then check for evaluability if b1 = "ast_if_expr" then -- interchange and redecompose [n1,n2] := [n2,n1]; [a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2; end if; if a1 = "ast_genset_noexp" then -- convert to form with expression iter_var := a2(2)(2); n1 := [a1,a2,a3,a4] := ["ast_genset",iter_var,a2,a3]; end if; if b1 = "ast_genset_noexp" then -- convert to form with expression iter_var := b2(2)(2); n2 := [b1,b2,b3,b4] := ["ast_genset",iter_var,b2,b3]; end if; -- see if there is an iterator over an enumerated set and if so reduce if a1 = "ast_genset" and is_tuple(reduced := reduce_enum_iterators(n1)) then return disjoin_many({["ast_eq",n1,n2],monotone_infer_ast_eq(reduced,n2)}); end if; if b1 = "ast_genset" and is_tuple(reduced := reduce_enum_iterators(n2)) then return disjoin_many({["ast_eq",n1,n2],monotone_infer_ast_eq(n1,reduced)}); end if; if a1 = "ast_if_expr" and monotone_infer_ast_equiv(a2,"TRUE") = "TRUE" then -- use first branch return monotone_infer_ast_eq(a3,n2); end if; -- if one of the operators is a union then check the other for additivity and an argument which is a union --print("different lead ops: ",[n1,n2]); if a1 = "ast_add" then -- interchange and redecompose to put union operator in the second position [n1,n2] := [n2,n1]; [b1,b2,b3] := n2; [a1,a2,a3,a4] := n1; end if; if b1 = "ast_add" then -- there is a union operator in the second position --print("ast_add case: ",[a1,a2,a3,a4]); if a1 = "ast_of" then -- we have a function application; -- see if there is a position in which the function is additive, -- and in which a union operator appears as the top argument operator mprops_of_args := monotonicity_props(a2); a_list := a3(2..); addposns := {j: arg = a_list(j) | mprops_of_args(j) = 2 and arg(1) = "ast_add"}; conds := {["ast_eq",n1,n2]}; -- will collect additional possibilities for j in addposns loop [-,arg_first_summand,arg_second_summand] := a_list(j); a3(j + 1) := arg_first_summand; new_n11 := [a1,a2,a3]; a3(j + 1) := arg_second_summand; new_n12 := [a1,a2,a3]; new_n1 := ["ast_add",new_n11,new_n12]; conds with:= monotone_infer_ast_eq(new_n1,n2); end loop; return disjoin_many(conds); -- any of the deduced conditions would force equality end if; if a1 = "ast_genset" then -- we have a setformer -- see if the main operator in any of the iterator limits is an addition. If so, this can be treated as an 'additive argument' -- also, if the main operator in the condition clause is a disjunction, this can be treated as an 'additive argument' conds := {["ast_eq",n1,n2]}; if is_tuple(a4) then -- examine the condition clause [cond_op,cond_1,cond_2] := a4; if cond_op = "ast_or" then -- treat as 'additive argument' setformer_1 := [a1,a2,a3,cond_1]; setformer_2 := [a1,a2,a3,cond_2]; eq1 := monotone_infer_ast_eq(b2,setformer_1); eq2 := monotone_infer_ast_eq(b3,setformer_2); conds with:= conjoin_many({eq1,eq2}); eq1 := monotone_infer_ast_eq(b3,setformer_1); eq2 := monotone_infer_ast_eq(b2,setformer_2); conds with:= conjoin_many({eq1,eq2}); end if; end if; -- now scan over the iterators, looking for all those in which the operator is 'in' and the topmost operator is '+' -- any of these can be treated as an 'additive argument' itlist := a3(2..); -- the list of iterators varlist := genvarlist := iterlimit_list := []; for [itop,itvar,itlimit] = itlist(j) loop -- work over the iterator list --print("add-iter case: ",itop," ",itlimit); if itop = "ast_in" and itlimit(1) = "ast_add" then new_iter_1 := a3; new_iter_1(j + 1) := ["in",itvar,itlimit(2)]; new_iter_2 := a3; new_iter_2(j + 1) := ["in",itvar,itlimit(3)]; new_setf_1 := ["ast_genset",a2,new_iter_1,a4]; new_setf_2 := ["ast_genset",a2,new_iter_2,a4]; --print("new_setf_1: ",unparse(new_setf_1)," ",unparse(b2)); eq1 := monotone_infer_ast_eq(b2,new_setf_1); eq2 := monotone_infer_ast_eq(b3,new_setf_2); conds with:= conjoin_many({eq1,eq2}); eq1 := monotone_infer_ast_eq(b3,new_setf_1); eq2 := monotone_infer_ast_eq(b2,new_setf_2); conds with:= conjoin_many({eq1,eq2}); end if; end loop; --print("collected conds: ",{unparse(cond): cond in conds}); return disjoin_many(conds); end if; return ["ast_eq",n1,n2]; end if; -- next we treat setformer and expressionless setformers,, -- which are converted to standard setformers {e: iter | cond} -- these are treated by first finding as many lead parts of 'iter' -- as are independent of the parts of 'iter' that come before. -- The iteration bounds which appear in se are treated roughly as additive arguments -- if 'In' appears, but as monotone arguments as '•incin' appears. -- for the lead expressions we generate -- for the conditions we generate return ["ast_eq",n1,n2]; -- temporary end monotone_infer_ast_eq; procedure disjoin_many(set_of_clauses); -- construct a 'lazy' disjunction collected_disjunction_set := {} +/ {lazy_disj(2): lazy_disj in set_of_clauses | lazy_disj(1) = "disjoined"}; collected_conjunction_set := {conjoin_really(lazy_conj(2)): lazy_conj in set_of_clauses | lazy_conj(1) = "conjoined"}; collected_raw_set := {raw: raw in set_of_clauses | raw(1) /= "disjoined" and raw(1) /= "conjoined"}; return ["disjoined",collected_disjunction_set + collected_conjunction_set + collected_raw_set]; end disjoin_many; procedure conjoin_many(set_of_clauses); -- construct a 'lazy' conjunction collected_conjunction_set := {} +/ {lazy_disj(2): lazy_disj in set_of_clauses | lazy_disj(1) = "conjoined"}; collected_disjunction_set := {disjoin_really(lazy_conj(2)): lazy_conj in set_of_clauses | lazy_conj(1) = "disjoined"}; collected_raw_set := {raw: raw in set_of_clauses | raw(1) /= "disjoined" and raw(1) /= "conjoined"}; return ["conjoined",collected_disjunction_set + collected_conjunction_set + collected_raw_set]; end conjoin_many; procedure disjoin_really(set_of_clauses); -- construct a disjunction --print("disjoin_really: ",set_of_clauses); if (clause from set_of_clauses) = "TRUE" then return "TRUE"; end if; for subclause in set_of_clauses loop if subclause = "TRUE" then return "TRUE"; end if; clause := ["ast_or",clause,subclause]; end loop; return clause; end disjoin_really; procedure conjoin_really(set_of_clauses); -- construct a conjunction --print("conjoin_really: ",set_of_clauses); clause := []; for subclause in set_of_clauses | subclause /= "TRUE" loop if clause = [] then clause := subclause; continue; end if; clause := ["ast_and",clause,subclause]; end loop; return if clause = [] then "TRUE" else clause end if; end conjoin_really; procedure monotone_infer_ast_equiv(n1,n2); -- deduce an equivalence by monotone inference -- We traverse the two syntax trees downward as long as the lead operators of the nodes encountered -- are identical and none bind any variables. -- When there are different lead operators, demand equality of the subtrees, -- except in the following cases: -- when there is an or operator in one node n1 but not the other n2, and the nodes have -- one of the following forms: -- (iii) One of the nodes, say the second, has the form 'b or c', and the other is an existential quantifier of the form -- (a) (EXISTS x in s + t | P(x)), or (b) (EXISTS x in s | P(x) or Q(x)) (or both). In thes cases we form conjuncts -- Case (a) (EXISTS x in s | P(x)) •eq b) & (EXISTS x in t | P(x)) •eq c)) or vice-versa -- Case (b) (EXISTS x in s | P(x)) •eq & (EXISTS x in s | Q(x)) •eq c)) or vice-versa -- If both templates apply, the disjunction of both these sets of clauses should be formed. --print("monotone_infer_ast_equiv: ",n1,"\nn2: ",n2); if is_string(n1) or is_string(n2) then return if n1 = n2 then "TRUE" else ["DOT_EQ",n1,n2] end if; end if; [blob_1,blob_2] := blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]]); -- call special 'common blobbing' function if blob_1 = blob_2 then return "TRUE"; end if; -- check for more general equality directly evident by blobbing [a1,a2,a3,a4] := n1; [b1,b2,b3,a4] := n2; -- otherwise decompose the two trees if a1 = b1 then --print("equal ops in equiv"); case a1 when "ast_if_expr" => -- equality of conditional expressions cond := monotone_infer_ast_equiv(a2,b2); return disjoin_many({["DOT_EQ",n1,n2], conjoin_many({monotone_infer_ast_equiv(a2,b2),monotone_infer_ast_eq(a3,b3),monotone_infer_ast_eq(a4,b4)})}); when "ast_or","ast_and" => -- commutative expressions return disjoin_many({["DOT_EQ",n1,n2], conjoin_many({monotone_infer_ast_eq(a2,b2),monotone_infer_ast_eq(a3,b3)}), conjoin_many({monotone_infer_ast_equiv(a2,b3),monotone_infer_ast_equiv(a3,b2)})}); when "ast_forall", "ast_exists" => -- two quantifiers to be tested for equality -- quantifier pairs are treated in a special way if their sequences itseq of iterators are of the same -- length. if #(itlist1 := a2(2..)) /= #(itlist2 := b2(2..)) then return ["DOT_EQ",n1,n2]; end if; conds := {}; -- condition for equality of variable bounds; will be collected. varlist_1 := varlist_2 := genvarlist := iterlimit_list := []; for [itop1,itvar1,itlimit1] = itlist1(j) loop -- work over the two iterator lists in parallel [itop2,itvar2,itlimit2] := itlist2(j); freevars1 := find_free_vars(itlimit1); -- get the free variables in the iterators freevars2 := find_free_vars(itlimit2); subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1}; subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2}; if subst_map1 /= {} then -- replace the indicated variables by their generated forms itlimit1 := substitute(itlimit1,subst_map1); end if; if subst_map2 /= {} then -- replace the indicated variables by their generated forms itlimit2 := substitute(itlimit2,subst_map2); end if; varlist_1 with:= itvar1; -- extend the lists of iterator and generated variables varlist_2 with:= itvar2; genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; if itop1 /= itop2 then if itop1 = "DOT_INCIN" then -- convert to member of powerset itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1]; end if; if itop2 = "DOT_INCIN" then -- convert to member of powerset itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2]; end if; end if; conds with:= monotone_infer_ast_eq(itlimit1,itlimit2); iterlimit_list with:= itlimit1; -- collect the (first) list of iteration limits end loop; -- now demand that the substituted conditions are equivalent conds with:= monotone_infer_ast_equiv(substitute(a3,subst_map1),substitute(b3,subst_map2)); --print("conds: ",{unparse(cond): cond in conds}); return conjoin_many(conds); when "ast_not" => -- SETL bulitin monadic return disjoin_many({monotone_infer_ast_equiv(a2,b2),["DOT_EQ",n1,n2]}); -- test arguments for equality when "ast_of" => -- function application if a2 /= b2 or #(a_list := a3(2..)) /= #(b_list := b3(2..)) then return ["DOT_EQ",n1,n2]; end if; --print("otherwise check: ",a_list," ",b_list," ",conjoin_many({monotone_infer_ast_eq(aj,b_list(j)): aj = a_list(j)})); -- otherwise check the argument lists for identity return disjoin_many({conjoin_many({monotone_infer_ast_eq(aj,b_list(j)): aj = a_list(j)}),["DOT_EQ",n1,n2]}); otherwise => return disjoin_many({["DOT_EQ",n1,n2], conjoin_many({monotone_infer_ast_equiv(a2,b2),monotone_infer_ast_equiv(a3,b3)})}); end case; end if; -- if one of the operators is a conditional then check for evaluability if a1 = "ast_if_expr" and monotone_infer_ast_equiv(a2,"TRUE") = "TRUE" then -- use first branch return monotone_infer_ast_eq(a3,n2); end if; -- if one of the operators is a disjunction then check the other for additivity and an argument which is a union --print("different lead ops in equiv: ",[n1,n2]); if a1 = "ast_or" or a1 = "ast_and" then -- interchange and redecompose to put con/disjunction operator in the second position [n1,n2] := [n2,n1]; [b1,b2,b3] := n2; [a1,a2,a3] := n1; end if; if b1 = "ast_or" then -- there is a union operator in the second position if a1 = "ast_exists" then -- we have an existential --print("ast_or_exists case in equiv: ",[a1,a2,a3]); -- see if the main operator in any of the iterator limits is an addition. If so, this can be treated as an 'additive argument' -- also, if the main operator in the condition clause is a disjunction, this can be treated as an 'additive argument' conds := {["DOT_EQ",n1,n2]}; if is_tuple(a3) then -- examine the condition clause [cond_op,cond_1,cond_2] := a3; if cond_op = "ast_or" then -- treat as 'additive argument' --print("additive in equiv: ",[a1,a2,a3]); exis_1 := [a1,a2,cond_1]; exis_2 := [a1,a2,cond_2]; eq1 := monotone_infer_ast_equiv(b2,exis_1); eq2 := monotone_infer_ast_equiv(b3,exis_2); conds with:= conjoin_many({eq1,eq2}); eq1 := monotone_infer_ast_equiv(b3,exis_1); eq2 := monotone_infer_ast_equiv(b2,exis_2); conds with:= conjoin_many({eq1,eq2}); end if; end if; -- now scan over the iterators, looking for all those in which the operator is 'in' and the topmost operator is '+' -- any of these can be treated as an 'additive argument' itlist := a2(2..); -- the list of iterators varlist := genvarlist := iterlimit_list := []; for [itop,itvar,itlimit] = itlist(j) loop -- work over two iterator list --print("add-iter case in equiv: ",itop," ",itlimit); if itop = "ast_in" and itlimit(1) = "ast_add" then new_iter_1 := a2; new_iter_1(j + 1) := ["in",itvar,itlimit(2)]; new_iter_2 := a2; new_iter_2(j + 1) := ["in",itvar,itlimit(3)]; new_exi_1 := ["ast_exists",new_iter_1,a3]; new_exi_2 := ["ast_exists",new_iter_2,a3]; eq1 := monotone_infer_ast_equiv(b2,new_exi_1); eq2 := monotone_infer_ast_equiv(b3,new_exi_2); conds with:= conjoin_many({eq1,eq2}); eq1 := monotone_infer_ast_equiv(b3,new_exi_1); eq2 := monotone_infer_ast_equiv(b2,new_exi_2); conds with:= conjoin_many({eq1,eq2}); end if; end loop; --print("collected conds: ",{unparse(cond): cond in conds}); return disjoin_many(conds); end if; end if; if b1 = "ast_and" then -- there is a conjunction operator in the second position if a1 = "ast_forall" then -- we have a universal --print("ast_or_exists case in equiv: ",[a1,a2,a3]); -- see if the main operator in any of the iterator limits is an addition. If so, this can be treated as an 'additive argument' -- also, if the main operator in the condition clause is a disjunction, this can be treated as an 'additive argument' conds := {["DOT_EQ",n1,n2]}; if is_tuple(a3) then -- examine the condition clause [cond_op,cond_1,cond_2] := a3; if cond_op = "ast_and" then -- treat as 'conjunctive argument' --print("conjunctive in equiv: ",[a1,a2,a3]); univ_1 := [a1,a2,cond_1]; univ_2 := [a1,a2,cond_2]; eq1 := monotone_infer_ast_equiv(b2,univ_1); eq2 := monotone_infer_ast_equiv(b3,univ_2); conds with:= conjoin_many({eq1,eq2}); eq1 := monotone_infer_ast_equiv(b3,univ_1); eq2 := monotone_infer_ast_equiv(b2,univ_2); conds with:= conjoin_many({eq1,eq2}); end if; end if; -- now scan over the iterators, looking for all those in which the operator is 'in' and the topmost operator is '+' -- any of these can be treated as an 'additive argument' itlist := a2(2..); -- the list of iterators varlist := genvarlist := iterlimit_list := []; for [itop,itvar,itlimit] = itlist(j) loop -- work over two iterator list --print("add-iter case in equiv: ",itop," ",itlimit); if itop = "ast_in" and itlimit(1) = "ast_add" then new_iter_1 := a2; new_iter_1(j + 1) := ["in",itvar,itlimit(2)]; new_iter_2 := a2; new_iter_2(j + 1) := ["in",itvar,itlimit(3)]; new_exi_1 := ["ast_forall",new_iter_1,a3]; new_exi_2 := ["ast_forall",new_iter_2,a3]; eq1 := monotone_infer_ast_equiv(b2,new_exi_1); eq2 := monotone_infer_ast_equiv(b3,new_exi_2); conds with:= conjoin_many({eq1,eq2}); eq1 := monotone_infer_ast_equiv(b3,new_exi_1); eq2 := monotone_infer_ast_equiv(b2,new_exi_2); conds with:= conjoin_many({eq1,eq2}); end if; end loop; --print("collected conds: ",{unparse(cond): cond in conds}); return disjoin_many(conds); end if; return ["DOT_EQ",n1,n2]; -- if nothing special can be done end if; return ["DOT_EQ",n1,n2]; end monotone_infer_ast_equiv; procedure reduce_enum_iterators(node); -- look for iterators over enumerated sets in a setformer or quantifier, -- and if found then replace by assignments of variable -- if not found then return OM return OM; -- *********** REMOVE if node(1) = "ast_genset" then [a1,a0,a2,a3] := node; else -- must be quantifier [a1,a2,a3] := node; end if; iter_list := a2(2..); if not(exists iter in iter_list | iter(1) = "ast_in" and (itlim := iter(3))(1) = "ast_enum_set") then return OM; end if; case a1 when "ast_genset" => print("reduce_enum_iterators: ",iter_list); -- reduce to union when "ast_exists" => print("reduce_enum_iterators: ",iter_list); -- reduce to disjunction when "ast_forall" => print("reduce_enum_iterators: ",iter_list); -- reduce to conjunction end case; end reduce_enum_iterators; procedure monotone_infer_ast_imp(n1,n2); -- deduce an implication by monotone inference -- We traverse the two syntax trees downward as long as the lead operators of the nodes encountered -- are identical and none bind any variables. -- When there are different lead operators, we forego processing, except a few two quantifier-related cases: -- except in the following cases: -- (i) (FORALL x in s * t | ..) •imp (b & c) might be the conjunct (FORALL x in s | ..) •imp b) & (FORALL x in t | ..) •imp t) -- (ii) (FORALL x in s | P & Q) •imp (b & c) might be the conjunct (FORALL x in s | P) •imp b) & (FORALL x in s | Q) •imp t) -- (iii) (b or c) •imp (EXISTS x in s + t | ..) might be the disjunct (b •imp (EXISTS x in s | ..)) or (c •imp (EXISTS x in t | ..)) -- (iv) (b or c) •imp (EXISTS x in s | P or Q) might be the disjunct (b •imp (EXISTS x in s | P)) or (c •imp (EXISTS x in s | Q)) -- If both templates apply, the disjunction of both these sets of clauses should be formed. --print("monotone_infer_ast_imp: ",unparse(n1)," ",unparse(n2)); if is_string(n1) and is_string(n2) then return if n1 = n2 then "TRUE" else ["DOT_IMP",n1,n2] end if; end if; [blob_1,blob_2] := blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]]); -- call special 'common blobbing' function if blob_1 = blob_2 then return "TRUE"; end if; -- check for more general equality evident by blobbing if n2 = "TRUE" then return "TRUE"; end if; -- this case will be common since generated by other monot-inference routines [a1,a2,a3,a4] := n1; if is_string(n2) then if a1 = "ast_or" then return disjoin_many({["DOT_IMP",n1,n2],conjoin_many({monotone_infer_ast_imp(a2,n2),monotone_infer_ast_imp(a3,n2)})}); elseif a1 = "ast_and" then return disjoin_many({["DOT_IMP",n1,n2],monotone_infer_ast_imp(a2,n2),monotone_infer_ast_imp(a3,n2)}); elseif a1 = "ast_if_expr" and monotone_infer(a2) = "TRUE" then return disjoin_many({["DOT_IMP",n1,n2],monotone_infer_ast_imp(a3,n2)}); else return ["DOT_IMP",n1,n2]; end if; end if; [b1,b2,b3,b4] := n2; -- otherwise decompose the two trees if a1 = b1 then -- identical lead operators case a1 --print("monotone_infer_ast_imp same: ",unparse(n1)," ",unparse(n2)); when "ast_if_expr" => -- implication of conditional expressions cond := monotone_infer_ast_equiv(a2,b2); return disjoin_many({["DOT_IMP",n1,n2], if cond /= "TRUE" then conjoin_many({cond,monotone_infer_ast_imp(a3,b3),monotone_infer_ast_imp(b4,a4)}) else monotone_infer_ast_imp(a3,b3) end if}); when "ast_or","ast_and" => -- commutative expressions return disjoin_many({["ast_incs",n1,n2], conjoin_many({monotone_infer_ast_imp(a2,b2),monotone_infer_ast_imp(a3,b3)}), conjoin_many({monotone_infer_ast_imp(a2,b3),monotone_infer_ast_imp(a3,b2)})}); when "ast_not" => -- two inverse implications return monotone_infer_ast_imp(b2,a2); when "ast_forall" => -- universals -- pairs of universals are treated in a special way if their sequences itseq of iterators are of the same length. if #(itlist1 := a2(2..)) /= #(itlist2 := b2(2..)) then return ["DOT_IMP",n1,n2]; end if; conds := {}; -- condition for inclusion of variable bounds; will be collected. varlist_1 := varlist_2 := genvarlist := iterlimit_list := []; --print("universals: ",itlist1," ",itlist2); for [itop1,itvar1,itlimit1] = itlist1(j) loop -- work over the two iterator lists in parallel [itop2,itvar2,itlimit2] := itlist2(j); freevars1 := find_free_vars(itlimit1); -- get the free variables in the iterators freevars2 := find_free_vars(itlimit2); subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1}; subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2}; if subst_map1 /= {} then -- replace the indicated variables by their generated forms itlimit1 := substitute(itlimit1,subst_map1); end if; if subst_map2 /= {} then -- replace the indicated variables by their generated forms itlimit2 := substitute(itlimit2,subst_map2); end if; varlist_1 with:= itvar1; -- extend the lists of iterator and generated variables varlist_2 with:= itvar2; genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; if itop1 /= itop2 then -- convert inclusion to powerset membership if itop1 = "DOT_INCIN" then -- convert to member of powerset itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1]; end if; if itop2 = "DOT_INCIN" then -- convert to member of powerset itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2]; end if; end if; conds with:= monotone_infer_ast_incs(itlimit1,itlimit2); -- hypothesis must iterlimit_list with:= itlimit1; -- collect the (first) list of iteration limits end loop; freevars1 := find_free_vars(a3); -- get the free variables in the iterators freevars2 := find_free_vars(b3); subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1}; subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2}; if subst_map1 /= {} then -- replace the indicated variables by their generated forms a3 := substitute(a3,subst_map1); end if; if subst_map2 /= {} then -- replace the indicated variables by their generated forms b3 := substitute(b3,subst_map2); end if; conds with:= monotone_infer_ast_imp(substitute(a3,subst_map1),substitute(b3,subst_map2)); -- demand that the condition in the first existential imply that in the second return disjoin_many({conjoin_many(conds),["DOT_IMP",n1,n2]}); when "ast_exists" => -- existentials -- pairs of existentials are treated in a special way if their sequences itseq of iterators are of the same length. if #(itlist1 := a2(2..)) /= #(itlist2 := b2(2..)) then return ["DOT_IMP",n1,n2]; end if; conds := {}; -- condition for inclusion of variable bounds; will be collected. varlist_1 := varlist_2 := genvarlist := iterlimit_list := []; --print("existentials: ",itlist1," ",itlist2); for [itop1,itvar1,itlimit1] = itlist1(j) loop -- work over the two iterator lists in parallel [itop2,itvar2,itlimit2] := itlist2(j); freevars1 := find_free_vars(itlimit1); -- get the free variables in the iterators freevars2 := find_free_vars(itlimit2); subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1}; subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2}; if subst_map1 /= {} then -- replace the indicated variables by their generated forms itlimit1 := substitute(itlimit1,subst_map1); end if; if subst_map2 /= {} then -- replace the indicated variables by their generated forms itlimit2 := substitute(itlimit2,subst_map2); end if; varlist_1 with:= itvar1; -- extend the lists of iterator and generated variables varlist_2 with:= itvar2; genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; if itop1 /= itop2 then -- convert inclusion to powerset membership if itop1 = "DOT_INCIN" then -- convert to member of powerset itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1]; end if; if itop2 = "DOT_INCIN" then -- convert to member of powerset itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2]; end if; end if; conds with:= monotone_infer_ast_incs(itlimit2,itlimit1); -- demand that limit from second existential include that from first iterlimit_list with:= itlimit1; -- collect the (first) list of iteration limits end loop; freevars1 := find_free_vars(a3); -- get the free variables in the iterators freevars2 := find_free_vars(b3); subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1}; subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2}; if subst_map1 /= {} then -- replace the indicated variables by their generated forms a3 := substitute(a3,subst_map1); end if; if subst_map2 /= {} then -- replace the indicated variables by their generated forms b3 := substitute(b3,subst_map2); end if; conds with:= monotone_infer_ast_imp(substitute(a3,subst_map1),substitute(b3,subst_map2)); -- demand that the condition in the first existential imply that in the second --print("conds: ",{unparse(cond): cond in conds}); return disjoin_many({conjoin_many(conds),["DOT_IMP",n1,n2]}); when "ast_of" => -- function application; equality is an alternative mprops_of_args := monotonicity_props(a2); if mprops_of_args = OM then -- demand equality if a2 /= b2 or #(a_list := a3(2..)) /= #(b_list := b3(2..)) then return ["ast_incs",n1,n2]; end if; return disjoin_many({monotone_infer_ast_eq(n1,n2),["ast_incs",n1,n2]}); end if; -- otherwise check the argument lists for identity in positions which are not monotone, but for inclusion in such posns. a_list := a3(2..); b_list := b3(2..); incposns := {j: arg = a_list(j) | mprops_of_args(j) > 0}; decposns := {j: arg = a_list(j) | mprops_of_args(j) < 0}; if incposns = {} and decposns = {} then -- arguments must be equal return disjoin_many({monotone_infer_ast_eq(n1,n2),["ast_incs",n1,n2]}); end if; --print("ast_of_imp: ",mprops_of_args," ",decposns); -- but if there are increasing and/or arguments. then collect inclusions and reversed inclusions -- for them, and identities for the others conditions := {if j in incposns then monotone_infer_ast_incs(b_list(j),argj) elseif j in decposns then monotone_infer_ast_incs(argj,b_list(j)) else monotone_infer_ast_eq(argj,b_list(j)) end if: argj = a_list(j)}; return disjoin_many(conditions with ["ast_imp",n1,n2]); otherwise => -- otherwise nothing to do return ["DOT_IMP",n1,n2]; end case; end if; --print("different ops imp: ",n1," ",n2); -- if one of the operators is a conditional then check for evaluability if b1 = "ast_if_expr" then -- interchange and redecompose [n1,n2] := [n2,n1]; [a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2; end if; if a1 = "ast_if_expr" and monotone_infer_ast_equiv(a2,"TRUE") = "TRUE" then -- use first branch print("ast_if_expr imp"); return monotone_infer_ast_imp(a3,n2); end if; if b1 = "ast_or" then -- have a disjunction operator in the second position conds := {["DOT_IMP",n1,n2],monotone_infer_ast_imp(n1,b2),monotone_infer_ast_imp(n1,b3)}; -- two possible conditions which would force implication -- existentials are treated in a special way if their sequences itseq of iterators contain -- a limiting expression which is a union, or if their condition part is a disjunction. -- such positions are treated as 'additive arguments' if a1 = "ast_exists" then -- transform using additivity and make recursive call to case of equal operators itlist := a2(2..); -- get list of iterators for [itop,itvar,itlimit] = itlist(j) | itop = "ast_in" and itlimit(1) = "ast_add" loop a21 := a2; a21(j + 1) := [itop,itvar,itlimit(2)]; -- transform using additivity: build new arguments a22 := a2; a22(j + 1) := [itop,itvar,itlimit(3)]; newq1 := [a1,a21,a3]; newq2 := [a1,a22,a3]; newdis := ["ast_or",newq1,newq2]; conds with:= monotone_infer_ast_imp(newdis,n2); -- apply additivity as an alternative end loop; if a3(1) = "ast_or" then -- the first condition is a disjunction newq1 := [a1,a2,a3(2)]; newq2 := [a1,a2,a3(3)]; newdis := ["ast_or",newq1,newq2]; conds with:= monotone_infer_ast_imp(newdis,n2); -- apply additivity as an alternative end if; end if; return disjoin_many(conds); -- any of the accumulated conditions would force implication end if; if a1 = "ast_or" then -- have a disjunction operator in the first position conds := {["DOT_IMP",n1,n2],conjoin_many({monotone_infer_ast_imp(a2,n2),monotone_infer_ast_imp(a3,n2)})}; -- two conditions which would force implication -- existentials are treated in a special way if their sequences itseq of iterators contain -- a limiting expression which is a union, or if their condition part is a disjunction. -- such positions are treated as 'additive arguments' if b1 = "ast_exists" then -- transform using additivity and make recursive call to case of equal operators itlist := b2(2..); -- get list of iterators for [itop,itvar,itlimit] = itlist(j) | itop = "ast_in" and itlimit(1) = "ast_add" loop b21 := b2; b21(j + 1) := [itop,itvar,itlimit(2)]; -- transform using additivity: build new arguments b22 := b2; b22(j + 1) := [itop,itvar,itlimit(3)]; newq1 := [b1,b21,b3]; newq2 := [b1,b22,b3]; newdis := ["ast_or",newq1,newq2]; conds with:= monotone_infer_ast_imp(n1,newdis); -- apply additivity as an alternative end loop; if b3(1) = "ast_or" then -- the first condition is a disjunction newq1 := [b1,b2,b3(2)]; newq2 := [b1,b2,b3(3)]; newdis := ["ast_or",newq1,newq2]; conds with:= monotone_infer_ast_imp(n1,newdis); -- apply additivity as an alternative end if; end if; return disjoin_many(conds); -- any of the accumulated conditions would force implication end if; if b1 = "ast_and" then -- have a disjunction operator in the second position conds := {["DOT_IMP",n1,n2],conjoin_many({monotone_infer_ast_imp(n1,b2),monotone_infer_ast_imp(n1,b3)})}; -- two possible conditions whose conjunction would force implication -- universals are treated in a special way if their sequences itseq of iterators contain -- a limiting expression which is a union, or if their condition part is a conjunction. -- such positions are treated as 'additive arguments' if a1 = "ast_forall" then -- transform using additivity and make recursive call to case of equal operators itlist := a2(2..); -- get list of iterators for [itop,itvar,itlimit] = itlist(j) | itop = "ast_in" and itlimit(1) = "ast_add" loop a21 := a2; a21(j + 1) := [itop,itvar,itlimit(2)]; -- transform using additivity: build new arguments a22 := a2; a22(j + 1) := [itop,itvar,itlimit(3)]; newq1 := [a1,a21,a3]; newq2 := [a1,a22,a3]; newdis := ["ast_and",newq1,newq2]; conds with:= monotone_infer_ast_imp(newdis,n2); -- apply additivity as an alternative end loop; if a3(1) = "ast_and" then -- the first condition is a disjunction newq1 := [a1,a2,a3(2)]; newq2 := [a1,a2,a3(3)]; newcon := ["ast_and",newq1,newq2]; conds with:= monotone_infer_ast_imp(newcon,n2); -- apply conjunction as an alternative end if; end if; return disjoin_many(conds); -- any of the accumulated conditions would force implication end if; if a1 = "ast_and" then -- have a conjunction operator in the first position conds := {["DOT_IMP",n1,n2],monotone_infer_ast_imp(a2,n2),monotone_infer_ast_imp(a3,n2)}; -- two conditions either of which would force implication -- universals are treated in a special way if their sequences itseq of iterators contain -- a limiting expression which is a union, or if their condition part is a conjunction. -- such positions are treated as 'additive arguments' if b1 = "ast_forall" then -- transform using additivity and make recursive call to case of equal operators itlist := b2(2..); -- get list of iterators for [itop,itvar,itlimit] = itlist(j) | itop = "ast_in" and itlimit(1) = "ast_add" loop b21 := b2; b21(j + 1) := [itop,itvar,itlimit(2)]; -- transform using additivity: build new arguments b22 := b2; b22(j + 1) := [itop,itvar,itlimit(3)]; newq1 := [b1,b21,b3]; newq2 := [b1,b22,b3]; newcon := ["ast_and",newq1,newq2]; conds with:= monotone_infer_ast_imp(n1,newcon); -- apply additivity as an alternative end loop; if b3(1) = "ast_and" then -- the first condition is a disjunction newq1 := [b1,b2,b3(2)]; newq2 := [b1,b2,b3(3)]; newcon := ["ast_and",newq1,newq2]; conds with:= monotone_infer_ast_imp(n1,newcon); -- apply conjunction as an alternative end if; end if; return disjoin_many(conds); -- any of the accumulated conditions would force implication end if; return ["DOT_IMP",n1,n2]; end monotone_infer_ast_imp; procedure post_monotone(op_and_arg_string); -- note the monotonicity property of one or more function symbols -- this adds information concerning the monotonicity properties of an operator to the map 'monotonicity_props' -- for use by 'blob_to_monotone'. The parameter is a string of the form op_name,dep_1,...,dep_n, -- where each dep is either '+' (increasing), '++' (additive), '-' (decreasing), '0' (mixed) -- these are stored in the map as 1,2,-1,0 respectively. Multiple semicolon-separated declarations of this kind can be supplied op_and_arg_tups := breakup(breakup(op_and_arg_string,";"),","); for op_and_arg_tup in op_and_arg_tups loop op := case_change(op_and_arg_tup(1),"lu"); arg_qual := [if x = "+" then 1 elseif x = "++" then 2 elseif x = "--" then -2 elseif x = "-" then -1 else 0 end if: x in op_and_arg_tup(2..)]; monotonicity_props(op) := arg_qual; end loop; print("monotonicity_props: ",monotonicity_props); end post_monotone; -- **************************************************** -- *************** Algebraic inference **************** -- **************************************************** procedure find_algebraic_nodes(tree); -- finds the algebraic nodes in a tree, and returns them -- as a map from the '+' operator defining an algebraic operator set var algebraic_nodes := {}; -- the value of this global is a map; see comment above. -- an algebraic node is one which is tagged by an algebraic operator belonging to some -- algebraic operator set, but whose parent is either not algebraic or does not belong to -- the same algebraic operator set. find_algebraic_nodes_in(tree,OM); -- call the recursive workhorse return algebraic_nodes; -- return the map produced procedure find_algebraic_nodes_in(tree,plus_op_of_parent); -- internal recursive workhorse --print("find_algebraic_nodes_in: ",plus_op_of_parent," ",unicode_unparse(tree)); if is_string(tree) then return; end if; -- since this is not an algebraic expression if abbreviated_headers(tree(1)) in {"{}","{/}","EX","ALL"} then return; end if; -- we do not search below levels at which bound variables appear op := if (n1 := tree(1)) = "ast_of" then tree(2) else n1 end if; -- get the operator (infix, prefix, or fcn) args := if n1 = "ast_of" then tree(3)(2..) else tree(2..) end if; -- get its arguments if (ao := alg_of(op)) /= OM and ao /= plus_op_of_parent then -- this is an algebraic node, so associate it with its plus_op algebraic_nodes(ao) := (algebraic_nodes(ao)?{}) with tree; end if; -- in any case, continue search down the tree, passing the algebraic type of the new parent for arg in args loop find_algebraic_nodes_in(arg,ao); end loop; end find_algebraic_nodes_in; end find_algebraic_nodes; -- Once having found all algebraic nodes in a tree we standardize them, and for each generate an -- equality which states that the algebraic node is equal to its standardized form --procedure algebraic_identities(tree); -- generate algebraic identities from algebraic nodes -- var all_identities := []; -- will generate and return all algebraic identities from algebraic nodes -- algebraic_nodes := find_algebraic_nodes(tree); -- find the algebraic nodes -- for [-,subtree_set] in algebraic_nodes, subtree in subtree_set loop -- all_identities with:= generate_algebraic_identity(subtree); -- standardize the algebraic top of the tree and convert it into an identity -- end loop; -- return all_identities; -- return the generated list of algebraic identities --end algebraic_identities; procedure generate_algebraic_identity(tree); -- calculates the standard form of an algebraic tree and equates the original form with this --print("generate_algebraic_identity: ",unparse(tree),"\n",unparse(canorder_subtree(tree))); return ["ast_eq",tree,canorder_subtree(tree)]; -- simply returns the equality generated by canorder_subtree end generate_algebraic_identity; procedure canorder_subtree(tree); -- sorts the terms and factors of a standardized (flattened) subtree and performs cancellations if is_string(tree) then return tree; end if; -- nothing to do if tree is just a variable or constant plus_op := alg_of(topkind := if (tk := tree(1)) = "ast_of" then tree(2) else tk end if); -- get the topmost node and the corresponding addition operator, or the function sign if the top opearator is a function application -- sort the terms and factors ofthe standardized subtree and performs cancellation; then return the re-nested result flattened_tree := re_nest(order_and_cancel(st := standardize_subtree(tree,plus_op),plus_op)); flattened_tree := re_nest(order_and_cancel(standardize_subtree(flattened_tree,plus_op),plus_op)); -- put the tree into standardized form; re-nest to allow for identical associative operators in sequence -- repeat twice to get simplifications 2 levels deep -- the topmost node can be a reversal, difference, sum, or product -- res := re_nest(order_and_cancel(flattened_tree,plus_op)); return flattened_tree; end canorder_subtree; procedure order_and_cancel(tree,plus_op); -- debugging wrapper res := oorder_and_cancel(tree,plus_op); -- print("order_and_cancel:::: ",tree,"\n",unparse(re_nest(tree))," returns: ",unparse(re_nest(res))); return res; end order_and_cancel; procedure oorder_and_cancel(tree,plus_op); -- sorts the terms and factors of a standardized (flattened) subtree and performs cancellations (workhorse) --if debug_flag then print("order_and_cancel: ",tree," ",plus_op); end if; -- if the topmost operation in the tree is not algebraic, simply return it unchanged. -- the 'ast_of' case is needed to hanldle unary minus ops, which are written as Rev(x). -- 'kind' is set to the topmos algebraic opearator of the teree, if it is algebraic if is_string(tree) or alg_of(kind := if (tk := tree(1)) = "ast_of" then tree(2) else tk end if) /= plus_op then return tree; end if; case alg_role_of(kind) -- handle the varrious kinds of algebraic operations separately -- monadic minus: process the argument recursively, and re-integrate into a monadic minus when "--" => provisional_result := ["ast_of",tree(2),["ast_list",sarg := order_and_cancel(tree(3)(2),plus_op)]]; -- if the simplified argument of the monadic minus is now zero, return 0. Othersie return the constucted tree return if sarg = zero_from_addn(plus_op) then sarg else provisional_result end if; when "-" => -- subtraction; sort the positive and negative parts, and then cancel [sub_op,pos_part,neg_part] := tree; -- get the two arguments of the subtraction -- get the lead operators of the positive and negative parts, allowing for monadic minuses pos_tk := if is_string(pos_part) or (pos_tk := pos_part(1)) = "ast_of" then OM else pos_tk end if; neg_tk := if is_string(neg_part) or (neg_tk := neg_part(1)) = "ast_of" then OM else neg_tk end if; pos_reord := order_and_cancel(pos_part,plus_op); -- process the first argument recursively neg_reord := order_and_cancel(neg_part,plus_op); -- process the second argument recursively -- if at least one of these is a flattened sum, cancellation should be attempted -- if both are flattened sums, we cancel matching terms of opposite signs. -- if just one is a flattened sum, we add the other to it --print(". ",pos_reord," neg_reord: ",neg_reord," plus_op: ",plus_op," pos_tk: ",pos_tk); -- rewrite the positive and negative parts as a list of additive terms; -- if either is not such a list, convert it to a singleton list pos_reord :=if pos_tk = plus_op then pos_reord(2..) else [pos_reord] end if; nnre := #(neg_reord := if neg_tk = plus_op then neg_reord(2..) else [neg_reord] end if); -- also, get the length of the negative list of terms neg_posn := 1; -- this is advanced in the loop which follows, which iterates in coodinated fashion over the two ordered lists new_pos_reord := new_neg_reord := []; -- these will be collected after cancellation for pos_item in pos_reord loop -- iterate over the list of positive terms stgform_pos := str(standardize_bound_vars(pos_item)); -- convert it into a string, for subsequent comparison -- advance in the negative list, searching for a matching term, until we have gone too far while neg_posn <= nnre and (stgform_neg := str(standardize_bound_vars(neg_item := neg_reord(neg_posn)))) < stgform_pos loop new_neg_reord with:= neg_item; -- take the negative item and advance to the next negative item neg_posn +:= 1; end loop; -- at this point stgform_neg is at least as large as stgform_pos; check for an identical term if neg_posn <= nnre and stgform_pos = (stgform_neg := str(standardize_bound_vars(neg_item := neg_reord(neg_posn)))) then neg_posn +:= 1; continue; end if; -- omit any items which cancel new_pos_reord with:= pos_item; -- take the positive item and advance to the next positive item --print("nnre: ",nnre," new_pos_reord: ",new_pos_reord," new_neg_reord: ",new_neg_reord," neg_posn: ",neg_posn," stgform_pos: ",stgform_pos," stgform_neg: ",stgform_neg); end loop; -- here we must deal with any remaining negative and positive items if neg_posn <= nnre and stgform_neg > stgform_pos then new_neg_reord with:= neg_item; end if; -- take the last negative item examined if it is larger than the last positive item if neg_posn <= nnre then new_neg_reord +:= neg_reord(neg_posn + 1..); end if; -- take the unexamined negative items if any pos_tagged := if new_pos_reord = [] then [] -- tag positive and negative parts as sums if they involve more than one term elseif #new_pos_reord = 1 then new_pos_reord(1) else [plus_op] + new_pos_reord end if; neg_tagged := if new_neg_reord = [] then [] -- tag positive and negative parts as sums if they involve more than one term elseif #new_neg_reord = 1 then new_neg_reord(1) else [plus_op] + new_neg_reord end if; --print("new_pos_reord: ",new_pos_reord," new_neg_reord: ",new_neg_reord," pos_tagged: ",pos_tagged," neg_tagged: ",neg_tagged); -- if no terms remain, reeturn the appropraite zero -- if only a positive term remains, return it -- if only a negative term remains, return its reverse -- otherwise return the difference of the two terms return if pos_tagged = [] and neg_tagged = [] then zero_from_addn(plus_op) elseif neg_tagged = [] then pos_tagged elseif pos_tagged = [] then ["ast_of",sub_from_addn(plus_op),["ast_list",neg_tagged]] else [sub_op,pos_tagged,neg_tagged] end if; when "*" => return [tk] + [order_and_cancel(arg,plus_op): arg in sort_by_stgs(tree(2..))]; -- products are handled just by processing their factors recursively when "+" => return [tk] + [order_and_cancel(arg,plus_op): arg in sort_by_stgs(tree(2..))]; -- sums are handled just by processing their terms recursively -- but with a little more work we could look for opposing terms and cancel them otherwise => return tree; end case; end oorder_and_cancel; procedure sort_by_stgs(tree_tup); -- sorts a tuple of formula trees into alphabetical order of their standardized string form forms return [y: [x,y] in merge_sort([[str(standardize_bound_vars(tree)),tree]: tree in tree_tup])]; end sort_by_stgs; procedure standardize_subtree(tree,plus_op); -- debugging wrapper res := sstandardize_subtree(tree,plus_op); -- print("standardize_subtree:::: ",unparse(tree)," returns: ",unparse(res)); return res; end standardize_subtree; procedure sstandardize_subtree(tree,plus_op); -- reduces the top of an algebraic subtree to standardized form -- returns sequence of identical associative operator combinations as concatenated longer list of arguments, to allow sorting --if debug_flag then end if; reversal_op := reversal_from_addn(plus_op); -- find the reversal operator for the algebraic opearator family of this tree subtraction_op := sub_from_addn(plus_op); -- find the subtraction operator for the algebraic opearator family of this tree zero := zero_from_addn(plus_op); -- find the zero constant for the algebraic opearator family of this tree one := one_from_addn(plus_op); -- find the unit constant for the algebraic opearator family of this tree if is_string(tree) then return tree; end if; -- for variables there is nothing to do [n1,n2,n3] := tree; -- unpack the tree into its lead operator and two (or fewer) arguments if (ao := alg_of(node_kind := if n1 = "ast_of" then n2 else n1 end if)) /= plus_op or alg_role_of(node_kind) = "OM" then return tree; end if; -- if the tree is not consistent with the indicated plus_op, simply return it args := if n1 = "ast_of" then n3(2..) else tree(2..) end if; -- allow for case of monadic reversal operator, in which case 'args' is abtained from the template -- ["ast_of","rev",[ast_list,arg]] standardized_args := [standardize_subtree(arg,plus_op): arg in args]; -- standardize the operator arguments recursively. Each standardized argument returned will be either a string -- representing a zero or unit constant, the topmost node of a subtree not belonging to the same -- algebraic set as 'tree', or a flattened product, flattened sum of products, difference of -- flattened sums, or reversed flattened sum --print("standardize_subtree: ",tree," ao: ",ao," standardized_args: ",standardized_args); -- get the leading operator of the first argument opk := if (a1 := standardized_args(1))(1) = "ast_of" then a1(2) elseif a1 = zero or a1 = one then a1 else a1(1) end if; first_op_kind := if alg_of(opk) /= plus_op then "OM" else alg_role_of(opk) end if; -- if the op_kind is OM, or the first argument does not belong to the same algebraic set as its parent, -- convert it to the string OM if a1(1) = "ast_of" and a1(2) = reversal_op then a1 := a1(3)(2); end if; -- extract the value of argument if it is a reversal -- if here is a second argument, get its lead operator if (a2 := standardized_args(2)) /= OM then opk := if a2(1) = "ast_of" then a2(2) elseif a2 = OM then "OM" elseif a2 = zero or a2 = one then a2 else a2(1) end if; second_op_kind := if alg_of(opk) /= plus_op then "OM" else alg_role_of(opk) end if; if a2(1) = "ast_of" and a2(2) = reversal_op then a2 := a2(3)(2); end if; -- extract the value of argument if it is a reversal end if; --print("standardize_subtree: ",tree," first_op_kind: ",first_op_kind," second_op_kind: ",second_op_kind," zero: ",zero," a1: ",a1); --print("reversal_op: ",reversal_op," alg_role_of(n1): ", alg_role_of(n1)); -- process the separate cases that arise, accodring to the algebraic nature of the topmost -- tree operator, and then the nature of the lead operators of its first and second argument --if debug_flag then print("alg_role_of(node_kind):::: ",alg_role_of(node_kind)); end if; case alg_role_of(node_kind) -- node_kind is used so that Rev operators, which are function aplications, are teated correctly when "+","+nc" => -- TOP LEVEL CASE: addition or non-commutative addition --print("addition: ",a1," ",a2); case first_op_kind -- process the various kinds of first operands, case by case when "OM","1","*","*nc" => -- FIRST OPERAND CASE: addition: first op is non-algebraic or a flattened product case second_op_kind when "OM","1","*" => -- SECOND OPERAND CASE: second op is non-algebraic or a flattened product; -- just return a sum after putting the two operands into standardized order return [n1] + sort_by_stgs([a1,a2]); when "0" => -- second op is zero; na + 0 return a1; -- return the first op when "+" => -- second op is a flattened sum; prepend first arg return conc_em(a1,a2,plus_op); -- conc_em builds and returns a flattened sumflattened sum when "-" => -- second op is a difference; prepend its first arg to the first argument, and return a difference [sub_op,a22,a23] := a2; --print("addition then subtraction: ",first_op_kind," ",second_op_kind," a1: ",a1," a2: ",a2," result: ",[sub_op,conc_em(a1,a22,plus_op),a23]); return [sub_op,conc_em(a1,a22,plus_op),a23]; when "--" => -- second op is a reversal; return the difference of the first op and the second op's argument -- note that here a2 is already the value of the reversal argument return [subtraction_op,a1,a2]; end case; when "0" => -- FIRST OPERAND CASE: addition: first op is zero; return second op --print("first op is zero: ",if second_op_kind = "--" then ["ast_of",reversal_op,["ast_list",a2]] else a2 end if); return if second_op_kind = "--" then ["ast_of",reversal_op,["ast_list",a2]] else a2 end if; when "+","+nc" => -- FIRST OPERAND CASE: addition: first op is a sum case second_op_kind when "OM","1","*" => -- second op is non-algebraic or a product return conc_em(a1,a2,a1(1)); when "0" => -- second op is zero return a1; -- return the first op when "+" => -- second op is a flattened sum return conc_em(a1,a2,a1(1)); when "-" => -- second op is a difference; return concatenatated sum minus second arg of second arg [sub_op,a22,a23] := a2; return [sub_op,conc_em(a1,a22,a1(1)),a23]; when "--" => -- second op is a reversal this is a1 + (-a2) -- note that here a2 is already the value of the reversal argument return [subtraction_op,a1,a2]; -- return a difference end case; when "-" => -- FIRST OPERAND CASE: subtraction: first op is a difference case second_op_kind when "OM","1","*" => -- second op is non-algebraic or a product [sub_op,a12,a13] := a1; return [sub_op,conc_em(a12,a2,n1),a13]; when "0" => -- second op is zero return a1; -- return the first op when "+" => -- second op is a flattened sum; return concatenatated sum minus second arg of first arg [sub_op,a12,a13] := a1; return [sub_op,conc_em(a12,a2,a2(1)),a13]; -- use the addition operator a2(1) from the second operand when "-" => -- second op is a difference [sub_op,a12,a13] := a1; [-,a22,a23] := a2; return [sub_op,conc_em(a12,a22,n1),conc_em(a13,a23,n1)]; when "--" => -- second op is a reversal this is (a - b) - a2, becomes a - (b + a2) -- note that here a2 is already the value of the reversal argument [sub_op,a12,a13] := a1; conced_subs := conc_em(a13,a2,n1); return [sub_op,a12,conced_subs]; -- return a difference with a concatenated subtrahend end case; when "--" => -- FIRST OPERAND CASE: addition: first op is a reversal case second_op_kind when "--" => -- second op is also reversal. This is (-a) + (-b), becomes -(a + b) return ["ast_of",reversal_op,["ast_list",conc_em(a1,a2,plus_op)]]; -- JACK -- reversals are pushed to the outside, so this case becomes -(a + b) otherwise => return tree; -- no change in this case end case; end case; when "-" => -- TOP LEVEL CASE: subtraction --print("subtraction: ",a1," ",a2," ",first_op_kind," ",second_op_kind); case first_op_kind when "OM","1","*" => -- subtraction: first op is non-algebraic, or a product case second_op_kind when "OM","1","*","+" => -- second op is non-algebraic, or a product, or a flattened sum return [n1,a1,a2]; -- build into difference when "0" => -- second op is zero return a1; -- return the first op when "-" => -- second op is a difference. this is the case (a - (b - c)) becomes a + c - b [-,a22,a23] := a2; -- decompose second op return [n1,conc_em(a1,a23,plus_op),a22]; -- reverse second op and build into difference when "--" => -- second op is a reversal; convert to a sum: (a - (-b)) becomes (a + b) -- note that here a2 is already the value of the reversal argument return conc_em(a1,a2,plus_op); end case; when "0" => -- subtraction: first op is zero case second_op_kind when "OM","1","+","*" => -- second op is non-algebraic return ["ast_of",reversal_op,["ast_list",a2]]; -- convert to a reversal when "0" => -- second op is zero return zero; when "-" => -- second op is a difference: this is the case 0 - (a - b), becomes (b - a) [sub_op,a22,a23] := a2; -- decompose second op return [sub_op,a23,a22]; -- reverse the subtraction when "--" => -- second op is a reversal; this is the case 0 - (-a) becomes a; just return the value being reversed -- note that here a2 is already the value of the reversal argument return a2; -- reverse the difference end case; when "+" => -- subtraction: first op is a flattened sum case second_op_kind when "OM","1","+","*" => -- second op is non-algebraic, or involves no subtraction return [n1,a1,a2]; -- just build into subtraction when "0" => -- second op is zero return a1; -- return the first op when "-" => -- second op is a difference [-,a22,a23] := a2; -- decompose second op return [n1,conc_em(a1,a23,plus_op),a22]; -- reverse the subtraction when "--" => -- second op is a reversal: this is a1 - (-b)) -- note that in this case a2 is already the value being reversed return conc_em(a1,a2,plus_op); end case; when "-" => -- subtraction: first op is a difference [-,a12,a13] := a1; -- unpack it case second_op_kind when "OM","1","*","+" => -- second op is non-algebraic, or involves no subtraction return [n1,a12,conc_em(a13,a2,plus_op)]; -- just build into subtraction when "0" => -- second op is zero return a1; -- return the first op when "-" => -- second op is a difference [-,a22,a23] := a2; -- decompose second op return [n1,conc_em(a12,a23,plus_op),conc_em(a13,a22,plus_op)]; -- reverse the subtraction when "--" => -- second op is a reversal return [n1,conc_em(a12,a2,plus_op),a13]; -- reverse and add end case; when "--" => -- subtraction: first op is a reversal -- note that in this case a1 is already the value being reversed --print("subtraction first op is a reversal: ",a1," ",a2," ",[n1,a1,a2]); case second_op_kind when "OM","1","+","*" => -- second op is non-algebraic, or involves no subtraction. -- This is (-a1) - b becomes -(a + b), since the reversal cannot be pushed into b return ["ast_of",reversal_op,["ast_list",standardize_subtree([plus_op,a1,a2],plus_op)]]; when "0" => -- second op is zero return ["ast_of",reversal_op,["ast_list",a1]]; -- return the rebuilt first op when "-" => -- second op is a difference [-,a22,a23] := standardize_subtree([n1,a1,a2],plus_op); -- handle recursively return [n1,a23,a22]; -- build reversed arguments into subtraction when "--" => -- second op is a reversal: this is (-a1) - (-a2), becomes (a2 - a1) return [n1,a2,a1]; -- build reversed arguments into subtraction end case; end case; when "--" => -- TOP LEVEL CASE: additive inverse; there is just one argument --print("additive inverse: ",a1); case first_op_kind when "+" => -- Inversion: argument is an addition; push reversals outward so -(a + b) remains the same return ["ast_of",reversal_op,["ast_list",a1]]; -- standardize the argument, and return as Inversion when "OM","1","*" => -- Inversion: first op is non-algebraic or involves no subtraction return ["ast_of",reversal_op,["ast_list",a1]]; when "0" => -- Inversion: first op is zero return zero; -- result is 0 when "-" => -- Inversion: first op is a difference [sub_op,a12,a13] := a1; -- decompose first op return [sub_op,a13,a12]; -- reverse the subtraction when "--" => -- Inversion: first op is a reversal return a1; -- double reversal is original end case; when "*","*nc" => -- TOP LEVEL CASE: commutative or non-commutative multiplication case first_op_kind when "OM" => -- FIRST OPERAND CASE: multiplication: first op is non-algebraic case second_op_kind when "OM" => -- second op is non-algebraic return [n1,a1,a2]; when "0" => -- second op is zero return zero; when "1" => -- second op is unity return a1; when "+" => -- second op is a flattened sum; distribute the product --print("second op is a flattened sum: ",a2(2..)," ",distribute_mult([a1],a2(2..),n1)); -- this routine expects to be passed tuples of sums to be multiplied out return distribute_mult([a1],a2(2..),n1); when "-" => -- second op is a difference; distribute the product [sub_op,a22,a23] := a2; -- decompose second op --print("second op is a difference: a2: ",a2," a1: ",a1," n1: ",n1); -- this routine expects to be passed tuples of sums to be multiplied out return [sub_op,distribute_mult([a1],[a22],n1),distribute_mult([a1],[a23],n1)]; -- distribute the subtraction when "--" => -- second op is a reversal; return a reversed concatenated product unreversed_prod := conc_em(a1,a2,n1); -- concatenate the nonalgebraic argument with the argument of the reversal --print("unreversed_prod: ",unreversed_prod," ",a2); return ["ast_of",reversal_op,["ast_list",unreversed_prod]]; -- build into a top-level reversal and return when "*" => -- second op is a flattened product --print("second op is a flattened product: ",conc_em(a1,a2,a2(1))," ",a2(1)); return conc_em(a1,a2,a2(1)); -- use the product operation from the second operand end case; when "0" => -- FIRST OPERAND CASE: multiplication: first op is zero return zero; when "1" => -- FIRST OPERAND CASE: multiplication: first op is unity return if second_op_kind = "--" then ["ast_of",reversal_op,["ast_list",a2]] else a2 end if; -- return the actual second argument when "+" => -- FIRST OPERAND CASE: addition: first op is a flattened sum --print("top level is multiplication: first op is a flattened sum, second_op_kind is: ",second_op_kind," a1: ",unparse(a1)," a2: ",unparse(a2)); case second_op_kind when "OM","*" => -- second op is non-algebraic or is a product --print("distribute_mult: ",unparse(distribute_mult(a1(2..),[a2],n1))); return distribute_mult(a1(2..),[a2],n1); -- this routine expects to be passed tuples of sums to be multiplied out when "0" => -- second op is zero return zero; when "1" => -- second op is unity return a1; -- return the first op when "+" => -- second op is a flattened sum; form double distribution of sums --print("double distribution: ",a1(2..)," ",a2(2..)," ",distribute_mult(a1(2..),a2(2..),n1)); return distribute_mult(a1(2..),a2(2..),n1); -- this routine expects to be passed tuples of sums to be multiplied out when "-" => -- second op is a difference; form double distribution of difference [sub_op,a22,a23] := a2; -- decompose second op --print("sum times difference: ",a1," ",a2," ",distribute_mult(a1(2..),a22(2..),n1)," ",distribute_mult(a1(2..),a23(2..),n1)); return [sub_op,distribute_mult(a1(2..),if is_string(a22) or alg_of(a22(1)) /= plus_op then [a22] else a22(2..) end if,n1), distribute_mult(a1(2..),if is_string(a23) or alg_of(a23(1)) /= plus_op then [a23] else a23(2..) end if,n1)]; -- distribute the subtraction -- distribute_mult expects to be passed tuples of sums to be multiplied out when "--" => -- second op is a reversal; form reversed result --print("second op is a reversal: ",ao," ",a1," ",a2); return ["ast_of",reversal_op,["ast_list",standardize_subtree([n1,a1,a2],ao)]]; -- this operation is executed recursively end case; when "-" => -- FIRST OPERAND CASE: multiplication: first op is a difference [-,a12,a13] := a1; -- decompose first op; this is a12 - a13 case second_op_kind when "OM" => -- second op is non-algebraic. This case is (a12 - a13) • a2, where a12 and a13 can be flattened sums -- we distribute the multiplication over the subtraction and return a difference first_arg_pos_terms := if is_string(a12) or alg_of(a12(1)) /= plus_op or alg_role_of(a12(1)) /= "+" then [a12] else a12(2..) end if; first_arg_neg_terms := if is_string(a13) or alg_of(a13(1)) /= plus_op or alg_role_of(a13(1)) /= "+" then [a13] else a13(2..) end if; --print("first arg of a product is a difference, second arg is non-algebraic: a1: ",unparse(a1)," a2: ",unparse(a2)," first_dist: ",unparse(distribute_mult(first_arg_pos_terms,[a2],n1))," second_dist: ",unparse(distribute_mult(first_arg_neg_terms,[a2],n1))); return [a1(1),distribute_mult(first_arg_pos_terms,[a2],n1), distribute_mult(first_arg_neg_terms,[a2],n1)]; -- distribute the multiplications and return a difference -- distribute_mult expects to be passed tuples of sums to be multiplied out when "0" => -- second op is zero return zero; when "1" => -- second op is unity return a1; when "+" => -- second op is a flattened sum return [a1(1),distribute_mult(if is_string(a12) or alg_of(a12(1)) /= plus_op or alg_role_of(a12(1)) /= "+" then [a12] else a12(2..) end if,[a2],n1), distribute_mult(if is_string(a13) or alg_of(a13(1)) /= plus_op or alg_role_of(a13(1)) /= "+" then [a13] else a13(2..) end if,[a2],n1)]; -- distribute the subtraction when "-" => -- second op is a difference; product of two differences [-,a12,a13] := a1; -- decompose first op a12ta22 := distribute_mult(if is_string(a12) or alg_of(a12(1)) /= plus_op or alg_role_of(a12(1)) /= "+" then [a12] else a12(2..) end if,if is_string(a22) or alg_of(a22(1)) /= plus_op then [a22] else a22(2..) end if,n1); a13ta23 := distribute_mult(if is_string(a13) or alg_of(a13(1)) /= plus_op or alg_role_of(a13(1)) /= "+" then [a13] else a13(2..) end if,if is_string(a23) or alg_of(a23(1)) /= plus_op then [a23] else a23(2..) end if,n1); pos_part := conc_em(a12ta22,a13ta23,ao); a12ta23 := distribute_mult(if is_string(a12) or alg_of(a12(1)) /= plus_op or alg_role_of(a12(1)) /= "+" then [a12] else a12(2..) end if,if is_string(a23) or alg_of(a23(1)) /= plus_op then [a23] else a23(2..) end if,n1); a13ta22 := distribute_mult(if is_string(a13) or alg_of(a13(1)) /= plus_op or alg_role_of(a13(1)) /= "+" then [a13] else a13(2..) end if,if is_string(a22) or alg_of(a22(1)) /= plus_op then [a22] else a22(2..) end if,n1); neg_part := conc_em(a12ta23,a13ta23,ao); return [a1(1),pos_part,neg_part]; when "--" => -- second op is a reversal [-,a12,a13] := a1; -- decompose first op pos_prod := distribute_mult(if is_string(a12) or alg_of(a12(1)) /= plus_op or alg_role_of(a12(1)) /= "+" then [a12] else a12(2..) end if,if is_string(a2) or alg_of(a2(1)) /= plus_op then [a2] else a2(2..) end if,n1); neg_prod := distribute_mult(if is_string(a13) or alg_of(a13(1)) /= plus_op or alg_role_of(a13(1)) /= "+" then [a13] else a13(2..) end if,if is_string(a2) or alg_of(a2(1)) /= plus_op then [a2] else a2(2..) end if,n1); return [a1(1),neg_prod,pos_prod]; when "*" => -- second op is a flattened product; prepend the first argument to the second and return as a flattened product -- the case here is (a12 - a13) • a2, a2 being a product return [a1(1),conc_em(a12,a2,n1),conc_em(a13,a2,n1)]; -- return the distributed difference -- return something; end case; when "--" => -- FIRST OPERAND CASE: multiplication: first op is a reversal case second_op_kind when "OM","+","*" => -- second op is non-algebraic (times reversal or sum; handle recursivey) unreversed_prod := [n1,a1,a2]; return ["ast_of",reversal_op,["ast_list",standardize_subtree(unreversed_prod,ao)]]; when "0" => -- second op is zero return zero; when "1" => -- second op is unity return ["ast_of",reversal_op,["ast_list",a1]]; -- restore the initially removed reversal when "-" => -- second op is a difference [r0,r1,r2] := standardize_subtree([n1,a1,a2],ao); return [r0,r2,r1]; when "--" => -- second op is a reversal (drop reversals and handle recursively) unreversed_prod := [n1,a1,a2]; return standardize_subtree(unreversed_prod,ao); end case; when "*" => -- FIRST OPERAND CASE: multiplication: first op is a flattened product case second_op_kind when "OM" => -- second op is non-algebraic --print("multiplication: first op is a flattened product second op is non-algebraic: ",conc_em(a1,a2,n1)); return conc_em(a1,a2,n1); -- concatenate the products when "0" => -- second op is zero return zero; when "1" => -- second op is unity return a1; when "+" => -- second op is a flattened sum; distribute return distribute_mult([a1],a2(2..),n1); when "-" => -- second op is a difference; distribute over difference [sub_op,a22,a23] := a2; -- decompose second op pos_part := distribute_mult([a1],if is_string (a22) then a22 else a22(2..) end if,n1); neg_part := distribute_mult([a1],if is_string (a23) then a23 else a23(2..) end if,n1); return [sub_op,pos_part,neg_part]; when "--" => -- second op is a reversal; handle recursively unreversed_prod := [n1,a1,a2]; return ["ast_of",reversal_op,["ast_list",standardize_subtree(unreversed_prod,ao)]]; when "*" => -- second op is a flattened product --print("product of products: ",a1," ",a2); return conc_em(a1,a2,n1); end case; otherwise => return tree; end case; otherwise => return tree; end case; end sstandardize_subtree; procedure conc_em(a1,a2,conc_op); -- concatenates two flattened sequences, at least one of which begins with conc_op a1 := if is_tuple(a1) and a1(1) = conc_op then a1(2..) else [a1] end if; a2 := if is_tuple(a2) and a2(1) = conc_op then a2(2..) else [a2] end if; return [conc_op] + a1 + a2; end conc_em; procedure re_nest(flattened_tree); -- recursively reconvert a standardized (flattened) tree to its ordinary 'nested' form --if debug_flag then print("tree to unflatten: ",flattened_tree); end if; if is_string(flattened_tree) then return flattened_tree; end if; [n1,n2,n3] := flattened_tree; -- unpack the flattened tree op_kind := if n1 = "ast_of" then alg_role_of(n2) else alg_role_of(n1) end if; --if debug_flag then print("re_nest: ",op_kind," ",n1," ",flattened_tree); end if; if op_kind = OM or op_kind notin {"+","+nc","*","*nc","-","--"} then return flattened_tree; end if; -- handle non-algebraic nodes if op_kind = "--" then -- put reversal into standard form, dropping double reversals if is_tuple(revarg := n3(2)) and revarg(1) = n1 and revarg(2) = n2 then -- double reversal, so drop (recursively) return re_nest(revarg(3)(2)); end if; return [n1,n2,["ast_list",re_nest(n3(2))]]; end if; if op_kind = "-" then -- flatten the subtraction arguments [sub_op,a1,a2] := flattened_tree; return [sub_op,re_nest(a1),re_nest(a2)]; end if; -- if the operation is commutative, and is either a multiplication of an addition, sort its arguments if op_kind = "+" or op_kind = "*" then --if debug_flag then print("flattened_tree before: ",flattened_tree); end if; flattened_tree := [n1] + sort_by_stgs([re_nest(comp): comp = flattened_tree(2..)(j)]); --if debug_flag then print("flattened_tree after: ",flattened_tree); end if; else -- ovoid sorting since not known to be commutative flattened_tree := [if j = 1 then comp else re_nest(comp) end if: comp = flattened_tree(j)]; -- re-nest the tree arguments end if; nested := flattened_tree(1..3); for j in [4..#flattened_tree] loop nested := [n1,nested,flattened_tree(j)]; end loop; --print("re_nesting: ",op_kind," ",n1," ",flattened_tree," ",nested); return nested; end re_nest; procedure distribute_mult(tup1,tup2,mult_op); -- distribute one tuple of sums over another -- this routine expects to be passed tuples of sums to be multiplied out --print("distribute_mult tup1: ",tup1," tup2: ",tup2," mult_op: ",mult_op); plus_op := alg_of(mult_op); --print("unstandardized result: ",[plus_op] + [conc_em(x,y,mult_op): x in tup1,y in tup2]); res := if #tup1 = 1 and #tup2 = 1 then conc_em(tup1(1),tup2(1),mult_op) -- if the argumets are both monomials, just multiply them -- otherwise mutiply their separate terms and return the sum of these products -- else re_nest(standardize_subtree(unstand := [plus_op] + [re_nest(conc_em(x,y,mult_op)): x in tup1,y in tup2],plus_op)) end if; else re_nest(standardize_subtree(re_nest(unstand := [plus_op] + [re_nest(conc_em(x,y,mult_op)): x in tup1,y in tup2]),plus_op)) end if; --print("distribute_mult tup1: ",unparse(tup1)," tup2: ",unparse(tup2)," mult_op: ",mult_op," res: ",unparse(res)," unstand: ",unstand," standardize_subtree(unstand,plus_op): ",standardize_subtree(unstand,plus_op)); return res; end distribute_mult; -- ********************************************************************* -- ********************* Algebraic standardization ********************* -- ********************************************************************* -- If addition, subtraction, and multiplication, and both zero and unit constants are available, -- we reduce formulae by distributing multiplication over addition and subtraction, until -- a formula is fully reduced to a sum/difference of products. If multiplication is commutative -- all the bottom-level products are then rearranged in alphabetical order of their blobs. Pure -- nested runs of additions and subtractions are first rearranged in alphabetical order of their blobs -- so that cancellaion of terms having identical blobs can be performed. These terms are then rearranged -- in alphabetical order. Hence the standardized form of an algebraic node is either: (i) one of -- the constants 0 or 1; (ii) a non-algebraic term; (iii) a product of non-algebraic terms, -- arranged in alphabetical order of their blobs if multiplication is commutaive; -- (iv) a sum of such products, arranged in alphabetical order of their blobs; (v) a difference -- of such sums; or (vi) the reverse of such a sum. -- Each algebraic node in a tree is associated with an algebraic operator set, which contains at least -- an associative addition operator '+', and perhaps also and additive unit '0', an additive inversion -- operator '-' which can also be used in infix form as a subtraction operator, -- a multiplication operator '*' (in which case the addition operator is required to be commutative), -- and a multiplicative unit constant '1'. The map alg_of op sends each of these operators into the -- associated '+' operator (which is always used as the representative of the algebraic operator set -- to which it belongs). The map alg_role_of(op_sign), whose value can be '0', '1', '+', -- '+nc' (non-commutative addition), '-', '--' (additive inverse), '*' (multiplication), or -- '*nc' (non-commutative multiplication). -- (additive inverse), procedure post_alg_roles(stg); -- adds an algebraic set to alg_of and alg_role_of maps -- also builds the auxiliary maps sub_from_addn,reversal_from_addn -- the string contains the comma-separated operator names in -- any order, each followed by its role -- The string supplied should consit of ring operator names in alll the odd positions, followed by standard names -- for the algebraic roles of each operator and constant in the following even position. The standard -- operator names to be used are + - -- (monadic minus) *; the standard constant signs are 0 1 -- an example is post_alg_roles("•S_PLUS,+,•S_ZERO,0,•S_ONE,1,•S_MINUS,-,•S_REV,--,•S_TIMES,*,Za,ring"); data := breakup(stg,",;"); -- cut the string into a tuple -- check that the string supplied has an even number of components and contains a plus operator -- and has ony known standard operator signs in its even positions if (not even(#data)) or (not (exists plusop = data(j) | (odd(j) and data(j + 1) = "+"))) or (exists opsign = data(j) | (even(j) and data(j) notin {"0","1","+","+nc","-","--","*","*nc","OM","ring"})) then print("******* Error: algebraic operator set declaration ",stg," is faulty"); return; end if; for opsign = data(j) | odd(j) loop -- iterate over the tuple, noting the algebraic role of each operator sign supplied alg_of(opsign) := plusop; -- maps all algebraic operators into the plus operator of their ring alg_role_of(opsign) := djp := data(j + 1); -- but then correct -- extend supplementary maps sub_from_addn, reversal_from_addn, zero_from_addn, one_from_addn, mult_from_addn, etc. if djp = "-" then sub_from_addn(plusop) := opsign; elseif djp = "--" then reversal_from_addn(plusop) := opsign; end if; if djp = "0" then zero_from_addn(plusop) := opsign; end if; if djp = "1" then one_from_addn(plusop) := opsign; end if; if djp = "*" then mult_from_addn(plusop) := opsign; end if; if djp = "ring" then ring_from_addn(plusop) := opsign; end if; end loop; --print("alg_of: ",alg_of," ",alg_role_of," ",zero_from_addn); end post_alg_roles; procedure find_ring_members(tree); -- collects the ring membership assertions at the top conjunctive level of a tree var memb_assertions := {[x,{["ast_in",y,ring := ring_from_addn(x)],["ast_in",zero_from_addn(x),ring]}]: [x,y] in one_from_addn}; -- intialize to known members (0 and 1) this maps each known addition operator for a ring R into a pair of assertions -- of the abstract form {'0 in R', '1 in R'} -- recursive workhorse will collect and arrange by algebraic set find_ring_members_in(tree); -- collects the ring membership assertions by recursive treewalk --print("find_ring_members return: ",memb_assertions); return memb_assertions; -- return the full set of ring membership assertions found at top level procedure find_ring_members_in(tree); -- collects the ring membership assertions if is_string(tree) then return; end if; -- nothing to do if string [n1,n2,n3] := tree; -- unpack tree -- process top-level conjuncts by walkig recursively dwn the lis of conjuctions at the top level if n1 = "ast_and" or n1 = "AMP_" then find_ring_members_in(n2); find_ring_members_in(n3); return; end if; --print("find_ring_members_in: ",tree," alg_of(n3): ",alg_of(n3)); -- otherwise, if we have a membership statement in a node whose opearator is algebraic, then collect it if n1 = "ast_in" and (plus_op := alg_of(n3)) /= OM and n3 = ring_from_addn(plus_op) then -- we have a conjunct of the form x in R; collect this ring membership assertion memb_assertions(plus_op) := (memb_assertions(plus_op)?{}) with tree; end if; end find_ring_members_in; end find_ring_members; -- ******************************************************************************** -- *********** Miscellaneous tree searching and transformation routines *********** -- ******************************************************************************** procedure find_fnc_symbs(node); -- find the function symbols in a tree (main entry) all_fnc_symbs := {}; find_fnc_symbs_in(node); return all_fnc_symbs - builtin_fcns; -- use the recursive workhorse and a global variable end find_fnc_symbs; procedure find_fnc_symbs_in(node); -- find the function symbols in a tree (recursive workhorse) --print("find_fnc_symbs_in: ",node," ",is_string(node)," ",all_fnc_symbs); if is_string(node) then return; end if; -- down to a variable or constant case (ah := abbreviated_headers(n1 := node(1)))?n1 when "()" => -- this is the case of functional and predicate application; the second variable is a reserved symbol, not a set all_fnc_symbs with:= node(2); for sn in node(3..) loop find_fnc_symbs_in(sn); end loop; when "and","or","==","+","-","{-}","in","notin","/==","=","/=","[]","[-]","ast_if_expr","ast_if", "{.}","itr","Etr","incs","incin","imp","*","->","not","null","{}","{/}","EX","ALL" => -- various builtins for sn in node(2..) loop find_fnc_symbs_in(sn); end loop; -- now collect free variables in args otherwise => -- additional infix, prefix, and ordinary operators; functional application all_fnc_symbs with:= node(if #node = 2 then 1 else 1 end if); for sn in node(2..) loop find_fnc_symbs_in(sn); end loop; -- now collect free variables in args end case; end find_fnc_symbs_in; procedure dequantify(tree,substitution_tup); -- makes substitutions for specified quantified variables of a formula. (main entry; uses workhorse) -- this routine works from left-to right through a quantified formula, progressively using elements from the -- indicated tuple to make day_total for the bound variables encountered. It descends thru quantifiers, -- the boolean operators and, or, not, and •imp (but not equivalences), keeping track of the boolean sign -- of the terms encountered, and replacing quantified variables where possible. day_total of non-strings -- for existential quantified variables are refused. -- A triple [substituted_formula,set_of_strings_skolemized,unused_] is returned. -- non-empty unused_substitutions list probably represents an error. -- to allow specified quantifiers or setformers which would otherwise attract substitutions to be bypassed -- selectively, we allow OM elements to be included in the susbstitution tup passed to this routine. -- when such an OM is matched to a substitution-candidate explciitly or implicitly quantified subexpression, -- it terminates substitution, either before it started or at the quantifier reached. return dequantify_in(tree,substitution_tup,{},true,{}); print("returned: ",res); -- call the workhorse with an initially null list of bound variables end dequantify; procedure dequantify_in(tree,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); --print("dequantify_in_trace: ",unparse(tree)); res := dequantify_in_trace(tree,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); --print("returned: ",res); return res; end dequantify_in; procedure dequantify_in_trace(tree,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- inner recursive workhorse of substitution routine. substitution_tup is passed down from the initial -- call, with progressive deletion of the elements of substitution_tup as they are used and -- pass into substitution_map, which is used so that every occurrence of a bound variable -- will be replaced by its assigned expression, if it has not been bypassed if is_string(tree) and tree in bound_vars then -- replace bottom-level names as specified return substitution_map(tree)?tree; end if; [n1,n2,n3] := tree; -- unpack the node case abbreviated_headers(n1)?n1 -- handle quantifiers and setformers in a special way, to detect bound variables when "and","or" => -- 'positive' boolean operators [n2,skolemized_in_a1,substitution_tup] := dequantify_in(n2,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- continue recursively [n3,skolemized_in_a2,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- continue recursively return [[n1,n2,n3],skolemized_in_a1 + skolemized_in_a2,substitution_tup]; -- since substitutions may have been done in either of the arguments, substitution_tup may have shortened when "not" => -- 'negative' boolean operator [n2,skolemized_in_a1,substitution_tup] := -- continue recursively, reversing the virtual sign of the subformula dequantify_in(n2,substitution_tup,substitution_map,not bool_sign,bound_vars_not_replaced); return [[n1,n2],skolemized_in_a1,substitution_tup]; -- since substitutions may have been done in either of the arguments, substitution_tup may have shortened when "imp" => -- 'mixed' boolean operator; this is like 'or', but the first argument reverses sign [n2,skolemized_in_a1,substitution_tup] := dequantify_in(n2,substitution_tup,substitution_map,not bool_sign,bound_vars_not_replaced); -- continue recursively --print("imp: ",n3," substitution_tup: ",substitution_tup," substitution_map: ",substitution_map); [n3,skolemized_in_a2,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- continue recursively return [[n1,n2,n3],skolemized_in_a1 + skolemized_in_a2,substitution_tup]; -- since substitutions may have been done in either of the arguments, substitution_tup may have shortened when "EX" => -- existential. The second node is an iterator -- a syntactic example is: ["ast_iter_list", ["ast_in", "X", "S"], ["DOT_INCIN", "Y", "T"]]. [n1,n2,n3] := tree; -- unpack the parts of the syntax node limiting_clauses := []; -- the limiting_clauses will be conjoined into a final conjunction, which will appear in -- result formula as (clause1 & clause2 & ...) •imp substituted_body leftover_iteration_clauses := []; -- to accumulate iteration_clauses whose bound variable is not replaced iter_tag := n2(1); -- get the list tag for the iterator replacement_stopped := false; -- flag indicating wheter replacement was stopped either explicitly or implicitly if not bool_sign then -- the sign has reversed, so this is an implicit universal. all substitutions will be accepted for [iter_op,bv,limiting_expn] in n2(2..) loop -- process all the clauses of the iterator if substitution_tup /= [] and not replacement_stopped then -- there are still more substitutions available, so make one more limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced); -- make the accumulated substitution in the limiting_expn; use the inner workhorse directly replacement_expression fromb substitution_tup; -- get the next replacement expression to use if replacement_expression = OM then -- replacement is being stopped manually replacement_stopped := true; -- only prior replacements will be used substitution_tup := [replacement_expression] + substitution_tup; -- return the unused replacement expression else -- note the replacement to be made henceforth substitution_map(bv) := replacement_expression; -- this will replace the bound variable henceforth end if; limiting_clauses with:= [iter_op,replacement_expression,limiting_expn]; -- in the new clause, the bound variable is replaced -- accumulate the substituted limiting_clause, for later use, as explained above else -- there are no more substitutions available or replacement has been stopped, -- so the remaining pieces of the iterator are 'leftovers' limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced); -- make the accumulated substitution in the limiting_expn; use the inner workhorse directly leftover_iteration_clauses with:= [iter_op,bv,limiting_expn]; -- the substituted clause will be used in a quantifier end if; end loop; -- once all the clauses of the iterator have been processed, we process the quantified predicate -- this is the existential case, reversed bound_vars_not_replaced +:= {b: [op,bv,limit] in leftover_iteration_clauses}; -- there may be additional bound variables not being replaced if leftover_iteration_clauses = [] then -- just return the substituted body as an implication involving all the limiting_clauses [n3,skolemized_in_pred,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- make substitutions in the predicate conj := conjoin(limiting_clauses); -- conjoin a collection of clauses return [if limiting_clauses = [] then n3 else ["ast_and",conj,n3] end if,skolemized_in_pred,substitution_tup]; -- return the said implication else -- return the substituted body as a quantified implication involving all the limiting_clauses n3 := substitute_in(n3,substitution_map,bound_vars_not_replaced); -- make a simple substitution n3 := [n1,[iter_tag] + leftover_iteration_clauses,n3]; -- reattach the quantifier and remaining iterators conj := conjoin(limiting_clauses); -- conjoin a collection of clauses return [if limiting_clauses = [] then n3 else ["ast_and",conj,n3] end if,[],substitution_tup]; -- return the said implication. nothing is skolemized end if; else -- this is really an existential, so only constant substitutions will be accepted. These will be -- noted as having been skolemized, i.e. they receive their definitions by replacing bound variables in an existential skolemized_here := []; -- start collecting variables which are skolemized by this existential for [iter_op,bv,limiting_expn] in n2(2..) loop -- process the clauses of the iterator until the first that gives trouble if substitution_tup /= [] and not replacement_stopped then -- there are still more substitutions available, so see if we can make one more limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced); -- make the accumulated substitution in the limiting_expn; use the inner workhorse directly replacement_expression fromb substitution_tup; -- get the next replacement expression to use if replacement_expression = OM or not is_string(replacement_expression) then -- replacement is being stopped manually or implicitly --print("really an existential replacement_stopped:"); replacement_stopped := true; -- only prior replacements will be used leftover_iteration_clauses with:= [iter_op,bv,limiting_expn]; -- this iteration clause is bypassed substitution_tup := [replacement_expression] + substitution_tup; -- return the unused replacement expression else -- skolemization by this existential is possible substitution_map(bv) := replacement_expression; -- this string will replace the bound variable henceforth limiting_clauses with:= [iter_op,replacement_expression,limiting_expn]; -- in the new clause, the bound variable is replaced. -- accumulate the substituted limiting_clause, for later use, as explained above skolemized_here with:= replacement_expression; -- note that the replacement_expression (a string) -- is being defined here end if; else -- there are no more susbstitutions available or replacement has been stopped, -- so the remaining pieces of the iterator are 'leftovers' limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced); -- make the accumulated substitution in the limiting_expn; use the inner workhorse directly leftover_iteration_clauses with:= [iter_op,bv,limiting_expn]; -- the substituted clause will be used in a quantifier end if; end loop; -- once all the clauses of the iterator have been processed, we process the quantified predicate -- this is the existential case, not reversed if leftover_iteration_clauses = [] then -- just return the substituted body as an implication involving all the limiting_clauses [n3,skolemized_in_pred,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); conj := conjoin(limiting_clauses); -- conjoin a collection of clauses return [if limiting_clauses = [] then n3 else ["ast_and",conj,n3] end if,skolemized_here + skolemized_in_pred,substitution_tup]; -- return the said implication else -- just return the substituted body as a quantified implication involving all the limiting_clauses n3 := substitute_in(n3,substitution_map,bound_vars_not_replaced); -- make substitutions in the predicate. Here, only a simple substitution is made n3 := [n1,[iter_tag] + leftover_iteration_clauses,n3]; -- reattach the quantifier and remaining iterators --print("really an existential leftover: ",n3," ",leftover_iteration_clauses); conj := conjoin(limiting_clauses); -- conjoin a collection of clauses return [if limiting_clauses = [] then n3 else ["ast_and",conj,n3] end if,skolemized_here,substitution_tup]; -- return the said implication, noting all the variables that have been skolemized here and in the predicate end if; end if; when "ALL" => -- universal. This is similar to the existential case, but with reversal of the case to skolemize [n1,n2,n3] := tree; -- unpack the parts of the syntax node limiting_clauses := []; -- the limiting_clauses will be conjoined into a final conjunction, which will appear in -- result formula as (clause1 & clause2 & ...) •imp substituted_body leftover_iteration_clauses := []; -- to accumulate iteration_clauses whose bound variable is not replaced iter_tag := n2(1); -- get the list tag for the iterator replacement_stopped := false; -- flag indicating whether replacement was stopped either explicitly or implicitly if bool_sign then -- the sign has not reversed, so this is a true universal. all substitutions will be accepted for [iter_op,bv,limiting_expn] in n2(2..) loop -- process all the clauses of the iterator if substitution_tup /= [] and not replacement_stopped then -- there are still more substitutions available, so make one more limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced); -- make the accumulated substitution in the limiting_expn; use the inner workhorse directly replacement_expression fromb substitution_tup; -- get the next replacement expression to use if replacement_expression = OM then -- replacement is being stopped manually replacement_stopped := true; -- only prior replacements will be used leftover_iteration_clauses with:= [iter_op,bv,limiting_expn]; -- this will not be used, so become a leftover_iteration_clause --print("replacement_stopped: "); else -- note the replacement to be made henceforth substitution_map(bv) := replacement_expression; -- this will replace the bound variable henceforth limiting_clauses with:= [iter_op,replacement_expression,limiting_expn]; -- in the new clause, the bound variable is replaced -- accumulate the substituted limiting_clause, for later use, as explained above end if; else -- there are no more susbstitutions available or replacement has been stopped, -- so the remaining pieces of the iterator are 'leftovers' limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced); -- make the accumulated substitution in the limiting_expn; use the inner workhorse directly leftover_iteration_clauses with:= [iter_op,bv,limiting_expn]; -- the substituted clause will be used in a quantifier end if; end loop; -- once all the clauses of the iterator have been processed, we process the quantified predicate -- this is the universal case, not reversed bound_vars_not_replaced +:= {b: [op,bv,limit] in leftover_iteration_clauses}; -- there may be additional bound variables not being replaced --print("leftover_iteration_clauses: ",leftover_iteration_clauses); if leftover_iteration_clauses = [] then -- just return the substituted body as an implication involving all the limiting_clauses [n3,skolemized_in_pred,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- make substitutions in the predicate conj := conjoin(limiting_clauses); -- conjoin a collection of clauses return [if limiting_clauses = [] then n3 else ["DOT_IMP",conj,n3] end if,skolemized_in_pred,substitution_tup]; -- return the said implication else -- return the substituted body as a quantified implication involving all the limiting_clauses n3:= substitute_in(n3,substitution_map,bound_vars_not_replaced); n3 := [n1,[iter_tag] + leftover_iteration_clauses,n3]; -- re-attach the quantifier and remaining iterators conj := conjoin(limiting_clauses); -- conjoin a collection of clauses return [if limiting_clauses = [] then n3 else ["DOT_IMP",conj,n3] end if,[],substitution_tup]; -- return the said implication. nothing is skolemized end if; else -- this is really an implicit existential, so only constant substitutions will be accepted. These will be -- skolemized skolemized_here := []; -- start collecting variables which are skolemized by this existential for [iter_op,bv,limiting_expn] in n2(2..) loop -- process the clauses of the iterator until the first that gives trouble if substitution_tup /= [] and not replacement_stopped then -- there are still more sustitutions available, so see if we can make one more limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced); -- make the accumulated substitution in the limiting_expn; use the inner workhorse directly replacement_expression fromb substitution_tup; -- get the next replacement expression to use if replacement_expression = OM or not is_string(replacement_expression) then -- replacement is being stopped manually or implicitly replacement_stopped := true; -- only prior replacements will be used leftover_iteration_clauses with:= [iter_op,bv,limiting_expn]; -- this iteration clause is bypassed substitution_tup := [replacement_expression] + substitution_tup; -- return the unused replacement expression else -- skolemization by this existential is possible substitution_map(bv) := replacement_expression; -- this string will replace the bound variable henceforth limiting_clauses with:= [iter_op,replacement_expression,limiting_expn]; -- in the new clause, the bound variable is replaced. -- accumulate the substituted limiting_clause, for later use, as explained above skolemized_here with:= replacement_expression; -- note that the replacement_expression (a string) -- is being defined here end if; else -- there are no more susbstitutions available or replacement has been stopped, -- so the remaining pieces of the iterator are 'leftovers' limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced); -- make the accumulated substitution in the limiting_expn; use the inner workhorse directly leftover_iteration_clauses with:= [iter_op,bv,limiting_expn]; -- the substituted clause will be used in a quantifier end if; end loop; -- once all the clauses of the iterator have been processed, we process the quantified predicate if leftover_iteration_clauses = [] then -- just return the substituted body as an implication involving all the limiting_clauses [n3,skolemized_in_pred,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- make substitutions in the predicate conj := conjoin(limiting_clauses); -- conjoin a collection of clauses return [if limiting_clauses = [] then n3 else ["DOT_IMP",conj,n3] end if,skolemized_here + skolemized_in_pred,substitution_tup]; -- return the said implication else -- just return the substituted body as a quantified implication involving all the limiting_clauses --print("leftover_iteration_clauses: ",leftover_iteration_clauses); n3 := [n1,[iter_tag] + leftover_iteration_clauses,n3]; -- reattach the quantifier and remaining iterators n3 := substitute_in(n3,substitution_map,bound_vars_not_replaced); -- make substitutions in the predicate. Here, only a simple substitution is made conj := conjoin(limiting_clauses); -- conjoin a collection of clauses return [if limiting_clauses = [] then n3 else ["DOT_IMP",conj,n3] end if,skolemized_here,substitution_tup]; -- return the said implication, noting all the variables that have been skolemized here and in the predicate end if; end if; when "in" => -- this can only be processed when the second argument is a setformer if (n31 := n3(1)) /= "ast_genset" and n31 /= "ast_genset_noexp" then -- cannot be dequantified -- just perform a simple substitution, and return the triple -- [substituted_result,nothing_skolemized,remaining_substitution_tup] --print("cannot be dequantified: ",tree," substitution_map: ",substitution_map); return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup]; elseif n31 = "ast_genset" then -- we have a set-former with an expression -- convert it to an existential, and process as such -- here the subnode is of length 4, m2 being the tree for the expr and m3 the iterator [m1,m2,m3,m4] := n3; -- unpack the setformer subnode corresponding_existential := ["ast_exists",m3,["ast_and",["ast_eq",n2,m2],m4]]; return dequantify_in(corresponding_existential,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- continue recursively, treating this as an existential else -- we have a set-former with no expression. -- The membership relation x in {y in u | P(y)} simplifies to (x in u and P(x)), but not here return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup]; end if; when "notin" => -- this is much like 'in', but with a reversal of sign if (n31 := n3(1)) /= "ast_genset" and n31 /= "ast_genset_noexp" then -- cannot be dequantified -- just perform a simple substitution, and return the triple -- [substituted_result,nothing_skolemized,remaining_substitution_tup] return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup]; elseif n31 = "ast_genset" then -- we have a set-former with an expression -- convert it to a related existential, and process as such. we use the 'FORALL ... not ...' form -- here the subnode is of length 4, m2 being the tree for the expr and m3 the iterator [m1,m2,m3,m4] := n3; -- unpack the setformer subnode corresponding_universal := ["ast_forall",m3,["ast_not",["ast_and",["ast_eq",n2,m2],m4]]]; --print("'notin ast_genset' case: ",corresponding_universal); print(unparse(corresponding_universal)); return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- continue recursively, treating this as a universal else -- we have a set-former with no expression. -- The membership relation x notin {y in u | P(y)} simplifies to not(x in u and P(x)), but not here return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup]; end if; --->working dequantify when "incs" => -- set inclusion. we handle this in case the second argument is a setformer by rewriting -- a incs {e(x): x in s | P(x)} as (FORALL x in s | P(x) •imp (e(x) in a)) -- and a incs {x in s | P(x)} as (FORALL x in s | P(x) •imp (x in a)) if (n31 := n3(1)) /= "ast_genset" and n31 /= "ast_genset_noexp" then -- cannot be dequantified -- just perform a simple substitution, and return the triple -- [substituted_result,nothing_skolemized,remaining_substitution_tup] return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup]; elseif n31 = "ast_genset" then -- we have a set-former with an expression; see above -- convert it to a universal, and process as such -- here the subnode is of length 4, m2 being the tree for the expr and m3 the iterator [m1,m2,m3,m4] := n3; -- unpack the setformer subnode corresponding_universal := ["ast_forall",m3,["DOT_IMP",m4,["ast_in",m2,n2]]]; return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- continue recursively, treating this as a universal else -- we have a set-former with no expression. Treat as described above [m1,m2,m3] := n3; -- unpack the setformer subnode the_var := m2(2)(2); -- get the quantified variable corresponding_universal := ["ast_forall",m2,["DOT_IMP",m3,["ast_in",the_var,n2]]]; return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- continue recursively, treating this as a universal end if; when "incin" => -- reversed set inclusion. we handle this in case the first argument is a setformer by rewriting -- {e(x): x in s | P(x)} •incin a as (FORALL x in s | P(x) •imp (e(x) in a)) -- and {x in s | P(x)} •incin a as (FORALL x in s | P(x) •imp (x in a)) if (n21 := n2(1)) /= "ast_genset" and n21 /= "ast_genset_noexp" then -- cannot be dequantified -- just perform a simple substitution, and return the triple -- [substituted_result,nothing_skolemized,remaining_substitution_tup] return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup]; elseif n21 = "ast_genset" then -- we have a set-former with an expression; see above -- convert it to a universal, and process as such -- here the subnode is of length 4, m2 being the tree for the expr and m3 the iterator [m1,m2,m3,m4] := n2; -- unpack the setformer subnode corresponding_universal := ["ast_forall",m3,["DOT_IMP",m4,["ast_in",m2,n3]]]; return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- continue recursively, treating this as a universal else -- we have a set-former with no expression. Treat as described above [m1,m2,m3] := n2; -- unpack the setformer subnode the_var := m2(2)(2); -- get the quantified variable corresponding_universal := ["ast_forall",m2,["DOT_IMP",m3,["ast_in",the_var,n3]]]; return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced); -- continue recursively, treating this as a universal end if; when "()" => -- predicate or function application --print("function application: ",tree); return [tree(1..2) with substitute_in(tree(3),substitution_map,bound_vars_not_replaced),[],substitution_tup]; end case; -- in the remaining cases we just perform a simple substitution, -- and return the triple [substituted_result,nothing_skolemized,remaining_substitution_tup] return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup]; end dequantify_in_trace; procedure conjoin(clauses); -- conjoin a collection of clauses conj := clauses(1); -- start building a conjunction for j in [2..#clauses] loop conj := ["ast_and", conj,clauses(j)]; end loop; -- conjoin the next clause return conj; end conjoin; --->tests -- **************************************************** -- ***************** Test Collection ****************** -- **************************************************** -- procedure test_find_fnc_symbs; -- test of the find_fnc_symbs procedure print("****** TESTS OF FIND_FUNCTION_SYMBOLS PROC ******"); stgs := ["sin(x) + cos(x);", "{sin(x) + cos(x): x in f(y) | P(x,y)};", "{x in f(y) | P(x,y)};", "(EXISTS x in f(y)~[g(y,h(y))] | P(x,y));", "{{x},{{x},{{y},y}}};"]; for stg in stgs loop print(); tree := parze_expr(stg); print(find_fnc_symbs(tree(2))); end loop; end test_find_fnc_symbs; procedure test_dequantify(); -- test of the dequantify procedure print("****** TESTS OF DEQUANTIFY PROC ******"); -- the tuples used for testing consist of a formula to be dequantified, -- followed by a string of tems to be substituted for the quantified variables in the first formula. tups := [["not ((EXISTS x in s | (FORALL y in s | P(x,y))) •imp (FORALL y in s | (EXISTS x in s | P(x,y))));","a;","","b;"], ["(not (((A in s) and (FORALL Y in s | P(A,Y))) •imp ((B in s) •imp (EXISTS X in s | P(X,B)))));","b;","a;"], ["not ((FORALL x in s | (FORALL y in s | P(x,y))) •imp (FORALL y in s | (FORALL x in s | P(x,y))));","","a;","b;"], ["not ((FORALL X in S | (FORALL Y in S | P(X,Y))) •imp ((A in S) •imp ((B in S) •imp P(B,A))));","b;","a;"], -- ["(not (((FORALL Y in s | P(A,Y))) •imp ((EXISTS X in s | P(X,B)))));","b;","a;"], -- ["(FORALL x in u | P(x));","g(c);"], -- ["(EXISTS x in u, y in v(x) | P(x,y)) or (FORALL x in u | R(x));","cc;","","dd;"], -- ["(FORALL x in u, y in v(x) | P(x,y)) or (FORALL x in u | R(x));","H(u);","","G(u);"], -- ["(EXISTS y in u | (FORALL X in S | P(x,y)));","cc;","G(u);"], -- ["(EXISTS y in u | (FORALL X in S | P(x,y)));","cc;"], -- ["(EXISTS y in u | (FORALL X in S | P(x,y))) or (FORALL X in S | Q(x));","G(u);"], -- ["(FORALL X in S | (P(X) •imp (E(X) in A)));","G(u);"], -- ["a incs {e(x,y): x in s,y in t | P(x,y)};","G(u);","H(u);"], -- ["a incs {e(x,y): x in s,y in t | P(x,y)};","G(u);"], -- ["a incs {x in s| P(x)};","G(u);"], -- ["{e(x,y): x in s,y in t | P(x,y)} •incin a;","G(u);","H(u);"], -- ["{e(x,y): x in s,y in t | P(x,y)} •incin a;","G(u);"], -- ["{x in s| P(x)} •incin a;","G(u);"], -- ["(FORALL Y in S | (not (X = E(Y) and P(Y))));","G(u);"], -- ["(EXISTS x in u | P(x));","G(u);"], -- ["(FORALL x in u, y in v | P(x,y));","cc;"], -- ["(FORALL x in u, y in v | P(x,y));","cc;","dd;"], -- ["(FORALL x in u, y in v(x) | P(x,y));","cc;","G(u);"], -- ["(FORALL x in u, y in v(x) | P(x,y));","H(u);","G(u);"], -- ["(FORALL x in u | (EXISTS y in v(x) | P(x,y)));","H(u);","cc;"], -- ["(FORALL x in u | (EXISTS y in v(x) | P(x,y)));","H(u);","G(u);"], -- ["(EXISTS x in u | P(x));","G(u);"], -- ["(EXISTS x in u, y in v | P(x,y));","cc;"], -- ["(EXISTS x in u, y in v | P(x,y));","cc;","dd;"], -- ["(EXISTS x in u, y in v | P(x,y));","cc;","G(u);"], -- ["(EXISTS x in u, y in v | P(x,y));","H(u);","G(u);"], -- ["not (FORALL x in u | P(x));","dd;"], -- ["not (EXISTS x in u | P(x));","G(u);"], -- ["(FORALL x in u | P(x)) and (FORALL x in u | Q(x));","G(u);","H(u);"], -- ["(FORALL x in u | P(x)) or (FORALL x in u | Q(x));","G(u);","H(u);"], -- ["(EXISTS x in u | P(x)) •imp (FORALL x in u | Q(x));","G(u);","H(u);"], -- ["x in {y in s | P(y)};","cc;"], -- ["x notin {y in s | P(y)};","H(u);"], -- ["x in {e(y): y in s | P(y)};","cc;"], -- ["x notin {e(y): y in s | P(y)};","H(u);"], ["(EXISTS x in u | P(x));","cc;"]]; for tup in tups loop print(); tree := parze_expr(tup(1))(2); substitution_tup := [if f = "" then OM else parze_expr(f)(2) end if: f in tup(2..)]; [formula,skolemized,unused] := dequantify(tree,substitution_tup); print("dequantified formula is: ",unparse(formula)); print("variables skolemized are: ",skolemized); print("unused replacements are: ",[unparse(r): r in unused]); end loop; end test_dequantify; procedure test_monotone_infer; -- test of the monotone_infer procedure --->tests2 print("****** TESTS OF NEW MONOTONE INFERENCE PROC ******"); post_monotone("Un,++;Pow,+;#,+;•PLUS,+,+;•TIMES,+,+;Finite,-;Is_map,--;One_1_map,-"); -- note monotonicity properties of builtins forms := ["a + b = b + a;", "(FORALL u in domain(f) | #u in x2) •imp (FORALL u in #domain(f) | #u in x2);", -- "{[x,f(x)]: x in s | x in {c}} = {[x,f(x)]: x in s * {c}};", -- "a * b = b * a;", -- "if true then a + b else c end if = b + a;", -- "Un(a + b) = Un(b + a);", -- "pow(Un(a + b)) = pow(Un(b + a));", -- "#pow(Un(a + b)) = #pow(Un(b + a));", -- "#pow(Un(a + b)) = #pow(b + a);", -- "a + b incs a;", -- "#(a + b) incs #a;", -- "#pow((a + b)) incs #pow(a);", -- "#pow(Un(a + b)) incs #pow(Un(a));", -- "#pow(Un(a + b)) incs #pow(Un(c));", -- "Un(a + b) = Un(a) + Un(b);", -- "Un(a) + Un(b) = Un(a + b);", -- "Un(Un(a + b)) = Un(Un(a)) + Un(Un(b));", -- "Un(Un(a) + Un(b)) = Un(Un(a)) + Un(Un(b));", -- "pow(Un(a + b)) = pow(Un(a)) + pow(Un(b));", -- "{e(x): x in a + b | P(x)} = {e(x): x in b + a | P(x)};", -- "{e(x,x2): x in a + b, x2 in f(x) | P(x,x2)} = {e(y,y2): y in b + a, y2 in f(y) | P(y,y2)};", -- "{e(x): x •incin (a + b) | P(x)} = {e(x): x in pow(b + a) | P(x)};", -- "{e(x): x •incin (a + b) | P(x)} = {e(x): x in pow(b + a)};", -- "{e(x): x •incin (a + b) | true} = {e(x): x in pow(b + a)};", -- "{e(x): x •incin (a * b) | true} = {e(x): x in pow(b * a)};", -- "{x: x •incin (a * b)} = {x in pow(b * a) | true};", -- "{x in pow(b * a) | true} = {x: x •incin (a * b)};", -- "{x in pow(b * a + d * c) | true} = {x: x •incin (a * b + c * d)};", -- "{e(x): x in a | P(x)} + {e(x): x in a | Q(x)} = {e(x): x in a | Q(x) or P(x)};", -- "{e(x): x in a | P(x)} + {e(x): x in b | P(x)} = {e(x): x in a + b | P(x)};", -- "Un(a + b) = c + d;", -- "(EXISTS x in a + b | P(x)) •eq (EXISTS x in b + a | P(x));", -- "((EXISTS x in a | P(x)) or (EXISTS x in b | P(x))) •eq (EXISTS x in b + a | P(x));", -- "((EXISTS x in a | P(x)) or (EXISTS x in a | Q(x))) •eq (EXISTS x in a | P(x) or Q(x));", -- "((FORALL x in a | P(x)) and (FORALL x in a | Q(x))) •eq (FORALL x in a | P(x) and Q(x));", -- "((FORALL x in a | P(x)) and (FORALL x in b | P(x))) •eq (FORALL x in b + a | P(x));", -- "Un(Un(a + b)) = Un(Un(a) + Un(b));", -- "pow(Un(a)) + pow(Un(b)) incs pow(Un(a + b));", -- "{e(x): x in a + b | P(x)} = {ee(x): x in b + a | P(x)};", -- "{g(x) * h(x): x in pow(b * a + d * c) | true} = {h(x) * g(x): x •incin (a * b + c * d)};", -- "{e(x): x •incin (a + b) | P(x)} incs {e(x): x in pow(b) | P(x)};", -- "{e(x): x •incin (a + b) | P(x)} incs {e(x): x in pow(c) | P(x)};", -- "Un((a + b) + c) incs Un(c) + Un(b);", -- "(Un(c) + Un(b)) •incin Un((a + b) + c);", -- "{e(x): x in (a + (b + c)) | P(x)} incs {e(x): x in c | P(x)} + {e(x): x in b | P(x)};", -- "{e(x): x in (a + (b + c)) | P(x)} incs {e(x): x in a | P(x)} + ({e(x): x in b | P(x)} + {e(x): x in c | P(x)});", -- "{e(x): x in (b + (a + c)) | P(x)} incs {e(x): x in c | P(x)} + {e(x): x in b | P(x)};", -- "(a or b) •imp c;", -- "(a and b) •imp c;", -- "(a and b) •imp a;", -- "if (a and b) •imp a then c else d end if •imp c;", -- "if (a and b) •imp a then c else d end if •imp d;", -- "if a = a then c else d end if •imp c;", -- "if a = a then c else d end if •imp d;", -- "(a and b) •imp a;", -- "((a and b) or (c and d)) •imp (a or c);", -- "((a and b) and (c and d)) •imp (a and c);", -- "((not(a and c)) •imp (not((a and b) and (c and d))));", -- "(FORALL x in b + a | P(x)) •imp (FORALL x in a | P(x));", -- "(FORALL x in b + a | P(x) and Q(x)) •imp (FORALL x in a | P(x));", -- "(FORALL x in b + a | P(x)) •imp (FORALL x in a | P(x) or Q(x));", -- "(EXISTS x in a | P(x)) •imp (EXISTS x in b + a | P(x) or Q(x));", -- "(EXISTS x in b + a | P(x) or Q(x)) •imp ((EXISTS x in b | P(x) or Q(x)) or (EXISTS x in a | P(x) or Q(x)));", -- "(EXISTS x in a | P(x) or Q(x)) •imp ((EXISTS x in a | P(x)) or (EXISTS x in a | Q(x)));", -- "((EXISTS x in b | P(x) or Q(x)) or (EXISTS x in a | P(x) or Q(x))) •imp (EXISTS x in b + a | P(x) or Q(x));", -- "((EXISTS x in a | P(x)) or (EXISTS x in a | Q(x))) •imp (EXISTS x in a | P(x) or Q(x));", -- "(FORALL x in b + a | P(x) and Q(x)) •imp ((FORALL x in b | P(x) and Q(x)) and (FORALL x in a | P(x) and Q(x)));", -- "(FORALL x in a | P(x) and Q(x)) •imp ((FORALL x in a | P(x)) and (FORALL x in a | Q(x)));", -- "((FORALL x in b | P(x) and Q(x)) and (FORALL x in a | P(x) and Q(x))) •imp (FORALL x in b + a | P(x) and Q(x));", -- "((FORALL x in a | P(x)) and (FORALL x in a | Q(x))) •imp (FORALL x in a | P(x) and Q(x));", -- "{cdr(u): u in {[x,y],[zz,w]} | car(u) in {x}} = {cdr(u): u in {[x,y]} | car(u) in {x}} + {cdr(u): u in {[zz,w]} | car(u) in {x}};", -- "{e(x,y): x in g, y in (f + ff) | P(x,y)} = {e(x,y): x in g, y in f | P(x,y)} + {e(x,y): x in g, y in ff | P(x,y)};", -- "{if x = a then b elseif x = b then a else x end if: x in s} incs {if x = a then b elseif x = b then a else x end if: x in {a,b,c}};", -- "{E(X,Y): X in G, Y in F | P(X,Y)} = {E(X,Y): X in G, Y in F | P(X,Y)};", -- "({[X,Y]: X in A, Y in C} + {[X,Y]: X in B, Y in C}) = ({[X,Y]: X in A, Y in C} + {[X,Y]: X in B, Y in C});", -- "{[x,y]: x in a, y in c} + {[x,y]: x in b, y in c} = {[x,y]: x in a + b, y in c};", -- "(s - {orden(y): y in o2 + a}) •incin (s - {orden(y): y in o2});", -- "{[[car(u),car(cdr(u))],cdr(cdr(u))]: u in {[x,[y,0]]: x in n, y in m} + {[x,[y,1]]: x in n, y in k}} = {[[car(u),car(cdr(u))],cdr(cdr(u))]: u in {[x,[y,0]]: x in n, y in m}} + {[[car(u),car(cdr(u))],cdr(cdr(u))]: u in {[x,[y,1]]: x in n, y in k}};", -- "{e(u): u in {f(x,y): x in n, y in m} + {f(x,y): x in n, y in k}} = {e(u): u in {f(x,y): x in n, y in m}} + {e(u): u in {f(x,y): x in n, y in k}};", -- "{cdr(u): u in {[x,y]} + {[zz,w]} | car(u) in {x}} = {cdr(u): u in {[x,y]} | car(u) in {x}} + {cdr(u): u in {[zz,w]} | car(u) in {x}};", -- "Finite(a + b) •imp Finite(a);", -- "Finite(#(a + b)) •imp Finite(#a);", -- "Is_map(a + b) •imp Is_map(a);", -- "One_1_map(a + b) •imp One_1_map(a);", "a = a;"]; for form in forms loop print(); -- print("Tree returned: ",monotone_infer(parze_expr(form)(2))); print(unparse(monotone_infer(parze_expr(form)(2)))); end loop; end test_monotone_infer; procedure test_replace_fcn_symbol; -- test of the replace_fcn_symbol procedure quads := [["hsko(s,t)~[s];","H_THRYVAR","U,V","hsko(u,v)~[u];"], ["(h_thryvar(s,t) /= f({g(h_thryvar(y,t),y,s,t): y •incin s | (y /= s) & P(h_thryvar(y,t),y,s,t)},s,t)) & (hsko(s,t)~[s] /= f({g(hsko(y,t)~[y],y,s,t): y •incin s | (y /= s) & P(hsko(y,t)~[y],y,s,t)},s,t));","H_THRYVAR","U,V","hsko(u,v)~[u];"], -- ["pow(Un(a));","ast_pow","X","{u: u •incin x};"], -- ["pow(Un(a));","UN","X","{u: v in x, u in v};"], -- ["Un(Un(a));","UN","X","{u: v in x, u in v};"], -- ["if Un(a) /= 0 then pow(Un(a)) else Un(Un(a)) end if ;","UN","X","{u: v in x, u in v};"], -- ["range(Un(a));","ast_range","X","{cdr(u): u in x};"], -- ["range(Un(range(a)));","ast_range","X","{cdr(u): u in x};"], -- ["{Un(a),Un(Un(a))};","UN","X","{u: v in x, u in v};"], -- ["{Un(a),Un(b)};","UN","X","{u: v in x, u in v};"], -- ["[Un(a),Un(Un(a))];","UN","X","{u: v in x, u in v};"], -- ["{Un(a): a in pow(Un(b)) | Un(Un(a)) = 0};","UN","X","{u: v in x, u in v};"], -- ["{a in pow(Un(b)) | Un(Un(a)) = 0};","UN","X","{u: v in x, u in v};"], -- ["(FORALL a in pow(Un(b)) | Un(Un(a)) = 0);","UN","X","{u: v in x, u in v};"], -- ["(EXISTS a in pow(Un(b)) | Un(Un(a)) = 0) or (FORALL a in pow(Un(b)) | Un(Un(a)) = 0);","UN","X","{u: v in x, u in v};"], -- ["a •MINUS b;","DOT_MINUS","X,Y","#(X - Y);"], -- ["f~[b];","TILDE_","F,X","cdr(arb({y: y in F •ON {X}}));"], -- ["arb({{c},{{c},{{d},d}}}) = arb([c,d]);","ast_enum_tup","X,Y","{{X},{{X},{{Y},Y}}};"], -- ["[c,d];","ast_enum_tup","X,Y","{{X},{{X},{{Y},Y}}};"], -- ["[Un(c),Un(d)];","UN","X","{u: v in x,u in v};"], ["Un(f(Un(a)));","UN","X","{u: v in x,u in v};"]]; for [form,symb,symbargs,symbdef] in quads loop print(); print(unparse(replace_fcn_symbol(parze_expr(form)(2),symb,breakup(symbargs,","),parze_expr(symbdef)(2)))); end loop; end test_replace_fcn_symbol; procedure replace_fcn_symbol(expn,symbol,symbvars,symbdef); -- at each occurrence of a symbol in expn, finds the arguments of symbol, -- and substitutes them in symbdef for the indicated free variables of symbdef -- replacing the symbol occurrence by this substituted form -- but if symbvars = OM, in which case the definition should a simple string, occurrences of -- 'symbol' are replaced by occurrences of 'symbdef' if is_string(expn) then return if expn = symbol then symbdef else expn end if; end if; -- conditionally replace variables found at bottom level --print("replace_fcn_symbol: ",expn); [n1,n2,n3,n4] := expn; -- otherwise unpack top level of tree case n1 when "ast_of" => -- function application arglist := [if j = 1 then arg else replace_fcn_symbol(arg,symbol,symbvars,symbdef) end if: arg = n3(j)]; -- make substitutions within them if n2 = symbol then -- we have occurrence of a significant symbol --print("
replace_fcn_symbol: symbol is: ",symbol," symbvars: ",symbvars?"OM"," symbol definition is: ",unicode_unparse(symbdef)," replacement takes place in expression: ",unicode_unparse(expn)," node tag ",expn(1)," opname = symbol",expn(2) = symbol,"
"); --print("
now testing symbvars: ",symbvars = OM," ",symbvars?"UNDEfined"); if symbvars = OM then -- just replace 'symbol' by 'symbdef' and keep the same argument list --print("
returning substituted: ",unicode_unparse([n1,symbdef,arglist])); return [n1,symbdef,arglist]; end if; if n3 = OM or #symbvars /= #(n3(2..)) then --print("[n1,n2,n3,n4]: ",[n1,n2,n3,n4]," ",symbvars); -- mismatch between number of args and number of parameters supplied mismatched_args := true; -- keep record of the offense mismatched_symbvars := symbvars; mismatched_expn := unparse(expn); return expn; -- do no substitutions end if; replacement_map := {[symbvar,arglist(j + 1)?symbvar]: symbvar = symbvars(j)}; -- map each definition parameter into the argument which replaces it return substitute(symbdef,replacement_map); -- substitute these replacements within the symbol definition and return the result end if; return [n1,n2,arglist]; -- otherwise just return the symbol with the substituted arguments when "ast_genset" => -- setformer subst_n2 := replace_fcn_symbol(n2,symbol,symbvars,symbdef); subst_iter := [if j = 1 then iter else replace_fcn_symbol(iter,symbol,symbvars,symbdef) end if: iter = n3(j)]; subst_cond := if n4 = "st_null" then n4 else replace_fcn_symbol(n4,symbol,symbvars,symbdef) end if; return [n1,subst_n2,subst_iter,subst_cond]; when "ast_genset_no_expr","ast_forall","ast_exists" => -- setformer, no expression, quantifier subst_iter := [if j = 1 then iter else replace_fcn_symbol(iter,symbol,symbvars,symbdef) end if: iter = n2(j)]; subst_cond := if n3 = "st_null" then n4 else replace_fcn_symbol(n3,symbol,symbvars,symbdef) end if; return [n1,subst_iter,subst_cond]; -- -- when "ast_forall" => -- universal quantifier --print(expn); -- when "ast_exists" => -- existential quantifier --print(expn); when "ast_enum_set" => -- enumerated set return [n1] + [replace_fcn_symbol(elt,symbol,symbvars,symbdef): elt in expn(2..)]; when "ast_enum_tup" => -- enumerated tuple arglist := [replace_fcn_symbol(elt,symbol,symbvars,symbdef): elt in expn(2..)]; if case_change(n1,"lu") = case_change(symbol,"lu") then -- if the tuple iself is being expanded then replacement_map := {[symbvar,arglist(j)?symbvar]: symbvar = symbvars(j)}; -- map each definition parameter into the argument which replaces it return substitute(symbdef,replacement_map); -- substitute these replacements within the symbol definition and return the result end if; return [n1] + arglist; -- otherwise just return the tuple arguments, as a tuple when "#","ast_pow","ast_range","ast_domain","ast_arb" => -- builtin monadics substarg := replace_fcn_symbol(n2,symbol,symbvars,symbdef); if n1 = symbol then -- we have occurrence of a significant symbol replacement_map := {[symbvar,substarg?symbvar]: symbvar = symbvars(j)}; -- map each definition parameter into the argument which replaces it return substitute(symbdef,replacement_map); -- substitute these replacements within the symbol definition and return the result end if; return [n1,substarg]; -- otherwise just return the symbol with the substituted arguments when "TILDE_" => -- function application (has special syntax) --print("expn: ",expn); substarg := replace_fcn_symbol(n2,symbol,symbvars,symbdef); substarg2 := replace_fcn_symbol(n3(2),symbol,symbvars,symbdef); -- throw away nonstandard square brackets --print("replacement_map: ",replacement_map," result: ",unparse(substitute(symbdef,replacement_map))," substarg: ",unparse(substarg)," substarg2: ",unparse(substarg2)," symbdef: ",unparse(symbdef)); if n1 /= symbol then return ["TILDE_",substarg,["ast_enum_tup",substarg2]]; end if; return ["ast_of", "CDR", ["ast_list", ["ast_arb", ["DOT_ON", substarg, ["ast_enum_set", substarg2]]]]]; -- combine these replacements as a tilde and return the result otherwise => if n1 = symbol then -- defined binary operator substarg := replace_fcn_symbol(n2,symbol,symbvars,symbdef); substarg2 :=if n3 /= OM then replace_fcn_symbol(n3,symbol,symbvars,symbdef) else OM end if; if n1 = symbol then -- we have occurrence of a significant symbol replacement_map := {[symbvar,if j = 1 then substarg else substarg2 end if?symbvar]: symbvar = symbvars(j)}; -- map each definition parameter into the argument which replaces it return substitute(symbdef,replacement_map); -- substitute these replacements within the symbol definition and return the result end if; return [n1,substarg,substarg2]; -- otherwise just return the symbol with the substituted arguments else -- some other operator substarg :=if n2 /= OM then replace_fcn_symbol(n2,symbol,symbvars,symbdef) else OM end if; substarg2 :=if n3 /= OM then replace_fcn_symbol(n3,symbol,symbvars,symbdef) else OM end if; substarg3 :=if n4 /= OM then replace_fcn_symbol(n4,symbol,symbvars,symbdef) else OM end if; return [n1,substarg,substarg2,substarg3]; end if; end case; end replace_fcn_symbol; procedure find_setformers_and_quants(tree); -- finds the setformer and quantifier nodes in a tree, and returns them -- as a list var setformers_and_quants := []; -- the list to be returned find_setformers_and_quants_in(tree); -- call the recursive workhorse return setformers_and_quants; -- return the map produced procedure find_setformers_and_quants_in(tree); -- internal recursive workhorse if is_string(tree) then return; end if; --print("find_setformers_and_quants_in::: ",unparse(tree)); [n1,n2,n3] := tree; -- break node into operands and operator: generally infix (but not always) if (ah := abbreviated_headers(n1)) in {"{}","{/}","EX","ALL"} then setformers_and_quants with:= tree; end if; case ah when "if" => find_setformers_and_quants_in(n2); find_setformers_and_quants_in(n3); find_setformers_and_quants_in(tree(4)); -- if expression when "and","or","==","=",":=","incs","incin","imp","+","*","-" ,"in","notin","/=","/==","@" => -- various binaries find_setformers_and_quants_in(n2); find_setformers_and_quants_in(n3); when "{-}" => for nj in tree(2..) loop find_setformers_and_quants_in(nj); end loop; -- enumerated set when "[-]" => find_setformers_and_quants_in(n2); if n3 /= OM then find_setformers_and_quants_in(n3); end if; -- ordered pair, or singleton for tilde pplication when "domain","range","not","arb" => find_setformers_and_quants_in(n2); -- built-in monadics when "EX","ALL","{/}" => -- quant or setformer, no expr; look for sets in the iterator list bounds and in the condition find_setformers_and_quants_in(n2); find_setformers_and_quants_in(n3); when "{}" => -- setformer; look for sets in the lead expression, the iterator list bounds and in the condition find_setformers_and_quants_in(n2); find_setformers_and_quants_in(n3); find_setformers_and_quants_in(tree(4)); when "[]" => -- list, e.g. of arguments; search for sets in the iterator bounds for iter in tree(2..) | not (is_string(iter) or is_string(bound := iter(3))) loop find_setformers_and_quants_in(bound); end loop; when "()" => -- function and predicate application; just search all the arguments for nj in tree(3)(2..) loop find_setformers_and_quants_in(nj); end loop; otherwise => for nj in tree(2..) loop find_setformers_and_quants_in(nj); end loop; -- other operators; process all arguments end case; end find_setformers_and_quants_in; end find_setformers_and_quants; -- ********************************************************************************* -- ********************************* Obsolete code ********************************* -- ********************************************************************************* procedure monotone_inference(node1,node2); -- calculates conditions for value defined by node 1 to include value defined by node 2 -- We begin by standardizing the two nodes so as to bring them into the closest feasible correspondence. -- Then we descend the two trees in parallel, looking for differences in the parse trees, and collecting bound variables. -- A difference can be found either at a common functional or predicate node. A dummy variable is assigned to each difference, -- and we return the set of quintuples [subtree1,subtree2,bound_variables,dummy_variable,is_pred] and the common reduced formula in which -- all differences have been replaced by the generated dummy variables. This common formula is then surveyed for monotone dependencies -- using 'blob_to_monotone'. Then the following deductions are possible: (a) if there is just one difference under no bound variables, -- and the expression is additive, then we can deduce an inequality between sums. (b) if there is any differnce at a position depending -- in a mixed way on the variable inserted at that position, then no deduction is possible. (c) Otherwise we can deduce either -- of two inclusions, from corrresponnding inclusions for the differences, with reversals in the difference positions which are decreasing_kind. difference_quintuples := {}; -- set of difference quintuples monot_var_ctr := 0; -- counter used for generation of variables -- node1 := standardize_bound_vars(node1); node2 := standardize_bound_vars(node2); -- standardize the bound variables in both formulae res := monotone_inference_in(node1,node2,{},true); -- workhorse; start at predicate level with no bound variables print("difference_quintuples: ",difference_quintuples); return res; end monotone_inference; procedure monotone_inference_in(tree1,tree2,bound_vars_with_ranges,is_pred); -- workhorse for 'monotone_inference' --print("monotone_inference_in: ",unparse(tree1)," ",unparse(tree2)," bound_vars_with_ranges = ",bound_vars_with_ranges," is_pred = ",is_pred); if is_string(tree1) or is_string(tree2) then -- a variable confronts a subexpression if tree1 = tree2 then return tree1; end if; -- no difference in bottom-level leaves; just return difference_quintuples with := [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred]; return newvar; -- return the representing variable end if; -- otherwise the nodes differ in their principal operator; collect the difference [n1_1,n2_1,n3_1] := tree1; [n1_2,n2_2,n3_2] := tree2; -- get the likely parts of the two clauses if n1_1 /= n1_2 then -- the nodes are not of the same kind, so return a difference variable difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred]; return newvar; -- return the representing variable end if; -- otherwise two subexpressions confront each other -- othewise the nodes are of the same kind, so go on to look for differences in their arguments case (ah := abbreviated_headers(n1_1)) when "and","or","==","/==","imp","null" => -- boolean operations -- ordinary operators with a fixed number of arguments; look for differences in their arguments res_1 := monotone_inference_in(n2_1,n2_2,bound_vars_with_ranges,true); -- find subpart differences res_2 := monotone_inference_in(n3_1,n3_2,bound_vars_with_ranges,true); -- subparts are predicates return [n1_1,res_1,res_2]; -- return the condensed tree, having found differences when "+","-","{.}","in","notin","=","/=","incs","incin","*","[-]" => -- ordinary operators with a fixed number of arguments; look for differences in their arguments -- ast_enum_tup should be ordered pair only; singleton for application operator is handled elsewhere --print("[n1_1,n2_1,n3_1]: ",[n1_1,n2_1,n3_1]," ",[n1_2,n2_2,n3_2]); res_1 := monotone_inference_in(n2_1,n2_2,bound_vars_with_ranges,false); -- find subpart differences res_2 := monotone_inference_in(n3_1,n3_2,bound_vars_with_ranges,false); -- subparts are terms return [n1_1,res_1,res_2]; -- return the condensed tree, having found differences when "->" => -- "->" is the functional application operator "TILDE_" res_1 := monotone_inference_in(n2_1,n2_2,bound_vars_with_ranges,false); -- subparts are expressions res_2 := monotone_inference_in(n3_1(2),n3_2(2),bound_vars_with_ranges,false); -- syntax is ["TILDE_", "F", ["ast_enum_tup", "X"]] return [n1_1,res_1,["ast_enum_tup",res_2]]; -- return the condensed tree, having found differences when "not" => res_1 := monotone_inference_in(n2_1,n2_2,bound_vars_with_ranges,true); -- subparts are predicates return [n1_1,res_1]; -- return the condensed tree, having found differences when "[]" => -- ast_list print("****** shouldnt happen - monotone_inference_in: ",ah); when "{-}" => -- enumerated sets. here we try to improve the agreement by sorting the elements if #(args1 := tree1(2..)) /= #(args2 := tree2(2..)) then -- the nodes differ in their number of arguments; treat as different difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred]; return newvar; -- return the representing variable end if; -- otherwise blob the elements and sort them to bring into the order most likely to agree args1_with_blobs := [[blob_to_string(a1,[],name_ctr),a1]: a1 in args1]; -- we leave out the bound variables, since these will be common to both sets args2_with_blobs := [[blob_to_string(a2,[],name_ctr),a2]: a2 in args2]; args1_sorted := [y: [x,y] in merge_sort(args1_with_blobs)]; args2_sorted := [y: [x,y] in merge_sort(args2_with_blobs)]; --print("args1_with_blobs: ",args1_sorted," ",args2_sorted);stop; -- look for differences in their arguments if args1_sorted /= args2_sorted then difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred]; return newvar; -- return the representing variable end if; return tree1; -- otherise we have fond identity, so return the common tree when "()" => -- this is the case of functional and predicate application; the second variable is a reserved symbol, not a set --print("function trees: ",tree1," ",tree2); if tree1 /= tree2 then -- the nodes differ difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred]; return newvar; -- return the representing variable end if; -- otherwise blob the elements and sort them to bring into the order most likely to agree return tree1; -- otherise we have fond identity, so return the common tree when "{}" => -- setformer with expression; here there is a fourth argument, namely the predicate (this may be "ast_null", represetnting 'true') -- here we are comparing two setformers having structures like {e1(x,y,z): x in s1, y in t1(x), z in w1(x,y) | A(x,y,z)}. -- if the iterator lists which appear are of the same length and have corresponding structures throughout, and have identical expressions, -- then we look for differences in the restrictions of the bound variables, and also for differences in the predicates -- otherwise we treat the two setformers as different body_1 := n2_1; body_2 := n2_2; -- get the two expressions being accumulated list_of_iters_1 := orig_list_of_iters_1 := n3_1(2..); list_of_iters_2 := orig_list_of_iters_2 := n3_2(2..); -- get the two lists of iterators -- the iter_list syntax is exemplified by ["ast_iter_list", ["ast_in", "X", "A"], ["ast_incs", "Y", "B"],...] cond_1 := tree1(4); cond_2 := tree2(4); -- get the two conditions if cond_1 = ["ast_null"] then cond_1 := "TRUE"; end if; -- replace empty conditions with "TRUE" if cond_2 = ["ast_null"] then cond_2 := "TRUE"; end if; if body_1 /= body_2 then -- iterator expressions differ; so treat as diferent difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred]; return newvar; -- return the representing variable end if; if (cl := #list_of_iters_1) /= #list_of_iters_2 then -- the iterators are of different lengths, so treat s different difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred]; return newvar; -- return the representing variable end if; -- otherise check that the iterators are all of the same types -- if not verify_equality_in(body_1,body_2,bound_vars_with_ranges + list_of_iters_1,false) then -- the bodies are not identical -- return false; -- verification by examination of subparts succeeds -- end if; -- otherwise we must check to see if the iterator lists are equivalent -- -- if not verify_equality_in(cond_1,cond_2,bound_vars_with_ranges + list_of_iters_1,true) then -- the conditions are not identical -- return false; -- verification by examination of subparts succeeds -- end if; -- otherwise we must check to see if the iterator lists are equivalent -- -- succeeds := true; -- see if the following loop succeeds ----print("body_1,body_2:: ",body_1," ",body_2," ",list_of_iters_1," ",list_of_iters_2); -- for k in [1..cl] loop -- [-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); -- get the restriction sets ----print("restr_set_1,restr_set_2:: ",restr_set_1," ",restr_set_2," ",bound_vars_with_ranges + list_of_iters_1(1..k - 1)," "); -- if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then -- succeeds := false; exit; -- end if; -- -- end loop; -- -- if succeeds then return true; end if; -- otherwise not all of the restriction sets are eqivalent, so we -- -- go on to see if identity can be verified 'directly' in some way -- -- for j in [1..cl] loop -- -- if j = cl then -- there are no suffixed qualifiers -- -- required_implication := ["ast_forall",["ast_iter_list"] + orig_list_of_iters_1,["DOT_EQ",cond_1,cond_2]]; -- required_identity := ["ast_forall",["ast_iter_list"] + orig_list_of_iters_1,["ast_eq",body_1,body_2]]; -- -- if not check_in_context(required_implication,bound_vars_with_ranges) then continue; end if; -- if not check_in_context(required_identity,bound_vars_with_ranges) then continue; end if; -- -- succeeds := true; -- see if the following loop succeeds -- for k in [1..cl] loop -- -- [-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); -- get the restriction sets -- -- if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then -- succeeds := false; exit; -- end if; -- -- end loop; -- -- if succeeds then return true; end if; -- otherwise keep looing to try to find a verification -- -- else -- there are suffixed qualifiers; use these in setformers -- -- set_1 := ["ast_genset",body_1,["ast_iter_list"] + orig_list_of_iters_1(j + 1..),cond_1]; -- set_2 := ["ast_genset",body_2,["ast_iter_list"] + orig_list_of_iters_2(j + 1..),cond_2]; -- required_identity := ["ast_forall",["ast_iter_list"] + orig_list_of_iters_1(1..j),["ast_eq",set_1,set_2]]; -- -- if not check_in_context(required_identity,bound_vars_with_ranges) then continue; end if; -- -- succeeds := true; -- see if the following loop succeeds -- for k in [1..j] loop -- -- [-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); -- get the restriction sets -- -- if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then -- succeeds := false; exit; -- end if; -- -- end loop; -- -- if succeeds then return true; end if; -- otherwise keep looping to try to find a verification -- -- end if; -- -- end loop; -- -- return false; -- if the iterator sequences don't agree, we give up in this case, allowing proof to proceed more manually, -- -- end if; -- -- when "{/}" => -- setformer without expression -- -- see comment at start of preceding case -- -- list_of_iters_1 := n2_1(2..); list_of_iters_2 := n2_2(2..); -- get the two lists of iterators -- cond_1 := n3_1; cond_2 := n3_2; -- get the two conditions -- [cl,list_of_iters_1,list_of_iters_2,cond_1,cond_2] := common_iter_len(list_of_iters_1,list_of_iters_2,cond_1,cond_2); -- -- if cl = #list_of_iters_1 and cl = #list_of_iters_2 then -- the iterators agree out to their full lengths; look for differences in bodies -- -- if not verify_equality_in(cond_1,cond_2,bound_vars_with_ranges + list_of_iters_1,true) then -- the conditions are not identical -- return false; -- verification by examination of subparts succeeds -- end if; -- otherwise we must check to see if the iterator lists are equivalent -- ----print("cond_1,cond_2:: ",cond_1," ",cond_2," ",list_of_iters_1," ",list_of_iters_2); -- [-,-,restr_set_1] := list_of_iters_1(1); [-,-,restr_set_2] := list_of_iters_2(1); -- get the restriction sets -- -- if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges,false) then -- return false; -- end if; -- -- end if; -- -- return true; -- if all tests are passed, we return true -- -- when "ALL","EX" => -- universal and existential quantifiers -- -- lead_quantifier := if ah = "ALL" then "ast_forall" else "ast_exists" end if; -- -- [list_of_iters_1,body_1] := flatten_universal(tree1); [list_of_iters_2,body_2] := flatten_universal(tree2); -- -- find the full flattened lists of prefixed universal quantifiers in the two trees -- -- now find the iterator portions which are of the same types. That is, the operators "ast_in" or "DOT_INCIN" -- -- must be the same, and for the "ast_in" case, either both ranges or none must be OM -- -- [cl,list_of_iters_1,list_of_iters_2,body_1,body_2] := common_iter_len(list_of_iters_1,list_of_iters_2,body_1,body_2); -- -- find the length of the iterator parts which are common -- -- if cl = #list_of_iters_1 and cl = #list_of_iters_2 then -- the iterators agree out to their full lengths; look for differences in bodies -- -- if not verify_equality_in(body_1,body_2,bound_vars_with_ranges + list_of_iters_1,true) then -- the bodies are not identical -- return false; -- verification by examination of subparts succeeds -- end if; -- otherwise we must check to see if the iterator lists are equivalent -- -- succeeds := true; -- see if the following loop succeeds ----print("body_1,body_2:: ",body_1," ",body_2," ",list_of_iters_1," ",list_of_iters_2); -- for k in [1..cl] loop -- [-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); -- get the restriction sets ----print("restr_set_1,restr_set_2:: ",restr_set_1," ",restr_set_2,`" ",bound_vars_with_ranges + list_of_iters_1(1..k - 1)," "); -- if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then -- succeeds := false; exit; -- end if; -- -- end loop; -- -- if succeeds then return true; end if; -- otherwise not all of the restriction sets are eqivalent, so we -- -- go on to see if identity can be verified 'directly' in some way -- -- elseif cl = #list_of_iters_1 then -- the full first iterator agrees with a prefix of the second iterator -- -- remaining_iters := list_of_iters_2(cl + 1..); -- find the remaining iters in the first group -- body_2 := ["ast_forall",["ast_iter_list"] + remaining_iters,body_2]; -- restore the remaining universals to the second clause -- -- elseif cl = #list_of_iters_2 then -- the full second iterator agrees with a prefix of the second iterator; insist on an identity -- -- remaining_iters := list_of_iters_1(cl + 1..); -- find the remaining iters in the second group -- body_1 := ["ast_forall",["ast_iter_list"] + remaining_iters,body_1]; -- restore the remaining universals to the first clause -- -- else -- only portions of the iterators agree; insist on an identity of the remaining parts -- -- remaining_iters1 := list_of_iters_1(cl + 1..); -- find the remaining iters in the first group -- body_1 := ["ast_forall",["ast_iter_list"] + remaining_iters1,body_1]; -- restore the remaining universals to the first clause -- -- remaining_iters2 := list_of_iters_2(cl + 1..); -- find the remaining iters in the second group -- body_2 := ["ast_forall",["ast_iter_list"] + remaining_iters2,body_2]; -- restore the remaining universals to the second clause -- -- end if; -- -- here we attempt 'direct', rather than 'subpart' verifiction, by trying identities -- -- prefixed by the full list of quantifiers and by any of its initial subparts, any one of which might be relevant ----print("try direct verification: cl = ",cl," lead_quantifier = ",lead_quantifier," list_of_iters_1 = ",list_of_iters_1," list_of_iters_2 = ",list_of_iters_2," body_1 = ",body_1," body_2 = ",body_2); -- for j in [cl + 1,cl..1] loop -- try clauses with varying numbers of prefixed quantifiers -- -- qbody_1 := if j > cl then body_1 else [lead_quantifier,["ast_iter_list"] + list_of_iters_1(j..),body_1] end if; -- -- prefix the bodies with varying numbers of quantifiers -- qbody_2 := if j > cl then body_2 else [lead_quantifier,["ast_iter_list"] + list_of_iters_2(j..),body_2] end if; -- -- required_equivalence := ["DOT_EQ",qbody_1,qbody_2]; -- set up, and then quantify, the required equivalence -- if j > 1 then required_equivalence := ["ast_forall",["ast_iter_list"] + list_of_iters_1(1..j - 1),required_equivalence]; end if; -- ----print("required_equivalence: ",j," ",unparse(required_equivalence)); -- if not check_in_context(required_equivalence,bound_vars_with_ranges) then continue; end if; -- -- since the equivalence, quantified using the list of quantifiers drawn from the first formula, fails. -- -- otherwise we must verify that the two lists of restriction sets are equivalent. -- -- This can be done recursively, since the restriction sets are syntacticallly 'smaller' than the -- -- expressions in which thy appear -- -- succeeds := true; -- see if the following loop succeeds -- -- for k in [1..j - 1] loop -- check the restriction sets in the prefixed iterators -- [-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); -- get the restriction sets -- -- if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then -- succeeds := false; exit; -- end if; -- ---- req_ident := ["ast_eq",restr_set_1,restr_set_2]; -- form the body of the required identity ---- required_equivalence := ["ast_and",required_equivalence,build_quantified_version(req_ident,list_of_iters_1(1..k - 1))]; ---- -- add the necessary quantifiers and conjoin to the required equivalence -- end loop; -- -- if succeeds then return true; end if; -- since a quantified equivalence and all the restriction set equivalences have been verified -- -- end loop; -- -- return false; -- if none of the quantified clauses verifies, we fail at this level -- -- when "itr","Etr" => -- iterators; here the iterators must be of the same kinds, and if one is involves a bounding set -- -- so must the other. the bound variable names may differ; if they do we generate a common new name for both, -- -- and sustitute it uniformly down both trees. -- -- find the common minimum of the iterator lists lengths -- if #(args1 := tree1(2..)) /= #(args2 := tree2(2..)) then -- the nodes differ in their number of arguments; treat as different -- -- diffs_vars_ranges with:= [bound_vars_with_ranges,tree1,tree2]; -- return; -- -- end if; -- -- for sn = args1(j) loop verify_equality_in(sn,args2(j),bound_vars_with_ranges,is_pred); end loop; otherwise => print("shouldn't happen verify_equality_in: ",ah," ",node); -- shouldn't happen end case; end monotone_inference_in; procedure test_monotone_inference; -- test of the monotone_inference procedure print("****** TESTS OF BASIC MONOTONE INFERENCE PROC ******"); -- print(); print("test_monotone_inference: ",parze_expr("{e(x): x incs a | P(x)};")); -- print(); print("test_monotone_inference forall: ",parze_expr("(FORALL x incs a | P(x));")); pairs := [["x incs a;","(x + y) incs a;"], ["x incs a or (not (y incs b));","(x + y) incs a or (not ((z + w) incs b));"]]; for [hypothesis,conclusion] in pairs loop print(); tree1 := parze_expr(hypothesis); tree2 := parze_expr(conclusion); print(monotone_inference(tree1(2),tree2(2))); end loop; end test_monotone_inference; end logic_syntax_analysis_pak2; -- **************************************************** -- **************** Proof by structure **************** -- **************************************************** -- Proof by structure uses a simple auxiliary language of structure -- descriptors to keep track of the top structural levels of sets appearing -- in scenario proofs. Any special set defined in a scenario, for example -- Za, the set of all non-negative integers, or Re, the set of all reals, can be used as -- a primary structure symbol in this language. This descriptor attaches to -- all members of the set, i.e. any integer has the descriptor Za. A -- significant but less basic example is Si, the set of all -- signed integers, which does not occur in our present scenario but could -- easily be defined. Structure descriptors need not be confined to sets, -- but can also designate classes, like the class Ord of all ordinals, the -- class Fin of all finite sets, the class Infin of all infinite sets, -- and the class U of all sets, etc. -- Given any symbols S,S_1,S_2,... representing structures we can then -- form: -- (i) {S}: describes a set all of whose elements have the descriptor S. -- For example,the set Za has the descriptor {Za}; the set of sets of -- integers has the descriptor {{Za}}. -- (ii) [S_1,S_2]: describes a pair whose components have respectively the -- descriptors S_1 and S_2. -- These constructions can be compounded. For example -- (e.1) {[Za,Za]} describes a set of integer pairs (and so applies to Si, -- the set of signed integers -- (e.2) {[Za,U]} describes a map from integers to elements of any kind, i.e -- describe any finite or infinite sequence. -- A given set can have several descriptors. For example, a finite sequence -- of signed integers has the descriptors {[Za,Si]} and Fin. Since Si itself -- has the descriptor {[Za,Za]}, a sequence of signed integers also has the -- descriptor {[Za,[Za,Za]]}, which in any given situation we may wish either -- to use of ignore. Infinite sequences of signed integers have the -- descriptors {[Za,Si]} and Infin. Real numbers in Cantor's representation -- are equivalence classes of such sequences, and therefore have the -- descriptors {{[Za,Si]}} and {Infin}. -- A mechanism within the verifier should track the descriptors of -- variables and expressions appearing in proofs whenever possible. For -- example, a variable x known to satisfy a clause 'x in Z' has the -- descriptor Za, a variable known to satisfy 'x in Si' has the descriptors -- Si and [Za,Za]. -- Setformers and other basic constructors operate in a known way on the -- structure descriptors introduced above. Suppose, for example, that s is -- a set known to have some descriptor {D}, and that e(x) is an expression -- having the free variable x which is known to map elements having the -- descriptor D into elements having the descriptor D'. Then -- {e(x): x in s | P} -- has the descriptor {D'}, while -- {[x,e(y)]: x in s, y in s | P} -- has the descriptor {[D,D']}. -- When a set s is known to have a descriptor {D}, any element x for which -- 'x in s' has been proved is known to have the descriptor D. If D is a -- primitive descriptor representing a known set, this will give us the -- assertion 'x in D', for example 'x in Z', which may be needed as an -- auxiliary hypothesis for the application of some theorem. Similarly any -- set s having the descriptor {[Za,Za]} is known to satisfy Is_map(s), and -- also -- (FORALL x in s | car(x) in Za & cdr(x) in Za) -- Conclusions of this kind can often result automatically. This is a -- principal use for our system of structure descriptors. -- Many other basic set-theoretic operations have known effects on -- descriptors. These often follow from the definitions of the operators in -- question. For example: -- (1) if s has the descriptor {D}, then so does every one of its subsets, -- and pow(s) has the descriptor {{D}}. -- (2) if s has the descriptor {{D}}, then Un(s) has the descriptor {D}. -- Note hat this follows automatically from the definition {x: y in s, x in -- y} of Un(s), since the bound variable y in the iterator has the -- descriptor {D}, so each of the x has the descriptor D, and the set as a -- whole has the descriptor {D}. -- (3) if s_1 and s_2 both have a descriptor {D}, then so does s_1 + s_2. -- (4) if s_1 and s_2 both have the descriptor Fin, then so does s_1 + s_2. -- (5) if s_1 and s_2 have descriptors {D_1} and {D_2} respectively, then -- s_1 * s_2 has both descriptors {D_1} and {D_2}. Even if s_2 has no -- descriptor, s_1 * s_2 and s_1 - s_2 has the descriptor {D_1}, as does -- any set s for which an assertion s •incin s_1 has been proved. -- (6) if s_1 has the descriptor Fin, so do s_1 * s_2 and s_1 - s_2, as -- does any set s for which an assertion s •incin s_1 has been proved. -- (7) if s_1 and s_2 have the descriptor Fin, so does any setformer {e: x -- in s_1, y in s_2 | P},or any setformer {e: x in s_1 | P} -- (8) #s always has the descriptor Card. Since the class of cardinals has -- the descriptor {Ord}, #s also has the descriptor Ord, as does any x -- known to be a cardinal. If s has the descriptor Fin, then #s has the -- descriptor Za. Since Za itself has the descriptor {Fin}, #s also has the -- descriptor Fin. -- (9) if has the descriptor {D}, then any setformer like {x: x •incin s| -- p} is known to have the descriptor {{D}}; this result obviously -- generalizes. -- (10) if sets s and t have the descriptors {D} and {D'} respectively, -- then their Cartesian product s •PROD t has the descriptor {[D,D']}, If s -- and t both have the descriptor Fin, so does s •PROD t. -- (11) if s and t have descriptors {[D,D']} and {[D',D'']} respectively, -- then s@t has the descriptor {[D,D'']}. If s and t both have the -- descriptor Fin, so does s@t. -- (12) if s and t have descriptors D, D' respectively, then [s,t] has the -- descriptor [D,D']. If u has the descriptor [D,D'], then car(u) has the -- descriptor D and cdr(u) has the descriptor D'. -- (12) if F has the descriptor {[D,D']}, then inv(F) has the descriptor -- {[D',D]}, and F •ON s has the descriptor {[D',D]}. if F has the -- descriptor Fin, then inv(F) and F •ON s both have the descriptor Fin -- also. -- There may be useful extensions of these ideas to single-valued and -- one-one maps; also to topologcal situations, spaces of continuous -- functions, etc. -- Note that some of the conclusions derived manually in the present -- scenarios can result automatically by use of structure descriptors. For -- example, the cardinal sum is defined as -- #({[x,0]: x in s_1} + {[x,1]: x in s_2}), -- making it obvious that the sum of two integers is an integer. Similarly, -- the definition of cardinal product, namely -- #{[x,y]: x in s_1,y in s_2} -- makes it apparent that the product of two integers is an integer. Since -- the difference of integers is defined by #(n - m), it also follows -- immediately that the difference of integers is an integer. -- Ordinals also have the descriptors {Ord}, since any element of an -- ordinal is an ordinal. Any Un(s) of a set having the descriptor {Ord} -- has the descriptor Ord. It may be worth carrying the set next(Z) as an -- additional descriptor. If this s done, Un(s) will be known to have the -- descriptor next(Za) is s has the descriptor {Za}, and so to have the -- descriptor Za (i.e. to be an integer) if there is another s' having the -- descriptor next(Z) for which -- a statement s in s' is available. -- In many cases a definition or theorem appearing in a scenario will -- characterize the action on structure descriptors of one or more of the -- function symbols appearing in it. The examples given just above -- illustrate this. Such facts combined with the other rules given above -- extend the verifier's ability to tack the structures of objects appearing -- in proofs. For example, if s, t and u are sets known to have the -- descriptor {Za}, then -- {(x •TIMES y) •PLUS z: x in s, y in t, z in u | P} -- is also known to have the descriptor {Za}. -- The theory of summation yields the fact that Sum(f) has the descriptor D -- if f has the descriptors {[d,D]} and Fin, and if the 'PLUZ' operator -- appearing in the summation can be shown to map pairs of objects having -- the descriptor D into objects having this same descriptor. Thus, for -- example, the sum or product of any setformer like -- {[[x,y,z],(x •TIMES y) •PLUS z]: x in s, y in t, z in u | P} -- is also known to be an integer if s, t and u are sets known to have the -- descriptor {Za}. -- The structure definition mechanism explained above carries over in a -- useful way to recursively defined functions (in our set-theoretic -- context, these can be functions defined by transfinite induction.) To -- show why such extension is possible, we first need to note that the -- system of descriptors extends readily to function symbols, since these -- are very close semantically to sets of pairs. For example, the -- descriptor {[D_1,D_2]} can be ascribed to any one-parameter function -- symbol which maps each object having the descriptor D_1 into an object -- having the descriptor D_2. Similarly, the descriptor {[[D_1,D_2],D_3]} -- can be ascribed to any two-parameter function symbol which yields an -- object having the descriptor D_3 whenever its two parameters have the -- respective descriptors D_1 and D_2. (For example, the integer addition -- operator •PLUS has the descriptor {[[Za,Za],Za]}, but also the descriptors -- {[U,U],Ord]} since it always produces an ordinal, and the descriptor -- {[[Fin,Fin],Za]}, since it produces an integer for any two finite -- inputs.) In the three-parameter case, {[[[D_1,D_2],D_3],D_4]} can be -- ascribed to any three-parameter function symbol which yields an object -- having the descriptor D_4 whenever its three parameters have the -- respective descriptors D_1, D_2 and D_3. -- Using these descriptors, we can state the rule for function application -- as follows: If a one-parameter function symbol f has the descriptor -- {[D_1,D_2]}, and x has the descriptor D_1, then f(x) has the descriptor -- D_2. Similarly, if a two-parameter function symbol f has the descriptor -- {[[D_1,D_2],D_3]}, and its two arguments x_1,x_2 has the descriptor -- D_1,D_2, then f(x_1,x_2) has the descriptor D_3. We leave it to the -- reader to formulate the rules for more than two arguments. -- Function compounding acts in an obvious way on descriptors, for example -- if f has the descriptor {[D_1,D_2]} and g has the descriptor -- {[D_2,D_3]}, then g(f(.)) has the descriptor {[D_1,D_3]}. Rules like -- this make it obvious why -- #({[x,0]: x in s_1} + {[x,1]: x in s_2}), -- yields an integer for every pair of integer arguments: the functional -- expression {[x,0]: x in s_1} has the descriptor {[Fin,Fin]} simply -- because it is a setformer with s_1 as its only free variable, and -- likewise for {[x,1]: x in s_2}. Since the union operator '+' has the -- descriptor {[[Fin,Fin],Fin]}, it follows immediately that {[x,0]: x in -- s_1} + {[x,1]: x in s_2} has the descriptor {[[Fin,Fin],Fin]} also. -- Since #has the descriptors {[Fin,Fin]} and{[U,Ord]}, #({[x,0]: x in s_1} -- + {[x,1]: x in s_2}) has the descriptors {[[Za,Za],Fin]} and -- {[[Za,Za],Ord]}, and therefore {[[Za,Za],Za]}. Much the same argument applies -- to the integer product. -- Next consider a transfinite recursive definition of one of the general -- types we allow,namely -- f(s,t) := d({g(f(x,h(s,t)),s,t): x in s | P(x,f(x,h(s,t)),s,t)},s,t), -- where as before we assume that the functions d, g, and h have been -- defined prior to the occurrence of the recursive definition shown. In -- working with this definition we will want to establish that f has some -- descriptor {[[D_1,D_2],D_3]}, i.e. that it yields an element having -- descriptor D_3 for any input arguments with descriptors D_1,D_2 -- respectively. This conclusion will be valid under the following -- circumstances: we need to know that there exits descriptor D' such that -- (a) h has the descriptor {[[D_1,D_2],D_2]}; -- (b) g has the descriptor {[[[D_3,D_1],D_2],D']}; -- (c) d has the descriptor {[[[{D'},D_1],D_2],D_3]}. -- Then in the ground case of the transfinite recursive definition f({},t) -- has the value d({},s,t), and so must produce an element with the -- descriptor D_3. In the remaining case it follows inductively (given that -- s and t have the respective descriptors D_1,D_2) that f(x,h(s,t)) has -- the descriptor D_3 for every x in s, so that g(f(x,h(s,t)),s,t) has the -- descriptor D', and so -- (*) {g(f(x,h(s,t)),s,t): x in s | P(x,f(x,h(s,t)),s,t)} -- has the descriptor {D'}. Therefore the right side of the recursive -- definition seen above has the descriptor D_3, and it follows inductively -- that f has the descriptor {[[D_1,D_2],D_3]}. -- If s has the descriptor Fin, then the set (*) will have this descriptor -- also, and so if d has the descriptor {[[[Fin,Fin],D_2],Fin]}, f will -- have the descriptor {[[Fin,D_2],Fin]}. O the other hand, if d is an -- operator like arb, and so has the descriptor {[{D_1},D_2]} (where the -- null set must have the descriptor D_2), then g must have the descriptor -- {[[[Fin,Fin],D_2],Fin]}, and s the descriptor {Fin},for f(s,t) to have -- the descriptor Fin. In this case f has once again the descriptor -- {[[Fin,D_2],Fin]}. -- -- ***************************************************************** -- ************ routines realizing 'Proof by Structure' ************ -- ***************************************************************** package proof_by_structure; var vars_to_descriptors,debug_extract,debug_conj_tree; -- exposed for debugging purposes only -- main interface procedures procedure extract_relevant_descriptors(conj_tree); -- extract additional descriptors given tree of a conjunction procedure expression_descriptor(expn_stg,vars_to_descriptors); -- secondary interface procedures (exposed for debugging purposes only and to be invoked by test programs) procedure get_assertions_from_descriptors(vars_to_descriptors); -- convert descriptors to set membership assertions procedure descriptor_action_of_memb(descriptor_set); -- result of choosing an unknown member procedure descriptor_action_of_subset(descriptor_set); -- result of choosing an unknown subset procedure descriptor_action_of_pow(descriptor_set); procedure descriptor_action_of_Un(descriptor_set); procedure descriptor_action_of_union(descriptor_set1,descriptor_set2); procedure descriptor_action_of_intersection(descriptor_set1,descriptor_set2); procedure descriptor_action_of_difference(descriptor_set1,descriptor_set2); procedure descriptor_action_of_range(descriptor_set); procedure descriptor_action_of_domain(descriptor_set); procedure descriptor_action_of_arb(descriptor_set); procedure descriptor_action_of_pair(descriptor_set1,descriptor_set2); procedure descriptor_action_of_car(descriptor_set); procedure descriptor_action_of_cdr(descriptor_set); procedure descriptor_action_of_count(descriptor_set); procedure descriptor_action_of_next(descriptor_set); procedure descriptor_action_of_cartprod(descriptor_set1,descriptor_set2); procedure descriptor_action_of_funcprod(descriptor_set1,descriptor_set2); procedure descriptor_action_of_func_inv(descriptor_set); -- procedure descriptor_action_of_func_ident(descriptor_set); -- UNUSED --procedure tests; -- SYSTEMATIC TESTS FOR ABOVE PROCEDURES end proof_by_structure; package body proof_by_structure; use parser,string_utility_pak,logic_syntax_analysis_pak,logic_syntax_analysis_pak2; var first_proof_by_structure := true; var basic_sets := {"ZA","HFIN","RA","RE","SI","CM"}; var basic_preds := {"ORD","CARD","FIN","INFIN","COUNTABLE","NONNULL","SVM","IS_MAP","ONE_1_MAP"}; var basic_descriptors; -- union of basic_sets with basic_preds -- "COUNTABLE" MEANS 'FINITE OR ENUMERABLY INFINITE'; "HFIN" MEANS 'HEREDITARILY FINITE' -- COMPOUND DESCRIPTORS ARE CONSTRUCTED FROM THESE BASIC DESCRIPTORS BY PAIRING AND SINGLETON FORMATION var descriptors_of_basic := { -- MAPPING FROM BASIC DESCRIPTORS TO COMPOUND DESCRIPTORS GIVING THEIR PROPERTIES ["ZA",{{"ORD"},{"FIN"},{"HFIN"},"COUNTABLE","ORD","CARD","FIN","HFIN",{"CARD"},{"ZA"},{"COUNTABLE"}}], ["ORD",{{"ORD"}}], ["CARD",{"ORD",{"ORD"}}], ["HFIN",{{"HFIN"},{"FIN"},{"COUNTABLE"},"FIN","COUNTABLE"}], ["FIN",{"COUNTABLE"}], -- ["SI",{["ZA","ZA"]}], -- overly conventional ["RASEQ",{{["ZA","RA"]},"NONNULL","INFIN","IS_MAP","SVM","COUNTABLE"}], ["CM",{["RE","RE"]}], ["IS_MAP",{{["OM","OM"]}}], ["SVM",{{["OM","OM"]},"IS_MAP"}], ["ONE_1_MAP",{{["OM","OM"]},"SVM","IS_MAP"}], ["OM",{{"OM"}}] -- IS THIS NEEDED?? }; var m_descriptors_of_basic := { -- SIMILAR TO THE PRECEDING ONE, HANDLES MULTIPLE INHERITANCE [{"FIN",{"HFIN"}}, {"HFIN"}], [{"FIN","CARD"}, {"ZA"}], [{"FIN","ORD"}, {"ZA"}] }; -- *********** ASSOCIATION OF ACTIONS WITH SYNTAX-TREE NODES *********** var unary_op_actions := {["ast_arb",DESCRIPTOR_ACTION_OF_ARB], ["ast_range",DESCRIPTOR_ACTION_OF_RANGE],["ast_domain",DESCRIPTOR_ACTION_OF_DOMAIN], ["ast_nelt",DESCRIPTOR_ACTION_OF_COUNT],["ast_pow",DESCRIPTOR_ACTION_OF_POW]}; var binary_op_actions := {["ast_add",DESCRIPTOR_ACTION_OF_UNION],["ast_mult",DESCRIPTOR_ACTION_OF_INTERSECTION], ["DOT_PROD",DESCRIPTOR_ACTION_OF_CARTPROD], ["TILDE_",DESCRIPTOR_ACTION_OF_FUNC_APP],["AT_",DESCRIPTOR_ACTION_OF_FUNCPROD], ["ast_sub",DESCRIPTOR_ACTION_OF_DIFFERENCE],["ast_enum_tup",DESCRIPTOR_ACTION_OF_PAIR]}; var function_actions_and_numpars := {["UN",[DESCRIPTOR_ACTION_OF_UN,1]],["NEXT",[DESCRIPTOR_ACTION_OF_NEXT,1]], ["INV",[DESCRIPTOR_ACTION_OF_FUNC_INV,1]], ["CAR",[DESCRIPTOR_ACTION_OF_CAR,1]], ["CDR",[DESCRIPTOR_ACTION_OF_CDR,1]]}; var const_properties := { -- MAPS CONSTANTS TO COLLECTIONS OF SETS TO WHICH THEY ARE KNOWN TO BELONG ["0",{"CARD","FIN","COUNTABLE","IS_MAP","SVM","ONE_1_MAP"}], ["1",{"CARD","FIN","COUNTABLE","NONNULL"}], ["2",{"CARD","FIN","COUNTABLE","NONNULL"}], ["3",{"CARD","FIN","COUNTABLE","NONNULL"}], ["ZA",{"CARD","ORD","INFIN","COUNTABLE","NONNULL"}], ["RA",{"INFIN","COUNTABLE","NONNULL"}], ["RE",{"INFIN","NONNULL"}], ["HFIN",{"INFIN","COUNTABLE","NONNULL"}], ["CM",{{["RE","RE"]},"INFIN","NONNULL"}], ["SI",{"INFIN","NONNULL"}], -- ONLY A FEW OF THE CONSTANTS WHICH FOLLOW ARE DESCRIBED AS BEING NONNULL, ALTHOUGH THEY ALL ARE ["S_0",{"SI"}], ["S_1",{"SI"}], ["RA_0",{"RA"}], ["RA_1",{"RA"}], ["R_0",{"RE"}], ["R_1",{"RE"}], ["C_0",{"CM",["RE","RE"]}], ["C_1",{"CM",["RE","RE"]}], ["RASEQ", {{{["ZA","RA"]},"IS_MAP","SVM","COUNTABLE"},"NONNULL","INFIN"}], ["RACAUCHY",{{"RASEQ",{["ZA","RA"]},"IS_MAP","SVM","COUNTABLE"},"NONNULL","INFIN"}], ["RESEQ", {{{["ZA","RE"]},"IS_MAP","SVM","COUNTABLE"},"NONNULL","INFIN"}], ["RECAUCHY",{{"RESEQ",{["ZA","RE"]},"IS_MAP","SVM","COUNTABLE"},"NONNULL","INFIN"}], ["RA0SEQ",{"RASEQ",{["ZA","RA"]},"NONNULL","INFIN","IS_MAP","SVM","COUNTABLE"}], ["RA1SEQ",{"RASEQ",{["ZA","RA"]},"IS_MAP","SVM","NONNULL","INFIN","COUNTABLE"}], ["RE0SEQ",{"RESEQ",{["ZA","RE"]},"NONNULL","INFIN","IS_MAP","SVM","COUNTABLE"}], ["RE1SEQ",{"RESEQ",{["ZA","RE"]},"IS_MAP","SVM","NONNULL","INFIN","COUNTABLE"}] }; var unary_closed_on := { -- MAPS UNARY OPERATORS AND FUNCTIONS TO COLLECTIONS OF SETS ON WHICH THEY ARE KNOWN TO BE CLOSED ["S_REV",{"SI"}], ["RA_REV",{"RA"}], ["RA_ABS",{"RA"}], ["R_REV",{"RE"}], ["ABS",{"RE"}], ["C_REV",{"CM"}], ["INV",{"HFIN"}], ["RAS_REV",{{["ZA","RA"]}}], ["RAS_ABS",{{["ZA","RA"]}}], ["RES_REV",{{["ZA","RE"]}}], ["RES_ABS",{{["ZA","RE"]}}] }; var binary_closed_on := { -- MAPS BINARY OPERATORS AND FUNCTIONS TO COLLECTIONS OF SETS ON WHICH THEY ARE KNOWN TO BE CLOSED ["ast_add",{"CARD","ZA","ORD"}], ["ast_mult",{"CARD","ZA","ORD"}], ["DOT_PLUS",{"CARD","ZA"}], ["DOT_TIMES",{"CARD","ZA"}], -- NEEDED?? ["DOT_MINUS",{"CARD","ZA"}], ["DOT_OVER",{"ZA"}], ["DOT_S_PLUS",{"SI"}], ["DOT_S_TIMES",{"SI"}], ["DOT_S_MINUS",{"SI"}], ["DOT_RA_PLUS",{"RA"}], ["DOT_RA_TIMES",{"RA"}], ["DOT_RA_MINUS",{"RA"}], ["DOT_R_PLUS",{"RE"}], ["DOT_R_TIMES",{"RE"}], ["DOT_R_MINUS",{"RE"}], ["DOT_C_PLUS",{"CM"}], ["DOT_C_TIMES",{"CM"}], ["DOT_C_MINUS",{"CM"}], ["DOT_RAS_PLUS",{"RASEQ"}], ["DOT_RAS_TIMES",{"RASEQ"}], ["DOT_RAS_MINUS",{"RASEQ"}], ["DOT_RES_PLUS",{{["ZA","RE"]}}], ["DOT_RES_TIMES",{{["ZA","RE"]}}], ["DOT_RES_MINUS",{{["ZA","RE"]}}], ["DOT_PROD",{"NONNULL","FIN","COUNTABLE"}], ["AT_",{"FIN","HFIN","COUNTABLE","SVM","ONE_1_MAP"}] }; var finitely_additive_descriptors := { -- BASIC DESCRIPTORS KNOWN TO BE FINITELY ADDITIVE "ZA", "ORD", "FIN", "HFIN", "COUNTABLE", "CARD", "IS_MAP", {"ZA"} }; var fully_additive_descriptors := { -- BASIC DESCRIPTORS KNOWN TO BE UNCONDITIONALLY ADDITIVE "ORD", "IS_MAP", {"ZA"}}; var quasi_additive_descriptors := { -- BASIC DESCRIPTORS KNOWN TO BE UNCONDITIONALLY ADDITIVE (IF THE OVERALL ARGUMENT IS NONNULL) "INFIN","NONNULL"}; var inherited_descriptors := { -- BASIC DESCRIPTORS KNOWN TO BE INHERITED BY SUBSETS "FIN","HFIN","COUNTABLE","IS_MAP","SVM","ONE_1_MAP"}; var transitive_descriptors := { -- BASIC DESCRIPTORS KNOWN TO BE INHERITED BY MEMBERS "ZA","HFIN","ORD"}; procedure init_proof_by_structure(); --print("first_proof_by_structure", first_proof_by_structure); if first_proof_by_structure then first_proof_by_structure := false; basic_sets +:= domain descriptors_of_basic - basic_preds; basic_descriptors := (basic_sets + basic_preds) with "OM"; for k in ["0","1","2","3"] loop const_properties(k) := const_properties(k) + transitive_descriptors; end loop; for x in domain(const_properties) * basic_descriptors loop const_properties(x) := extended_descriptors3(const_properties(x) with {x}); end loop; --print("const_properties: ", const_properties); m_descriptors_of_basic := {[m, mm + descriptors_of_basic(arb(mm))]: mm = m_descriptors_of_basic(m)}; --print("m_descriptors_of_basic: ", m_descriptors_of_basic); end if; end init_proof_by_structure; procedure expression_descriptor(expn_stg,vars_to_descriptors); -- Calculates result descriptor set given an expression in the form of string (to be internally parsed into a tree) -- and the descriptors applicable to its free variables. -- This is the main routine of the the proof_by_structure system. We are concerned here with expressions of two -- principal kinds, simple expressions and setformer expressions. -- Simple expressions are processed recursively, descriptors being attached to all their nodes from bottom to top -- in accordance with the expressions found at each node. -- Conditional expressions of the form 'if c1 then e1 elseif c2 then e2.. end if' are treated as intersections of -- their 'e' parts; set-theoretic expressions have the form {e(x,y,..): x in s1, y in s2 | C } etc. -- We collect relevant clauses from the condition part C, and then calculate descriptors for all of the bounding sets -- s1, s2,... This gives us descriptors for their members x,y,.., which are then used to calculate -- a descriptor set D for e(x,y,..). The setformer then gets the descriptor {D}, to which Fin and Countable -- are attached if all the s1, s2,... have these descriptors, and NonNull is attached if all the sj are NonNull -- and the condition C is missing. tree := parse_expr(expn_stg + ";")(2); -- get the parse tree of the expression init_proof_by_structure(); return expression_descriptor_in(tree,vars_to_descriptors); -- call the recursive workhorse -- this will return the set of descriptors which attach to the top-level expression end expression_descriptor; procedure expression_descriptor_in(tree,vars_to_descriptors); -- recursive workhorse for 'expression_descriptor' (debugging wrapper) res := expression_descriptor_inn(tree,vars_to_descriptors); --print("expression_descriptor_in: ",tree," vars_to_descriptors: ",vars_to_descriptors," res: ",res); return if res = {} then {"OM"} elseif res /= {"OM"} then res less "OM" else res end if; end expression_descriptor_in; procedure expression_descriptor_inn(tree,vars_to_descriptors); -- recursive workhorse for 'expression_descriptor' -- returns the set of known descriptors of the top node of a tree --print("expression_descriptor_inn: ",tree,"\n",vars_to_descriptors); -- this routine also exploits known closure properties of unary and binary operators and functions of several parameters. -- Whenever such an operator or function is encountered, we find the set on which it is closed. If this appears in the -- descriptors of both arguments (or one argument in the case of unaries) it is transmitted to the result if is_string(tree) then return (vars_to_descriptors(tree)?{}) + (const_properties(tree)?{}); end if; -- if simple variable or constant, then return its given or known descriptor buffer_set := vars_to_descriptors(unparse(tree)) ? {}; [n1,n2,n3] := tree; -- otherwise decompose the tree at its top level, allowing for two arguments -- [n1,n2,n3] is [op,arg1,arg2] -- we check first for descriptors available because of general transitive closure properties, -- and return these if there are any if n1 = "TILDE_" then if #n3 /= 2 then buffer_set with:= "OM"; end if; n3 := n3(2); end if; -- if (closure_sets := unary_closed_on(n1)) /= OM then -- this is a non-built-in operator closed on some basic set -- arg_descs := expression_descriptor_in(n2,vars_to_descriptors); -- get the descriptors of the operator argument -- ok_descs := closure_sets * arg_descs; -- if ok_descs /= {} then buffer_set +:= ok_descs; end if; -- if transitivity generates a useful result, return it -- end if; if (closure_sets := binary_closed_on(n1)) /= OM then -- this is a non-built-in binary operator closed on some basic set arg_descs1 := expression_descriptor_in(n2,vars_to_descriptors); -- get the descriptors of the operator argument arg_descs2 := expression_descriptor_in(n3,vars_to_descriptors); -- get the descriptors of the operator argument ok_descs := closure_sets * arg_descs1 * arg_descs2; --print("binary_closed_on(n1): ",n1," ",closure_sets," ",arg_descs1," ",arg_descs2," ok_descs: ",ok_descs); if ok_descs /= {} then buffer_set +:= ok_descs; end if; -- if transitivity generates a useful result, return it end if; if n1 = "ast_of" and (closure_sets := unary_closed_on(n2)) /= OM then -- unary function case; -- these are non-built-in; abs is special since it is an operator arg_descs := expression_descriptor_in(n3(2),vars_to_descriptors); ok_descs := closure_sets * arg_descs; -- see if any of the closure sets is available as an arg descriptor --print("closure_sets: ",closure_sets," ",n3(2)," arg_descs: ",arg_descs); if ok_descs /= {} then buffer_set +:= ok_descs; end if; -- if transitivity generates a useful result, return it end if; -- Note: the following 'actions' are found in the library of procedures given at the beginning of this package action := unary_op_actions(n1)?binary_op_actions(n1)?if n1 = "ast_of" then (fanp := (function_actions_and_numpars(n2))?[])(1) end if; -- get the action associated with the function at this node, if any --print("expression_descriptor_in: ",tree," ",action," ",descriptor_action_of_intersection); if n1 notin {"ast_enum_set","ast_genset","ast_if_expr"} and action = OM then buffer_set with:= "OM"; end if; -- if there is none, we know nothing, so return the descriptor 'generic set' case n1 -- handle the various possible cases separately when "ast_arb","ast_range","ast_domain","ast_nelt","ast_pow" => -- unary operators argdescs := expression_descriptor_in(n2,vars_to_descriptors); -- get the descriptors of the argument expression --print("unary operator: ",n1," ",n2," ",argdescs," vars_to_descriptors: ",vars_to_descriptors); buffer_set +:= action(argdescs); -- apply the action relevant at this node when "ast_add","ast_mult","ast_sub","ast_enum_tup","DOT_PROD","TILDE_","AT_" => -- binary operators if n1 = "ast_enum_tup" and #tree /= 3 then buffer_set with:= "OM"; end if; argdescs1 := expression_descriptor_in(n2,vars_to_descriptors); -- get the descriptors of the argument expression argdescs2 := expression_descriptor_in(n3,vars_to_descriptors); -- get the descriptors of the argument expression --print("binary operator: ",n1," ",n2," ",n3," ",argdescs1," ",argdescs2); buffer_set +:= action(argdescs1,argdescs2); -- apply the action relevant at this node when "ast_of" => -- function application arglist := n3(2..); -- get the list of argument expressions of the function application argdescs1 := expression_descriptor_in(arglist(1),vars_to_descriptors); -- get the descriptors of the argument expressions if (np := fanp(2)?0) > 1 then argdescs2 := expression_descriptor_in(arglist(2),vars_to_descriptors); end if; if np > 2 then argdescs3 := expression_descriptor_in(arglist(3),vars_to_descriptors); end if; --print("np: ",np," ",action," ",descriptor_action_of_Un); if np = 1 then buffer_set +:= action(argdescs1); end if; if np = 2 then buffer_set +:= action(argdescs1,argdescs2); end if; if np = 3 then buffer_set +:= action(argdescs1,argdescs2,argdescs3); end if; -- other cases can obviously be added when "ast_enum_set" => -- enumerated sets: find the common descriptors of all the elements descs := expression_descriptor_in(n2,vars_to_descriptors); -- the members are the tree elements after n1 --print("ast_enum_set: ",descs," ",n2); descs := descs */[expression_descriptor_in(memb,vars_to_descriptors): memb = tree(j) | j > 2]; buffer_set +:= {{d}: d in descs} + {"FIN","NONNULL"} + -- the result is of course finite and nonempty if (forall tree_j = tree(j) | j = 1 or (exists d in expression_descriptor_in(tree_j,vars_to_descriptors) | is_pair(d))) then {"IS_MAP"} else {} end if; -- We are checking that there exists at least one pair d among the descriptors -- of each enumerated element, to allow for sets of the type -- {[x,y], a}, where a has a pair as descriptor. However, its efficiency -- can be improved, as expression_descriptor_in gets computed one more time. -- The following extension to the treatment of maps would be unsound: -- -- if "IS_MAP" in buffer_set then -- -- is_svm := true; -- -- map_check := {}; -- -- for j in [2..#tree] loop -- -- if is_tuple(p := tree(j)) and (p(1) = "ast_enum_tup") and (#p = 3) and (map_check(p(2)) = OM) then -- -- map_check(p(2)) := p(3); -- else -- is_svm := false; -- end if; -- end loop; -- -- if (is_svm) then -- -- buffer_set with:= "SVM"; -- -- if (#domain(map_check) = #range(map_check)) then buffer_set with:= "ONE_1_MAP"; end if; -- end if; -- end if; when "ast_genset" => -- setformer; see comment above -- a sample template, for {e(x,y): x in s, y in t | P(x,y)}, is -- ["ast_genset", tree_of_e(x,y), ["ast_iter_list", ["ast_in", "X", "S"], ["ast_in", "Y", "T"]], tree_of_P(x,y)] -- if the condition is void, we have instead -- ["ast_genset", tree_of_e(x,y), ["ast_iter_list", ["ast_in", "X", "S"], ["ast_in", "Y", "T"]], ["ast_null"]] lc1 := (limiting_clauses := n3(2..))(1); -- the limiting clauses of the setformer bound_var_descs := {}; -- these will be collected as we go along in the limiting clauses restriction_set_descs := []; -- we also collect the descriptors of the restriction sets themselves -- get the descriptor of the first limiting set restriction_set_descs with:= (descs_ls1 := expression_descriptor_in(lc1(3),vars_to_descriptors)); --print("lc1(3): ",lc1(3)," ",vars_to_descriptors," restriction_set_descs: ",restriction_set_descs); bound_var_descs(lc1(2)) := if lc1(1) = "ast_in" then descriptor_action_of_memb(descs_ls1) elseif lc1(1) = "DOT_INCIN" then descriptor_action_of_subset(descs_ls1) else {} end if; -- allow for inclusion-form iterators -- progressing from left to right, get the descriptors of the other limiting sets, for j in [2..#limiting_clauses] loop lcj := limiting_clauses(j); -- the limiting clauses of the setformer -- get the descriptor of the jth limiting set restriction_set_descs with:= (descs_lsj := expression_descriptor_in(lcj(3),vars_to_descriptors + bound_var_descs)); -- meanwhile assigning descriptors to the bound variables as they are encountered bound_var_descs(lcj(2)) := if lcj(1) = "ast_in" then descriptor_action_of_memb(descs_lsj) elseif lcj(1) = "DOT_INCIN" then descriptor_action_of_subset(descs_lsj) else {} end if; -- allow for inclusion-form iterators end loop; -- recursively calculate the descriptor of the lead expression vars_to_descriptors_save := vars_to_descriptors; -- save, in case some of the bound variables have the same name as some of the free variables for [v,descs] in bound_var_descs loop vars_to_descriptors(v) := descs; end loop; descs_lead := expression_descriptor_in(n2,vars_to_descriptors); --print(" descs_lead: ",descs_lead," vars_to_descriptors: ",vars_to_descriptors," n2: ",n2); vars_to_descriptors := vars_to_descriptors_save; -- restore, so as not to affect the external environment descs_lead := {{x}: x in descs_lead}; -- form the descriptor for a set of elements of this kind -- n1 is "ast_genset" -- n2 is of the form ["ast_enum_tup","x",tree_of_e(x)] -- n3 is of the form ["ast_iter_list",["ast_in","x","s"]] -- or of the equivalent form in which "ast_in" is replaced by "DOT_INCIN" if n2(1) = "ast_enum_tup" then lhss := {x(2): x = n3(i) | i > 1 and (x(1) = "ast_in" or x(1) = "DOT_INCIN")}; -- variables bound by iterators if (#lhss = #n3 - 1) -- viz., each iterator binds a distinct variable and if #lhss = 1 then n2(2) = arb(lhss) else is_tuple(n22 := n2(2)) and n22(1) = "ast_enum_tup" and #n22 = 3 and {n22(2),n22(3)} = lhss end if and all_conss(n2(3)) = lhss then descs_lead with:= "ONE_1_MAP"; end if; if ("ONE_1_MAP" in descs_lead) or (is_string(n2(2)) and -- we check that we have a pair [x,e(x)], where x is indeed a variable n3(1) = "ast_iter_list" and -- we check that we indeed have a list of iterators #n3 < 3 and -- we check that we have only one iterator and no condition P(x) ( (iter_type := n3(2)(1)) = "ast_in" or iter_type = "DOT_INCIN" )) then descs_lead with:= "SVM"; end if; descs_lead with:= "IS_MAP"; end if; --print("restriction_set_descs: ",restriction_set_descs); -- if all of the limiting sets are known to be finite, the result is finite if (forall de in restriction_set_descs | "FIN" in de) then descs_lead with:= "FIN"; end if; -- the setformer is countable if every restriction set is either finite or countable and a membership restriction if (forall de = restriction_set_descs(j) | ("COUNTABLE" in de or "FIN" in de) and (not("FIN" notin de and limiting_clauses(j)(1) = "DOT_INCIN"))) then descs_lead with:= "COUNTABLE"; end if; -- if all of the limiting sets are known to be NonNull and there is no condition the result is NonNull if (forall de = restriction_set_descs(j) | "NONNULL" in de) and tree(4) = ["ast_null"] then descs_lead with:= "NONNULL"; end if; -- if all of the limiting sets are known to be NonNull and there is no condition and one is infinite the result is Infinite if (forall de = restriction_set_descs(j) | ("NONNULL" in de or "INFIN" in de)) and (exists de = restriction_set_descs(j) | "INFIN" in de) and tree(4) = ["ast_null"] and all_conss(n2) = {x(2): x = n3(i) | i > 1 and (x(1) = "ast_in" or x(1) = "DOT_INCIN")} then descs_lead with:= "INFIN"; end if; buffer_set +:= descs_lead; -- return the calculated descriptors when "ast_if_expr" => -- conditional expression; find the common descriptors of both branches -- template is ["ast_if_expr", "A", "B", ["ast_if_expr", "C", "D", "E"]] argdescs1 := expression_descriptor_in(n3,vars_to_descriptors); -- get the descriptors of the first branch argdescs2 := expression_descriptor_in(tree(4),vars_to_descriptors); -- get the descriptors of the second branch --print("ast_if_expr: ",argdescs1," ",argdescs2); buffer_set +:= argdescs1 * argdescs2; -- return those descriptors that are common to both branches end case; return buffer_set; end expression_descriptor_inn; procedure all_conss(tree); -- test a tree for being all cons operators, and return the set of its variables return if is_string(tree) then {tree} elseif is_tuple(tree) and tree(1) = "ast_enum_tup" and #tree = 3 then -- if not all cons operators then return OM if (left := all_conss(tree(2))) = OM or (right := all_conss(tree(3))) = OM then OM else left + right end if else OM end if; end all_conss; procedure extract_relevant_descriptors(conj_tree); -- extract relevant descriptors given tree of a conjunction -- this involves information concerning membership, equality, and inclusion; also particular predicates -- it looks for Ref clauses of various forms directly expressible as descriptors, and collects these descriptors into a set which is returned. -- the clauses which can be handled in this way, and their translations, are x in Za, x in Re, Card(x), Ord(x), and in the other elementary sets, -- which translate into Za, Re, Card, Ord, etc.; x •incin Za etc., which translate into -- {Za}, {Re}, {Card}, {Ord}, etc. Finite(x) and Countable(x), which become Fin and Countable; not Finite(x) which becomes Infin; -- and x /= 0 which becomes NonNull. This extraction is iterated twice to handle cases like 'x in n and n in Za', and also handles cases like -- 'x /= 0 and y incs x' and 'Finite(x) and x incs y'. We also handle Svm and one_1_map. -- note that this routine works with variables only, not with subexpressions, so in some cases local variables will need to be defined in -- proofs and properties stated for these variables. init_proof_by_structure(); debug_extract := [memb_conjs,inc_conjs,equality_conjs] := extract_relevant_conjuncts(debug_conj_tree := conj_tree); -- walk the tree, collecting the relevant top-level conjuncts. This adds non-nullity assertions whenever memberships are found. -- dummy inclusions like [x,"FIN"] are used to represent the predicates Fin, Svm, Is_map, and one_1_map -- dummy inclusions like ["Nonull",x] are used to represent the predicates 'x /= 0' and 'not Finite(x)' -- Note the use of partially lowercase forms, which will distinguish these from actual scenario clauses which resemble them -- an attempt is made to identify the range and domain of variables for which Is_map(f) is asserted -- equalities with simple variables on one side are treated in a special way by calculating descriptors for their right-hand side -- and propagating them to the left-hand variable. This makes it possible to identify some setformers that give rise -- to mappings, single-valued mappings, and 1-1 mappings, or to subsets of known sets. vars_to_descriptors := {[v,w] in memb_conjs | w in basic_descriptors} + {[v,{w}]: [v,w] in inc_conjs | w in basic_descriptors}; -- preliminary conversion into map from vars to descriptors, as multivalued map --print("\nmemb_conjs before loop: ",memb_conjs); print("inc_conjs before loop: ",inc_conjs); print("equality_conjs before loop: ",equality_conjs); --print("vars_to_descriptors before loop: ",vars_to_descriptors); -- now we use a bit of transitive closure: if a in b is available and b incin basic_descriptor -- is present, we collect a in basic_descriptor; if a incin b is available and b incin basic_descriptor -- is present, we collect a incin basic_descriptor; if a in Za is available we collect a incin Za, and likewise -- for ordinals and cardinals. This process is continued as long as we are finding more -- primitives like Is_map, Svm, and Fin are treated a bit specially because of their relationship to inclusion, -- as is Infin. something_changed := true; -- force entry to loop debug_count := 0; while something_changed loop -- this propagation loop iterates as long as new attributes are being found -- for the variables which it encounters. something_changed := false; -- but maybe something will change in the body of the loop -- set inclusions are used to propagate all inheritable descriptors from their right-hand side to their -- left, and to propagate all membership relationship involving their left-hand sides to their right. if (debug_count +:= 1) > 10 then exit; end if; -- limit to at most 10 iterations newincs := {[s1,s3]: [s1,s2] in inc_conjs, s3 in inc_conjs{s2}} - inc_conjs; -- exploit the transitivity of inclusion if newincs /= {} then -- expand the set of known inclusions inc_conjs +:= newincs; something_changed := true; -- and flag for another iteration end if; newmembs := {[s1,s3]: [s1,s2] in memb_conjs, s3 in inc_conjs{s2}}; newmembs -:= memb_conjs; if newmembs /= {} then -- expand the set of known inclusions memb_conjs +:= newmembs; something_changed := true; -- and flag for another iteration end if; vars_to_descriptors +:= {[u,{v}]: [u,v] in inc_conjs | is_string(u) and u notin basic_preds and v in basic_descriptors} + {[u,v]: [u,v] in memb_conjs | is_string(u) and u notin basic_preds and v in basic_descriptors} + {[u,"NONNULL"]: u in inc_conjs{"NONNULL"} | is_string(u) and u notin basic_descriptors} + {[u,"INFIN"]: u in inc_conjs{"INFIN"} | is_string(u) and u notin basic_descriptors}; -- convert the conjuncts we have so far to a vars_to_descriptors multivalued map -- for each memb_conj [u,v], we get all the descriptors of v given the -- current vars_to_descriptors, -- and of thoos take the ones which are sets, whos menbers become descriptors of x. -- for each inc_conj [u,v], we get all the descriptors of v given the -- current vars_to_descriptors, -- and of those take the ones which are sets, which become descriptors of x. --print("propagation iteration " + debug_count + ": vars_to_descriptors in extract_relevant_descriptors: ",vars_to_descriptors); for [u,v] in memb_conjs loop -- v can be the tree of an expression if is_string(u) then vtd := {[x,vars_to_descriptors{x}]: x in domain(vars_to_descriptors)}; -- convert to set-valued map, as required by expression_descriptor_in expn_descriptors := expression_descriptor_in(v,vtd); -- call the recursive workhorse to get the descriptor set of the expression new_u := {}; if v in basic_preds then new_u := {[u,d]: d in descriptors_of_basic(v) with v}; elseif u notin basic_preds then --?? wouldn't this be an indication of an earlier bug? [ALEXANDRU] new_u := {[u,d]: d in descriptor_action_of_memb(expn_descriptors)}; end if; if not( vars_to_descriptors incs new_u) then vars_to_descriptors +:= new_u; something_changed := true; end if; end if; end loop; for [u,v] in inc_conjs loop -- v can be the tree of an expression vtd := {[x,vars_to_descriptors{x}]: x in domain(vars_to_descriptors)}; -- convert to set-valued map, as required by expression_descriptor_in expn_descriptors := expression_descriptor_in(v,vtd); -- call the recursive workhorse to get the descriptor set of the expression vars_to_descriptors +:= ({[u,ed]: ed in expn_descriptors | (is_set(ed) or (ed in inherited_descriptors and u notin basic_descriptors))} + {[u,ed]: ed in expn_descriptors | is_string(ed) and (ed notin basic_descriptors) and (u = "INFIN" or u = "NONNULL")}); end loop; -- end of loop for initial propagation by transitive closure -- for equalities, we calculate the descriptor set of the right hand side using -- the available vars_to_descriptors and propagate it to the left-hand variable. -- here expn is the parse tree of an expression for [v,expn] in equality_conjs loop -- iterate over all available equalities if v notin basic_sets then vtd := {[x,vars_to_descriptors{x}]: x in domain(vars_to_descriptors)}; -- convert to set-valud map, as required by expression_descriptor_in expn_descriptors := expression_descriptor_in(expn,vtd); -- call the recursive workhorse to get the descriptor set of the expression -- look for the new_descriptors for this variable -- new_descriptors := expn_descriptors - (desv := vars_to_descriptors{v}); new_descriptors := expn_descriptors + vars_to_descriptors{unparse(expn)} - (desv := vars_to_descriptors{v}); --print("vars_to_descriptors equality loop: ",v," ",vars_to_descriptors," expn_descriptors: ",expn_descriptors," new_descriptors: ",new_descriptors); if new_descriptors /= {} then vars_to_descriptors{v} := desv + new_descriptors; something_changed := true; end if; end if; end loop; -- if any of these operations extend the set of descriptors available for any variable, we set the 'something_changed' -- to true, thereby forcing another iteration. end loop; -- on exiting this loop we have collected all relevant descriptors vars_to_descriptors +:= ({[v,"INFIN"]: v in inc_conjs{"INFIN"} | is_string(v)} + {[v,"NONNULL"]: v in inc_conjs{"NONNULL"} | is_string(v)}); -- convert the INFIN and NONULL special inclusions to standard descriptors res := {[x,vars_to_descriptors{x}]: x in domain(vars_to_descriptors) | x notin basic_descriptors}; -- convert into map-to-sets and return --print("\ndebug_count: ",debug_count," vars_to_descriptors after loop exit: ",res," inc_conjs after loop exit: ",inc_conjs); return res; end extract_relevant_descriptors; procedure extract_relevant_conjuncts(tree); -- walk the tree, collecting the relevant top-level conjuncts. -- the relevant conjuncts are those stating membrship or inclusion of one variable in another var memb_conjs := {}; -- conjuncts designating membership: will be collected as pairs var inc_conjs := {}; -- conjuncts designating inclusion: will be collected as pairs var equality_conjs := {}; -- conjuncts designating equalities to setformers: will be collected as pairs extract_relevant_conjuncts_in_new(tree); -- call the recursive workhorse --print("[memb_conjs,inc_conjs,equality_conjs]: ",[memb_conjs,inc_conjs,equality_conjs]); return [memb_conjs,inc_conjs,equality_conjs]; -- return all the pairs collected procedure extract_relevant_conjuncts_in_new(tree); -- internal recursive workhorse --print("extract_relevant_conjuncts_in_new: ",tree); if is_string(tree) then return; end if; -- since we have hit bottom [n1,n2,n3] := tree; -- decompose the node case n1 when "ast_in" => -- collect if membership between variables -- memberships with compound right hand side are collected, since these can produce valuable descriptors memb_conjs with:= [unparse(n2),n3]; inc_conjs with:= ["NONNULL",unparse(n3)]; -- memberships with simple right hand side are collected as assertions of non-nullity when "ast_incs" => -- reverse and collect if inclusion between variables if is_tuple(n3) and n3(1) = "ast_enum_set" then for j in [2..#n3] loop memb_conjs with:= [unparse(n3(j)), n2]; end loop; else inc_conjs with:= [unparse(n3),n2]; -- inclusions with compound right hand side are collected, since these can produce valuable descriptors end if; when "DOT_INCIN" => -- collect if inclusion between variables if is_tuple(n2) and n2(1) = "ast_enum_set" then for j in [2..#n2] loop memb_conjs with:= [unparse(n2(j)), n3]; end loop; else inc_conjs with:= [unparse(n2),n3]; -- inclusions with compound right hand side are collected, since these can produce valuable descriptors end if; --print("inc_conjs: ",inc_conjs); when "ast_ne" => -- collect assertions of non-nullity if n3 = "0" then inc_conjs with:= ["NONNULL",unparse(n2)]; -- this is collected as an inclusion of a dummy element elseif n2 = "0" then inc_conjs with:= ["NONNULL",unparse(n3)]; -- this is collected as an inclusion of a dummy element end if; when "ast_eq" => -- we are concerned here with just a few kinds of equality clauses -- (1) assertions domain(x) = y and range(x) = y between variables, which are collected into dom_conjs and range_conjs respectively -- (2) assertions of equality between a variable and a setformer whose lead expression is a pair -- and whose limiting sets are simple variables, e.g. {[e(x),f(x)]: x in s | P(x)} but not -- {[e(x),f(x)]: x in (s + t) | P(x)}. These always define maps, and the closure properties of e(x) and -- f(x) may allow something to be said concerning the domain and range of these maps. In some cases like -- {[x,f(x)]: x in s | P(x)} we may be able to say that the map is single valued, and in cases like -- {[[x,y],[y,x]]: x in s, y in t | P(x,y)} we may be able to say that the map is 1-1. if is_string(n2) then -- variable equals setformer -- we collect equalities of all kinds, since even if they do not define maps we may be able to deduce something concerning their elements equality_conjs with:= [n2,n3]; if is_string(n3) then equality_conjs with:= [n3,n2]; end if; -- collect symmetrically to propagate descriptors in both directions elseif is_string(n3) then -- setformer equals variable -- we collect equalities of all kinds, since even if they do not define maps we may be able to deduce something concerning their elements equality_conjs with:= [n3,n2]; end if; -- these equalities should be used to propagate type info to the next level -- 'expression_descriptor' routine that calls this routine. when "ast_of" => -- collect if this is a predicate we can handle, converting it to a nominal membership case n2 -- examine the predicate when "FINITE" => -- collect and convert into a nominal inclusion memb_conjs with:= [unparse(n3(2)),"FIN"]; when "COUNTABLE" => -- collect and convert into a nominal inclusion memb_conjs with:= [unparse(n3(2)),"COUNTABLE"]; when "SVM" => -- collect and convert into a nominal inclusion memb_conjs with:= [unparse(n3(2)),"SVM"]; when "ONE_1_MAP" => -- collect and convert into a nominal inclusion memb_conjs with:= [unparse(n3(2)),"ONE_1_MAP"]; when "IS_MAP" => -- collect and convert into a nominal inclusion memb_conjs with:= [unparse(n3(2)),"IS_MAP"]; when "ORD" => -- collect and convert into a descriptor memb_conjs with:= [unparse(n3(2)),"ORD"]; when "CARD" => -- collect and convert into a descriptor memb_conjs with:= [unparse(n3(2)),"CARD"]; end case; when "ast_not" => -- collect if this is a negated predicate we can handle, converting it to a nominal membership if is_tuple(n2) then [m1,m2,m3] := n2; -- unpack the argument of the 'not' case m1 when "ast_eq" => -- collect assertions of non-nullity if is_string(m2) and m3 = "0" then inc_conjs with:= ["NONNULL",m2]; -- this is collected as an inclusion of a dummy element elseif is_string(m3) and m2 = "0" then inc_conjs with:= ["NONNULL",m3]; -- this is collected as an inclusion of a dummy element end if; when "ast_of" => -- collect assertions of infiniteness if m2 = "FINITE" then inc_conjs with:= ["INFIN",unparse(m3(2))]; -- this is collected as an inclusion of a dummy element end if; end case; end if; return; -- what remains is opaque when "ast_and","AMP_" => -- process arguments recursively; note that conjunctions can have two syntactic forms extract_relevant_conjuncts_in_new(n2); extract_relevant_conjuncts_in_new(n3); otherwise => return; -- what remains is opaque end case; end extract_relevant_conjuncts_in_new; procedure extract_relevant_conjuncts_in(tree); -- internal recursive workhorse (OLD VERSION) if is_string(tree) then return; end if; -- since we have hit bottom [n1,n2,n3] := tree; -- decompose the node case n1 when "ast_in" => -- collect if membership between variables if is_string(n2) then -- memberships with compound right hand side are collected, since these can produce valuable descriptors memb_conjs with:= [n2,n3]; end if; if is_string(n3) then -- memberships with simple right hand side are collected as assertions of non-nullity inc_conjs with:= ["NONNULL",n3]; end if; return; -- what remains is opaque when "ast_incs" => -- reverse and collect if inclusion between variables if is_string(n3) then -- inclusions with compound right hand side are collected, since these can produce valuable descriptors inc_conjs with:= [n3,n2]; end if; return; -- what remains is opaque when "DOT_INCIN" => -- collect if inclusion between variables if is_string(n2) then -- inclusions with compound right hand side are collected, since these can produce valuable descriptors inc_conjs with:= [n2,n3]; end if; return; -- what remains is opaque when "ast_ne" => -- collect assertions of non-nullity if is_string(n2) and n3 = "0" then inc_conjs with:= ["NONNULL",n2]; -- this is collected as an inclusion of a dummy element elseif is_string(n3) and n2 = "0" then inc_conjs with:= ["NONNULL",n3]; -- this is collected as an inclusion of a dummy element end if; return; -- what remains is opaque when "ast_eq" => -- we are concerned here with just a few kinds of equality clauses -- (1) assertions domain(x) = y and range(x) = y between variables, which are collected into dom_conjs and range_conjs respectively -- (2) assertions of equality between a variable and a setformer whose lead expression is a pair -- and whose limiting sets are simple variables, e.g. {[e(x),f(x)]: x in s | P(x)} but not -- {[e(x),f(x)]: x in (s + t) | P(x)}. These always define maps, and the closure properties of e(x) and -- f(x) may allow something to be said concerning the domain and range of these maps. In some cases like -- {[x,f(x)]: x in s | P(x)} we may be able to say that the map is single valued, and in cases like -- {[[x,y],[y,x]]: x in s, y in t | P(x,y)} we may be able to say that the map is 1-1. if is_string(n2) then -- variable equals setformer -- we collect equalities of all kinds, since even if they do not define maps we may be able to deduce something concerning their elements equality_conjs with:= [n2,n3]; if is_string(n3) then equality_conjs with:= [n3,n2]; end if; -- collect symmetrically to propagate descriptors in both directions elseif is_string(n3) then -- setformer equals variable -- we collect equalities of all kinds, since even if they do not define maps we may be able to deduce something concerning their elements equality_conjs with:= [n3,n2]; end if; when "ast_of" => -- collect if this is a predicate we can handle, converting it to a nominal membership case n2 -- examine the predicate when "FINITE" => -- collect and convert into a nominal inclusion if is_string(arg := n3(2)) then -- argument is a variable memb_conjs with:= [arg,"FIN"]; end if; return; -- what remains is opaque when "COUNTABLE" => -- collect and convert into a nominal inclusion if is_string(arg := n3(2)) then -- argument is a variable memb_conjs with:= [arg,"COUNTABLE"]; end if; return; -- what remains is opaque when "SVM" => -- collect and convert into a nominal inclusion if is_string(arg := n3(2)) then -- argument is a variable memb_conjs with:= [arg,"SVM"]; end if; return; -- what remains is opaque when "ONE_1_MAP" => -- collect and convert into a nominal inclusion if is_string(arg := n3(2)) then -- argument is a variable memb_conjs with:= [arg,"ONE_1_MAP"]; end if; return; -- what remains is opaque when "IS_MAP" => -- collect and convert into a nominal inclusion if is_string(arg := n3(2)) then -- argument is a variable memb_conjs with:= [arg,"IS_MAP"]; end if; return; -- what remains is opaque when "ORD" => -- collect and convert into a descriptor if is_string(arg := n3(2)) then -- argument is a variable memb_conjs with:= [arg,"ORD"]; end if; return; -- what remains is opaque end case; when "ast_not" => -- collect if this is a negated predicate we can handle, converting it to a nominal membership if is_tuple(n2) then [m1,m2,m3] := n2; -- unpack the argument of the 'not' case m1 when "ast_eq" => -- collect assertions of non-nullity if is_string(m2) and m3 = "0" then inc_conjs with:= ["NONNULL",m2]; -- this is collected as an inclusion of a dummy element elseif is_string(m3) and m2 = "0" then inc_conjs with:= ["NONNULL",m3]; -- this is collected as an inclusion of a dummy element end if; when "ast_of" => -- collect assertions of infiniteness if m2 = "FINITE" then if is_string(arg := m3(2)) then -- argument is a variable inc_conjs with:= ["INFIN",arg]; -- this is collected as an inclusion of a dummy element end if; end if; end case; end if; return; -- what remains is opaque when "ast_and","AMP_" => -- process arguments recursively; note that conjunctions can have two syntactic forms extract_relevant_conjuncts_in(n2); extract_relevant_conjuncts_in(n3); otherwise => return; -- what remains is opaque end case; end extract_relevant_conjuncts_in; end extract_relevant_conjuncts; procedure get_assertions_from_descriptors(vars_to_descriptors); -- convert descriptors to set membership assertions for use in ELEM deductions -- this looks for descriptors of various forms directly expressible as Ref clauses, and generates these clauses. -- the descriptors which can be handled in this way, and their translations, are Za, Re, Card, Ord, and the other elementary sets, -- which translate into x in Za, x in Re, Card(x), Ord(x), etc.; {Za}, {Re}, {Card}, {Ord}, which translate into -- x •incin Za etc., Fin and Countable, which become Finite(x) and Countable(x); Infin which becomes not Finite(x); -- and NonNull, which becomes x /= 0. We also handle Svm and one_1_map. new_vars_to_descriptors := vars_to_descriptors; -- make copy to extend --print("vars_to_descriptors: ",vars_to_descriptors); for [x,descs] in vars_to_descriptors loop if "CARD" in descs then descs with:= "ORD"; end if; for m in (domain m_descriptors_of_basic) loop if (descs incs m) then descs +:= m_descriptors_of_basic(m); end if; end loop; new_vars_to_descriptors(x) := descs; end loop; --print("new_vars_to_descriptors: ",new_vars_to_descriptors); vars_to_clauses := [xx: xx in {was: [x,descs] in new_vars_to_descriptors, desc in descs | (was := write_as_assertion(x,desc)) /= OM}]; -- eliminate duplicates --print("vars_to_clauses: ",vars_to_clauses); return join(vars_to_clauses," & "); end get_assertions_from_descriptors; procedure write_as_assertion(x,desc); -- convert an individual descriptor to an assertion or assertions, if possible --print("write_as_assertion: ",x," ",desc); if desc in basic_sets then res := "(" + x + " in " + desc + ")"; elseif desc in basic_preds then -- convert to appropriate predicate statement. These need to be handled individually case desc -- the cases to be considered are "ORD","CARD","FIN","Infin","Countable","NONNULL","Is_map","Svm","one_1_map" when "ORD","CARD","SVM","IS_MAP","ONE_1_MAP" => res := desc + "(" + x + ")"; when "FIN" => res := "Finite(" + x + ")"; when "INFIN" => res := "(not Finite(" + x + "))"; when "COUNTABLE" => res := "(#" + x + " •incin Za)"; when "NONNULL" => res := "(" + x + " /= 0)"; end case; elseif is_set(desc) then -- handle elementary inclusions, and case of map if desc = {} then res := OM; elseif (basicdesc := desc * basic_sets) /= {} then res := (+/ {" and (" + x + " •incin " + indesc2 + ")": indesc2 in basicdesc})(6..); elseif is_pair(indesc := arb(desc)) then -- we add "IS_MAP" descriptor [c1,c2] := indesc; res := "Is_map(" + x + ")" -- we check if we can extract relevant information about its domain / range -- in case of a descriptor {["ZA", "OM"]} or of a descriptor {[{"ZA", "ORD"}, "OM"]} + if c1 in basic_sets then " and (domain(" + x + ") •incin " + c1 + ")" -- elseif c1 in basic_descriptors then " and " + write_as_inclassertion("domain(" + x + ")", c1) elseif is_set(c1) then "" +/ {" and (domain(" + x + ") •incin pow(" + indesc2 + "))": indesc2 in basic_sets * c1} else "" end if -- similarly in case of a descriptor {["OM", "ZA"]} or of a descriptor {["OM", {"ZA", "ORD"}]} + if c2 in basic_sets then " and (range(" + x + ") •incin " + c2 + ")" -- elseif c2 in basic_descriptors then " and " + write_as_inclassertion("domain(" + x + ")", c2) elseif is_set(c2) then "" +/ {" and (range(" + x + ") •incin pow(" + indesc2 + "))": indesc2 in basic_sets * c2} else "" end if; elseif is_set(indesc) then --?? res := ("" +/ {" and (" + x + " •incin pow(" + indesc2 + "))": indesc2 in indesc * basic_sets})(6..); for indesc2 in indesc * basic_sets loop res := if res = OM then "(" + x + " •incin pow(" + indesc2 + "))" else res + " and (" + x + " •incin pow(" + indesc2 + "))" end if; end loop; end if; elseif is_pair(desc) and (c1 := desc(1)) in basic_sets and (c2 := desc(2)) in basic_sets then -- pair, with knowledge of components res := "(" + x + " = [car(" + x + "),cdr(" + x + ")]) and (car(" + x + ") in " + c1 + ") and (cdr(" + x + ") in " + c2 + ")"; end if; -- if res /= OM then print(x," ",desc," becomes: ",res); end if; return res; end write_as_assertion; -- ************ Library of procedures giving action of various important set-theoretic operators on descriptors ************ procedure extended_descriptors(descriptor_set); -- add implied attributes to original set of attributes --print("extended_descriptors gets: ",descriptor_set); descs := descriptor_set +/ {dob: att in descriptor_set | (dob := descriptors_of_basic(att)) /= OM}; --print("extended_descriptors generates: ",descriptor_set); for m in (domain m_descriptors_of_basic) loop if (descs incs m) then descs +:= m_descriptors_of_basic(m); end if; --print("extended_descriptors produces: ",descriptor_set); end loop; if (exists d in descs | is_set(d) and (exists e in d | is_pair(e))) then descs with:= "IS_MAP"; end if; return descs; end extended_descriptors; procedure extended_descriptors2(descriptor_set); -- add implied attributes to original set of attributes descs := extended_descriptors(descriptor_set); -- d := {} +/ {x in descs | is_set(x)}; -- if d /= {} then descs := (descs - d) with +/ {d}; end if; -- compress all descriptors of the form {D} together d := {x in descs | is_set(x)}; if d /= {} then descs := (descs - d) with +/ d; end if; -- compress all descriptors of the form {D} together return descs; end extended_descriptors2; procedure extended_descriptors3(descriptor_set); -- add implied attributes to original set of attributes descs1 := {} +/ {dob: satt in descriptor_set | is_set(satt) and (dob := descriptors_of_basic(arb(satt))) /= OM}; -- return extended_descriptors(descriptor_set + {{d}: d in descs1 | not is_set(d)}); return extended_descriptors(descriptor_set + {{d}: d in descs1}); -- maximum generality ensures best treatment of unionset end extended_descriptors3; procedure descriptor_action_of_count(descriptor_set); -- action of the #s primitive descriptor_set := extended_descriptors(descriptor_set); descs := {"CARD","ORD"}; if "FIN" in descriptor_set then descs +:= {"HFIN","FIN","ZA"}; end if; if "NONNULL" in descriptor_set then descs with:= "NONNULL"; end if; return descs; end descriptor_action_of_count; procedure descriptor_action_of_next(descriptor_set); -- action of the next(s) function descriptor_set := extended_descriptors(descriptor_set); descs := {"NONNULL"}; if "FIN" in descriptor_set and "CARD" in descriptor_set then descs with:= "CARD"; end if; return descs + (descriptor_set * {"ZA","ORD","HFIN","FIN","COUNTABLE","INFIN"}); end descriptor_action_of_next; procedure descriptor_action_of_memb(descriptor_set); -- result of choosing an unknown member return descriptor_action_of_arb(descriptor_set with "NONNULL"); end descriptor_action_of_memb; procedure descriptor_action_of_subset(descriptor_set); -- result of choosing an unknown subset descriptor_set := extended_descriptors(descriptor_set); return {x in descriptor_set | is_set(x) or x in inherited_descriptors}; -- in addition to Fin, Hfin, Countable, etc., descriptors of the form {D} survive end descriptor_action_of_subset; procedure descriptor_action_of_pow(descriptor_set); -- if the subsets of the argument x of pow have a given descriptor D, -- then pow(x) has the descriptor {D} descs1 := descriptor_action_of_subset(descriptor_set); descs := {{x}: x in descs1} with "NONNULL" + {"HFIN","FIN","INFIN"} * descs1 + {"INFIN"} * descriptor_set; return descs; end descriptor_action_of_pow; procedure descriptor_action_of_Un(descriptor_set); -- If the argument x of Un has a descriptor D of the form {{D'}}, -- Un(x) has the descriptor {D'}. Also, if x has a descriptor {D'} where D' is unconditionally additive, then -- has the descriptor D'. Similarly, if if x has a descriptor {D'} where D' is finitely additive and x also has -- the descriptor Fin, then Un(x) has the descriptor D'. A similar statement is true for "Countable" descriptor_set := extended_descriptors(descriptor_set); d := {} +/ {x in descriptor_set | is_set(x)}; descs1 := {u : u in d | is_set(u)}; if (EXISTS s = descriptors_of_basic(u) | {"ORD"} in s and u in d) then descs1 with:= "ORD"; end if; if "NONNULL" in descriptor_set then descs1 +:= {u: u in d | u in quasi_additive_descriptors}; end if; descs1 +:= if "FIN" in descriptor_set then {u: u in d | u in finitely_additive_descriptors} else -- proceed more liberally in this case {u: u in d | u in fully_additive_descriptors} end if; return if descs1 = {} then {"OM"} else descs1 end if; end descriptor_action_of_Un; procedure descriptor_action_of_union(descriptor_set1,descriptor_set2); -- this forms the intersection of all descriptors of the form {D} which are common to both sets; -- also of all descriptors which are finitely additive descriptor_set1 := extended_descriptors(descriptor_set1); descriptor_set2 := extended_descriptors(descriptor_set2); --print("descriptor_action_of_union:",descriptor_set1,descriptor_set2); descs1 := (({x in descriptor_set1 | is_set(x) or x in finitely_additive_descriptors} * {x in descriptor_set2 | is_set(x) or x in finitely_additive_descriptors})) + (quasi_additive_descriptors * (descriptor_set1 + descriptor_set2)); return if descs1 = {} then {"OM"} else descs1 end if; end descriptor_action_of_union; procedure descriptor_action_of_intersection(descriptor_set1,descriptor_set2); -- this forms the union of all descriptors of the form {D} which are posessed by either of its argument sets; -- also of all descriptors which are inherited --print("descriptor_set1: ",descriptor_set1," ",descriptor_set2); descs1 := descriptor_action_of_subset(descriptor_set1) + descriptor_action_of_subset(descriptor_set2); return if descs1 = {} then {"OM"} else descs1 end if; end descriptor_action_of_intersection; procedure descriptor_action_of_difference(descriptor_set1,descriptor_set2); -- this forms the union of all descriptors of the form {D} which are posessed by its first argument set; -- also of all descriptors which are inherited descriptor_set1 := extended_descriptors(descriptor_set1); descriptor_set2 := extended_descriptors(descriptor_set2); descs1 := {x in descriptor_set1 | is_set(x) or x in inherited_descriptors}; if ("INFIN" in descriptor_set1) and ({"FIN","HFIN","ZA"} * descriptor_set2 /= {}) then descs1 with:= "INFIN"; end if; return if descs1 = {} then {"OM"} else descs1 end if; end descriptor_action_of_difference; procedure descriptor_action_of_range(descriptor_set); -- this looks for all descriptors of the form {[D,D']} in descriptor_set, and for each collects -- a descriptor {D}. Also, if Fin or Countable is in descriptor_set it is collected. If there is any -- {[D,D']} in descriptor_set and NonNull is in descriptor_set it is collected descriptor_set := extended_descriptors(descriptor_set); descs := {"FIN","COUNTABLE"} * descriptor_set; d := {} +/ {x in descriptor_set | is_set(x)}; descs1 := {a(2): x in d, a in x | is_pair(a)}; if descs1 /= {} then descs with := {descs1}; if "NONNULL" in descriptor_set then descs with:= "NONNULL"; end if; end if; --print("descriptor_action_of_range returns: ",descriptor_set," descs: ",descs); return if descs = {} then {"OM"} else descs end if; end descriptor_action_of_range; procedure descriptor_action_of_domain(descriptor_set); -- this looks for all descriptors of the form {[D,D']} in descriptor_set, and for each collects -- a descriptor {D'}. Also, if Fin or Countable is in descriptor_set it is collected. If there is any -- {[D,D']} in descriptor_set and NONNULL is in descriptor_set it is collected descriptor_set := extended_descriptors(descriptor_set); descs := {"FIN","COUNTABLE"} * descriptor_set; d := {} +/ {x in descriptor_set | is_set(x)}; descs1 := {a(1): x in d, a in x | is_pair(a)}; if descs1 /= {} then descs with := {descs1}; if "NONNULL" in descriptor_set then descs with:= "NONNULL"; end if; end if; --print("descriptor_action_of_domain returns: ",descriptor_set," descs: ",descs); return if descs = {} then {"OM"} else descs end if; end descriptor_action_of_domain; procedure descriptor_action_of_arb(descriptor_set); -- if NonNull is in descriptor_set, then D is collected for each {D} in descriptor_set --print("descriptor_set in arb before: ",descriptor_set); descriptor_set := extended_descriptors(descriptor_set); --print("descriptor_set in arb: ",descriptor_set); d := {} +/ {x in descriptor_set | is_set(x)}; descs := (if "NONNULL" in descriptor_set then d else (d * transitive_descriptors) + if "CARD" in d then {"CARD"} else {} end if end if) + {x in descriptor_set | x in transitive_descriptors}; if "CARD" in descriptor_set then descs with:= "CARD"; end if; descs := extended_descriptors(descs); return if descs = {} then {"OM"} else descs end if; -- otherwise the value of arb could be an element of the set or could be 0 end descriptor_action_of_arb; procedure descriptor_action_of_pair(descriptor_set1,descriptor_set2); -- this forms a kind of cartesian product of the two descriptor sets descriptor_set1 := extended_descriptors2(descriptor_set1); descriptor_set2 := extended_descriptors2(descriptor_set2); --print("descriptor_action_of_pair: ",descriptor_set1," ",descriptor_set2); descs := {[x,y]: x in descriptor_set1,y in descriptor_set2}; return if descs = {} then {"OM"} else descs end if; end descriptor_action_of_pair; procedure descriptor_action_of_car(descriptor_set); -- this looks for all descriptors of the form [x,y] descriptor_set, and collects the x's descriptor_set := extended_descriptors(descriptor_set); descs := {x(1): x in descriptor_set | is_pair(x)} + (descriptor_set * transitive_descriptors); return if descs = {} then {"OM"} else descs end if; end descriptor_action_of_car; procedure descriptor_action_of_cdr(descriptor_set); -- this looks for all descriptors of the form [x,y] descriptor_set, and collects the y's descriptor_set := extended_descriptors(descriptor_set); descs := {x(2): x in descriptor_set | is_pair(x)} + (descriptor_set * transitive_descriptors); return if descs = {} then {"OM"} else descs end if; end descriptor_action_of_cdr; procedure descriptor_action_of_cartprod(descriptor_set1,descriptor_set2); -- This forms the union of all descriptors of the form {[D,D']} where -- D and D' are possessed by the first and second argument set respectively; -- also of any of the descriptors NonNull, Fin, Infin which is common -- to the argument sets. If one of the arguments is NonNull and the -- other is Inf, then Inf is collected. descriptor_set1 := extended_descriptors(descriptor_set1); descriptor_set2 := extended_descriptors(descriptor_set2); -- d1 := {x in descriptor_set1 | is_set(x)} + {{x}: x in (descriptor_set1 * transitive_descriptors * basic_sets)}; -- d2 := {x in descriptor_set2 | is_set(x)} + {{x}: x in (descriptor_set2 * transitive_descriptors * basic_sets)}; d1 := {{} +/ {x in descriptor_set1 | is_set(x)}}; d2 := {{} +/ {x in descriptor_set2 | is_set(x)}}; descs := {{[u,v]}: x in d1, y in d2, u in x, v in y} with "IS_MAP"; -- descs +:= {"NONNULL","FIN","COUNTABLE"} * descriptor_set1 * descriptor_set2; if (("NONNULL" in descriptor_set1) and ("INFIN" in descriptor_set2)) or (("NONNULL" in descriptor_set2) and ("INFIN" in descriptor_set1)) then descs with:= "INFIN"; end if; return descs; end descriptor_action_of_cartprod; procedure descriptor_action_of_funcprod(descriptor_set1,descriptor_set2); -- the syntactic template here is as shown by ["AT_", "F", "G"]. Note that a space is needed in the string form var descs1, descs2; descriptor_set1 := extended_descriptors(descriptor_set1); descriptor_set2 := extended_descriptors(descriptor_set2); descs1 := {} +/ {{p in x | is_pair(p)}: x in descriptor_set1 | is_set(x)}; descs2 := {} +/ {{p in x | is_pair(p)}: x in descriptor_set2 | is_set(x)}; -- descs := {{[p(1),q(2)]}: p in descs2, q in descs1 | p(2) = q(1)} with "IS_MAP"; descs := {{[p(1),q(2)]}: p in descs2, q in descs1} with "IS_MAP"; -- descs +:= (descriptor_set1 * descriptor_set2 * {"FIN","HFIN","COUNTABLE","ONE_1_MAP"}); return descs; end descriptor_action_of_funcprod; procedure descriptor_action_of_func_app(descriptor_set1,descriptor_set2); -- the syntactic template here is as shown by ["TILDE_", "F", ["ast_enum_tup", "X"]] -- needs thought to decide how to handle null sets descriptor_set1 := extended_descriptors(descriptor_set1); -- descriptor_set2 := extended_descriptors(descriptor_set2); -- UNUSED FOR THE TIME BEING descs := {} +/ {{p(2): p in x | is_pair(p) and (p(2) in const_properties("0"))}: x in descriptor_set1 | is_set(x)}; return if descs = {} then {"OM"} else descs end if; end descriptor_action_of_func_app; procedure descriptor_action_of_func_inv(descriptor_set); -- this is an ordinary unary function: the synactic template here is as shown by ["ast_of", "INV", ["ast_list", "F"]] descriptor_set := extended_descriptors(descriptor_set); -- descs := {{[p(2),p(1)]}: x in descriptor_set | is_set(x) and is_pair(p := arb(x))} with "IS_MAP"; descs := ({} +/ {{[p(2),p(1)]: p in x | is_pair(p)}: x in descriptor_set | is_set(x)}) with "IS_MAP"; descs +:= (descriptor_set * {"NONNULL","FIN","COUNTABLE","ONE_1_MAP"}); if descriptor_set incs {"IS_MAP","INFIN"} then descs with:= "INFIN"; end if; return descs; end descriptor_action_of_func_inv; -- procedure descriptor_action_of_func_ident(descriptor_set); -- -- this is an ordinary unary function: the synactic template here is as shown by ["ast_of", "IDENT", ["ast_list", "F"]] -- -- descriptor_set := extended_descriptors(descriptor_set); -- -- descs := {{[arb(x),arb(x)]}: x in descriptor_set | is_set(x)}; -- descs +:= {"NONNULL","FIN","COUNTABLE","INFIN"} * descriptor_set; -- -- return descs + {"IS_MAP",{["OM","OM"]},"SVM","ONE_1_MAP"}; -- --end descriptor_action_of_func_ident; procedure is_pair(p); -- at least for the time being, the only tuples that can occur in descriptors are pairs return is_tuple(p) and (#p = 2) and (p(1) /= OM); end is_pair; procedure fix_dot(stg); -- fix the dot character to make up for HTML change return "" +/ [if c = "•" then char(165) else c end if: c in stg]; end fix_dot; end proof_by_structure; -- **************************************************** -- *************** General-use algebraic parser ******* -- **************************************************** package algebraic_parser; -- package for simple algebraic parser procedure alg_parse(stg); -- the parsing routine procedure setup_parse_priorities_and_monadics(pri_map,mon_set,refversion); -- set up the priorities and monadics for algebraic test parsing end algebraic_parser; package body algebraic_parser; -- package for simple algebraic parser use string_utility_pak,get_lines_pak,sort_pak; const lets := "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"; const lets_plus := "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_"; const alphanums := "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_1234567890"; const lparens := "[({"; const rparens := "])}"; const numerics := "0123456789."; const whitespace := "\t \n\r"; const op_headers := "•~^@"; var ops := "*+-/
=&|:,!"; const match_to := {[ "}","{" ],[ "]","[" ],[ ")","(" ]}; -- matching left to right parens const let := 0,lparen := 1,rparen := 2,op := 3,numeric := 4,endc := 5,beginc := 6,val := 7,ophead := 8,bad := "bad"; const op_before := {[ "{","$2" ],[ "[","$1" ],[ "(","" ]}; -- dummy operators before various opening parentheses const exp_prec := 23; -- precedence of exponential op const conditional_prec := 5; -- precedence of conditional op sel tok_start(1),tok_body(2),tok_type(3); var op_precedence := {}; -- arithmetics var can_be_monadic := {"+","-","~"}; var orig_string,the_string,string_ix,sl; var parse_stack := small_parse_stack := []; var token_type := lparen,prior_type; var debug_nt,under_lines,parse_level; var ref_version := {}; -- maps opsigns used in external formulae into their Ref versions var while_iters := 0; -- possible diagnostics -- ^**** ERROR: Empty parentheses are not allowed. -- ^**** ERROR: Closing parenthesis cannot follow right after an operator sign. -- ^**** ERROR: Mismatched right-opening parenthesis. -- ^**** ERROR: Mismatched left-opening parenthesis. -- ^**** ERROR: Illegal character. -- ^**** ERROR: Multiple decimal points in number symbol. -- ^**** ERROR: Monadic use of this operator is not allowed. -- ^**** ERROR: Unmatched right-opening parenthesis. -- ^**** ERROR: Number symbol can only follow open parenthesis or operator. -- ^**** ERROR: Left parentheses are not allowed at end of formula. -- ^**** ERROR: Formula cannot end with an operator sign. -- ^**** ERROR: Unmatched left parenthesis. -- ^**** ERROR: Illegal operator sign -- ^**** ERROR: Impossibly long run of operator signs. -- ^**** ERROR: Logical negation operator cannot be binary. -- conditional operator must occur in groups of odd length -- this is a simple stacking parse. The symbols allowed are single alphabetics, parens, *+-/•. -- If a left paren is encountered, examine the type of the preceding symbol. If this is a numeric or a letter, -- generate a null operator instead and handle it as a normal operator. Otherwise stack this. -- If an op is encountered, examine the preceding symbol. Diagnose an error if it is an operator or paren -- and this cannot be monadic; but if this can be monadic, introduce a null op. If the preceding -- symbol is not an operator, examine the symbol before it. If that has lower precedence, stack -- this. If it has equal or greater precedence, generate it if it has greater precedence, -- otherwise stack this. -- If a numeric is encountered, examine the preceding symbol. Diagnose an error unless it is an operator. -- Otherwise stack the numeric. -- If a letter is encountered, examine the type of the preceding symbol. If this is a numeric or a letter, -- generate a null operator instead and handle it as a normal operator. Otherwise stack this. -- If space is encountered, bypass it. -- If a bad character is encountered, diagnose it and end the parse. -- If a right paren is encountered, insist that a numeric, letter, or right paren precede. If this is -- so, unstack the prior operators in precedence groups, and insist that the left parenthesis -- eventually found matches this. -- The parse is readily adaptable to a larger set of operators, including comparison, Boolean, -- and conditional operators, also set membership. The following conventions are proposed. We allow -- the operators =,~=,<,>,<=,>=; &,|,~,^,- (which is the same as <=), when the Boolean values are taken -- to be 0 (false) and 1 (true); << (min) and >> (max); a:b:c:d:e (necessarily in sequences of an -- odd number of components, meaning a:b:(c:d:e), where the middle is evaluated first and must be Boolean, -- and then the left (if true) or the right (if false); and x@s (for x in s). Functions and set operators -- can also be handled: procedure setup_parse_priorities_and_monadics(pri_map,mon_set,refversion); -- set up the priorities and monadics for algebraic test parsing; also the map for Ref translation op_precedence := pri_map; can_be_monadic := mon_set; ref_version := refversion?{}; end setup_parse_priorities_and_monadics; procedure alg_parse(stg); -- the parsing routine --print("parsing: ",stg); parse_stack := small_parse_stack := []; sl := #(the_string := orig_string := stg); string_ix := 1; prior_type := beginc; loop [ix,the_char] := nt := debug_nt := next_tok(); --print("nt:",nt," ",token_type," ",the_char," ",parse_stack); case token_type when let,numeric,lparen => -- simply stack parse_stack with:= [ix,the_char,token_type]; -- stack small_parse_stack with:= the_char; when rparen,endc => unstack_to_prec(0); -- unstack to precedence 0 (left paren or start) -- this leaves the matching open parenthesis on the stack -- now verify that the right parenthesis is matched, and properly matched if token_type = bad then return OM; end if; if token_type = rparen then -- check proper match if #parse_stack = 1 then string_ix -:= 1; return diagnose_parse("Unmatched left-opening parenthesis: " + the_char); end if; if (the_lp := parse_stack(#parse_stack - 1)).tok_body /= match_to(the_char) then -- parenthesis mismatch string_ix -:= 1; diagnose_parse("Mismatched right-opening parenthesis: " + the_lp.tok_body); return diagnose_parse("Mismatched left-opening parenthesis: " + the_char); end if; -- remove the matching paren. arg frome parse_stack; junk_paren frome parse_stack; parse_stack with:= arg; small_arg frome small_parse_stack; arg frome small_parse_stack; small_parse_stack with:= small_arg; token_type := val; -- next character sees a val else -- symbol is end-of-string; verify that the parse stack has at most one element. -- any other element must be an unmatched left parenthesis. if #parse_stack > 1 then return diagnose_parse("Unmatched right-opening parenthesis: " + orig_string); end if; return small_parse_stack(1); -- finished in any case -- return the parse tree, less outermost tuple bracket end if; -- if no error was found, we have now stacked a value. when op => -- must always be binary if (op_prec := op_precedence(the_char)) = OM then print("the_char:: ",the_char); return diagnose_parse("Operator of unknown precedence: " + the_char); end if; if (nps := #parse_stack) > 1 and op_prec < op_precedence(parse_stack(nps - 1).tok_body) then -- unstack first unstack_to_prec(op_prec); if token_type = bad then return OM; end if; end if; parse_stack with:= [ix,the_char,token_type]; -- now stack this op small_parse_stack with:= the_char; when bad => return OM; end case; end loop; return small_parse_stack(1); -- the parse tree, less outermost tuple bracket end alg_parse; procedure unstack_to_prec(prec); -- unstack operands and operators until an item of precedence no more than -- 'prec' is encountered. --print("unstack_to_prec: ",prec); while (nps := #parse_stack) > 1 and token_type /= bad and (top_op_prec := op_precedence(parse_stack(nps - 1).tok_body)) > prec loop unstack_at_prec(top_op_prec); --print("unstack_to_prec loop: ",#parse_stack - 1," ",parse_stack(#parse_stack - 1).tok_body," ",op_precedence(parse_stack(#parse_stack - 1).tok_body)); end loop; --print("small_parse_stack after unstack_to_prec: ",small_parse_stack); end unstack_to_prec; procedure unstack_at_prec(prec); -- unstack operators of equal precedence, handle monadics -- ops of precedence 3 (exponentials) are unstacked from right to left; others are left in a sequence. if prec = exp_prec then -- unstack from right to left while (nps := #parse_stack) > 1 and op_precedence(parse_stack(#parse_stack - 1).tok_body) = prec loop arg2 frome parse_stack; the_op frome parse_stack; arg1 frome parse_stack; parse_stack with:= [arg1.tok_start, [arg1,the_op,arg2], val]; small_arg2 frome small_parse_stack; small_the_op frome small_parse_stack; small_arg1 frome small_parse_stack; small_parse_stack with:= [ref_version(small_the_op)?small_the_op,small_arg1,small_arg2]; end loop; else -- unstack a sequence of operators of equal precedence first_val frome parse_stack; unparse_stack := [first_val]; small_first_val frome small_parse_stack; small_unparse_stack := [small_first_val]; while (nps := #parse_stack) > 0 and op_precedence(parse_stack(nps).tok_body) = prec loop -- note ?? that the op at nps must be binary since unaries have been eliminated if parse_stack(nps - 1).tok_body = "" then -- there is no argument on the stack -- the op is monadic, so apply it to the top of the unparse stack the_op frome parse_stack; unptop := unparse_stack(nump := #unparse_stack); unparse_stack(nump) := [the_op.tok_start,[the_op,unptop],val]; junk frome parse_stack; -- throw away the null argument of this monadic operator small_the_op frome small_parse_stack; -- miror the above operations for the small stack small_unptop := small_unparse_stack(small_nump := #small_unparse_stack); small_unparse_stack(small_nump) := [ref_version(small_the_op)?small_the_op,small_unptop]; junk frome small_parse_stack; -- throw away the null argument else -- the op is binary the_op frome parse_stack; the_arg frome parse_stack; unparse_stack with:= the_op; unparse_stack with:= the_arg; small_the_op frome small_parse_stack; small_the_arg frome small_parse_stack; small_unparse_stack with:= small_the_op; small_unparse_stack with:= small_the_arg; end if; end loop; nump := #unparse_stack; unparse_stack := [unparse_stack(j): j in [nump,nump - 1..1]]; condensed_piece := [unparse_stack(1).tok_start,unparse_stack, val]; small_nump := #small_unparse_stack; small_unparse_stack := [small_unparse_stack(j): j in [small_nump,small_nump - 1..1]]; small_condensed_piece := ops_first(small_unparse_stack); if small_condensed_piece(1) = "ast_of" and (is_string(scp3 := small_condensed_piece(3)) or scp3(1) /= "ast_list") then small_condensed_piece(3) := ["ast_list",scp3]; -- special action for functions of one arg end if; --print("small_condensed_piece: ",small_condensed_piece); parse_stack with:= condensed_piece; small_parse_stack with:= small_condensed_piece; cptb := condensed_piece.tok_body; if prec = conditional_prec and (#cptb mod 4) /= 1 then string_ix := cptb(#cptb - 1).tok_start; diagnose_parse("Conditional expresssions must contain an odd number of clauses."); end if; end if; end unstack_at_prec; procedure ops_first(arg_op_tup); -- nests tuple of args interspersed with ops all of equal precedence if (naat := #arg_op_tup) = 1 then return arg_op_tup(1); end if; -- arg only if op_precedence(aat2 := arg_op_tup(2)) < 5 then -- don't nest, also treat operator as prefix if operator has small positive precedence; -- these are separators, like commas --print("ops_first: ",arg_op_tup," ",[ref_version(aat2 := arg_op_tup(2))?aat2] + [x: x = arg_op_tup(j) | odd(j)]); return [ref_version(aat2 := arg_op_tup(2))?aat2] + [x: x = arg_op_tup(j) | odd(j)]; end if; nested := [ref_version(aat2)?aat2,arg_op_tup(1),arg_op_tup(3)]; for j in [4,6..naat] loop nested := [ref_version(aatj := arg_op_tup(j))?aatj,nested,arg_op_tup(j + 1)]; end loop; return nested; end ops_first; procedure char_type(c); -- returns type of character if (c <= "Z" and c >= "A") or (c <= "z" and c >= "a") then return let; end if; if c in lparens then return lparen; end if; if c in rparens then return rparen; end if; if c in ops then return op; end if; if c in op_headers then return ophead; end if; if (c <= "9" and c >= "0") or c = "." then return numeric; end if; if c in whitespace then return space; end if; return bad; end char_type; procedure next_tok(); -- get next token, classify type --print("next_tok from: ",the_string); some_space := span(the_string,whitespace); -- whitespace automatically bypassed if some_space /= "" then string_ix +:= #some_space; end if; if (stix := string_ix) > sl then if token_type = lparen then return diagnose("Formula cannot end with a left parenthesis."); end if; if token_type = op then return diagnose("Formula cannot end with an operator sign."); end if; token_type := endc; return [sl + 1,endc]; end if; a_numeric := span(the_string,numerics); if a_numeric /= "" then if token_type /= op and token_type /= lparen and token_type /= beginc then return diagnose("Number symbol can only follow open parenthesis or operator."); end if; if #breakup(a_numeric,".") > 2 then return diagnose("Multiple decimal points in number symbol."); end if; string_ix +:= #a_numeric; token_type := numeric; return [stix,a_numeric]; end if; if (new_type := char_type(ch := the_string(1))) = lparen then if token_type = numeric or token_type = let or token_type = val then token_type := op; return [stix,op_before(ch)]; -- insert a null operator end if; end if; --print("new_type,ch: ",char_type(ch := the_string(1))," ",ch); if (new_type := char_type(ch := the_string(1))) = let then if token_type = numeric or token_type = let or token_type = val then token_type := op; return [stix,""]; -- insert a null operator end if; -- otherwise, if the immediately following character is an underscore or numeric, -- extend the variable name if #the_string > 1 then -- and the_string(2) in "_1234567890" tok_name := span(the_string,alphanums); -- span off the variable name string_ix +:= #tok_name; token_type := let; return [stix,tok_name]; -- count space and return it end if; end if; if new_type = rparen then -- rule out blank parentheses or right paren following op if token_type = lparen then return diagnose("Empty parentheses are not allowed."); end if; if token_type = op then return diagnose("Closing parenthesis cannot follow right after an operator sign."); end if; end if; if new_type = ophead then -- collect operator name following body match(the_string,ch); follow := span(the_string,lets_plus); opsign := ch + follow; if op_precedence(opsign) = OM then return diagnose("Illegal operator sign: " + opsign); end if; -- examine token to the left if token_type = op or token_type = lparen then if opsign notin can_be_monadic then return diagnose("Monadic use of the operator " + opsign + "is not allowed."); end if; the_string := opsign + the_string; -- restore the operator to the string token_type := let; return [stix,""]; -- introduce a null value end if; token_type := op; string_ix +:= #opsign; return [stix,opsign]; end if; opsign := span(the_string,ops); --print("opsign: ",opsign); if opsign /= "" then -- have an operation sign if #opsign > 3 then return diagnose("Impossibly long run of operator signs: " + opsign); end if; if op_precedence(opsign) = OM then return diagnose("Illegal operator sign: " + opsign); end if; -- examine token to the left if token_type = op or token_type = lparen then if ch notin can_be_monadic then return diagnose("Monadic use of the operator " + opsign + " is not allowed."); end if; the_string := opsign + the_string; -- restore the operator to the string token_type := let; return [stix,""]; -- introduce a null value end if; token_type := op; string_ix +:= #opsign; return [stix,opsign]; end if; token_type := new_type; if new_type = bad then return diagnose("Illegal character: " + ch); -- indicate the bad character end if; --print("the string at end: ",the_string); the_string := the_string(2..); string_ix +:= 1; return [stix,ch]; -- just return a single mysterious character end next_tok; procedure diagnose(msg); -- issue error diagnosis print("**** ERROR: ",msg); token_type := bad; return [string_ix,endc]; end diagnose; procedure diagnose_parse(msg); -- issue error diagnosis and return OM print("**** ERROR: ",msg); end diagnose_parse; end algebraic_parser; --->program program test; use string_utility_pak,parser,sort_pak,logic_syntax_analysis_pak,logic_syntax_analysis_pak2,logic_parser_aux,logic_parser_globals; init_logic_syntax_analysis(); -- initialize for logic syntaxt-tree operations do_tests2(); -- do the tests for this package procedure do_tests2(); -- do the tests for this package test_monotone_infer(); -- test the monotone_infer procedure test_replace_fcn_symbol(); stop; -- test the replace_fcn_symbol procedure test_monotone_inference(); -- test the monotone_inference procedure test_find_fnc_symbs(); -- test the find_fnc_symbs procedure test_dequantify(); -- test the dequantify procedure post_alg_roles("DOT_S_PLUS,+,S_ZERO,0,S_ONE,1,DOT_S_MINUS,-,S_REV,--,DOT_S_TIMES,*,SI,ring"); post_alg_roles("ast_add,+,0,0,1,1,ast_sub,-,ast_uminus,--,ast_mult,*,SETS,ring"); post_alg_roles("DOT_PLUS,+,0,0,1,1,DOT_TIMES,*,DOT_MINUS,OM,Za,ring"); -- forms := ["a;", "S_Rev(cn) •S_TIMES S_Rev(dn) = cn •S_TIMES dn;", "S_Rev(car(n)) •S_TIMES S_Rev(cdr(n)) = car(n) •S_TIMES cdr(n);", -- "((dx •S_TIMES dw) •S_TIMES ((ay •S_TIMES dz) •S_PLUS (az •S_TIMES dy)));", -- " ((dx •S_TIMES ay) •S_TIMES (dw •S_TIMES dz)) •S_PLUS ((dw •S_TIMES az) •S_TIMES (dy •S_TIMES dx));", -- "(dy •S_TIMES dz) •S_TIMES ((ax •S_TIMES dw) •S_PLUS (aw •S_TIMES dx));", -- "(a •S_TIMES d) •S_TIMES (b •S_TIMES e);", -- "(0 + b) + (c + d);", -- "(a + 0) + (c + d);", -- "(0 - b) - (c + d);", -- "-a - (c + d);", -- "(0 + b);", -- "(0 + b) - (c + d);", -- "(a + 0) - (c + d);", -- "(0 - b) - (c - d);", -- "(f(a) + b) + (c + d);", -- "(1 + b) + (c + d);", -- "(0 + b) + (c + d);", -- "(a + 0) + (c + d);", -- "(f(a) - b) - (c - d);", -- "(1 - b) - (c - d);", -- "(a - 0) - (c - d);", -- "(f(a) - b) - (c + d);", -- "(1 - b) - (c + d);", -- "(0 - b) - (c + d);", -- "(a - 0) - (c + d);", -- "(f(a) + b) - (c + d);", -- "(1 + b) - (c + d);", -- "-a - (c + d);", -- "-(-a) - (c + d);", -- "- -a - (c + d);", -- "(a + b) * (a + b);", -- "(a + b) * (a - b);", -- "(a + b) * (b);", -- "(a + b) * (-b);", -- "(a - b) * (b);", -- "(a - b) * (-b);", -- "(a * b) * (c * d);", -- "(a * b) * (-(c * d));", -- "a * (-(c + d));", -- "(-(a * b)) * (c * d);", -- "(-(a * b)) * f(c * d);", -- "(-(a * b)) * (c + d);", -- "(-(a + b)) * (c - d);", -- "1 * (c - d);", -- "1 * (-(c - d));", -- "1 * (-c);", -- "(-(a + b)) * 1;", -- "0 * (c - d);", -- "(-(a + b)) * 0;", -- "(a * b) * (c + d);", -- "(a * b) * ((c + d) - (e * f));", -- "arb(a •S_TIMES S_REV(f(b •S_MINUS c))) in {x •S_PLUS y: x in a, y in b};", -- "arb(a * f(b - c)) in {x + y: x in a, y in b};", -- "(S_rev(S_rev(a))) •S_minus (c •S_plus d);", -- "(S_rev(S_rev(S_rev(S_rev(a))))) •S_minus (c •S_plus d);", -- "(S_rev(S_rev(S_rev(a)))) •S_minus (c •S_plus d);", -- "a •S_TIMES S_REV(f(b •S_MINUS c));", -- "S_REV(f(b •S_MINUS c));", -- "f(b •S_MINUS c);", -- "(S_rev(a •S_plus b));", -- "(S_rev(a •S_plus b)) •S_times S_one;", -- "(S_zero •S_plus b);", -- "(S_zero •S_plus b) •S_plus (c •S_plus d);", -- "(a •S_plus S_zero) •S_plus (c •S_plus d);", -- "(S_zero •S_minus b) •S_minus (c •S_plus d);", -- "S_rev(a) •S_minus (c •S_plus d);", -- "(S_zero •S_plus b);", -- "(S_zero •S_plus b) •S_minus (c •S_plus d);", -- "(a •S_plus S_zero) •S_minus (c •S_plus d);", -- "(S_zero •S_minus b) •S_minus (c •S_minus d);", -- "(f(a) •S_plus b) •S_plus (c •S_plus d);", -- "(S_one •S_plus b) •S_plus (c •S_plus d);", -- "(S_zero •S_plus b) •S_plus (c •S_plus d);", -- "(a •S_plus S_zero) •S_plus (c •S_plus d);", -- "(f(a) •S_minus b) •S_minus (c •S_minus d);", -- "(S_one •S_minus b) •S_minus (c •S_minus d);", -- "(a •S_minus S_zero) •S_minus (c •S_minus d);", -- "(f(a) •S_minus b) •S_minus (c •S_plus d);", -- "(S_one •S_minus b) •S_minus (c •S_plus d);", -- "(S_zero •S_minus b) •S_minus (c •S_plus d);", -- "(a •S_minus S_zero) •S_minus (c •S_plus d);", -- "(f(a) •S_plus b) •S_minus (c •S_plus d);", -- "(S_one •S_plus b) •S_minus (c •S_plus d);", -- "S_rev(a) •S_minus (c •S_plus d);", -- "(a •S_plus b) •S_times (a •S_plus b);", -- "(a •S_plus b) •S_times (a •S_minus b);", -- "(a •S_plus b) •S_times (b);", -- "(a •S_plus b) •S_times (S_rev(b));", -- "(a •S_minus b) •S_times (b);", -- "(a •S_minus b) •S_times (S_rev(b));", -- "(a •S_times b) •S_times (c •S_times d);", -- "(a •S_times b) •S_times (S_rev(c •S_times d));", -- "a •S_times (S_rev(c •S_plus d));", -- "(S_rev(a •S_times b)) •S_times (c •S_times d);", -- "(S_rev(a •S_times b)) •S_times f(c •S_times d);", -- "(S_rev(a •S_times b)) •S_times (c •S_plus d);", -- "(S_rev(a •S_plus b)) •S_times (c •S_minus d);", -- "S_one •S_times (c •S_minus d);", -- "S_one •S_times (S_rev(c •S_minus d));", -- "S_one •S_times (S_rev(c));", -- "S_zero •S_times (c •S_minus d);", -- "(S_rev(a •S_plus b)) •S_times S_zero;", -- "(a •S_times b) •S_times (c •S_plus d);", -- "(a •S_times b) •S_times ((c •S_plus d) •S_minus (e •S_times f));", -- "(-a) - (c + d);", -- "(-a) - 0;", -- "(-a) - (c - d);", -- "(-a) - -(c + d);", -- "(c + d) - (-a);", -- "0 - (-a);", -- "(c - d) - (-a);", -- "((a * d) * (b * e) + (d * a) * (b * e));", -- "((a(x) * {f(u): u in s}) * (b(x) * e( x)) + ({f(w): w in s} * a(x )) * (b(x ) * e(x))) + ((a(x) * b(x)) * ({f(u): u in s} * e(x)) + (e(x) * {f(v): v in s}) * (b(x) * a(x)));", -- "(a + b) - a;", -- "(a + b) - b;", -- "(b + a) - b;", -- "(a + b + c + d) - (a + d);", -- "(a + b + c + d) - (b + d);", -- "(d + b + c + a) - (a + d);", -- "(d + b + c + a) - (b + d);", -- "(a + b * bb + c + d) - (a + d);", -- "(a + b * bb + c + d) - (bb * b + d);", -- "(d + b * bb + c + a) - (a + d);", -- "(d + b * bb + c + a) - (bb * b + d);", -- "(a + b * bb + c + d) - bb * b;", -- "(d + b * bb + c + a) - bb * b;", -- "(a(x) + b(x)) - a(x);", -- "(a(x) + b(x)) - b(x);", -- "(b(x) + a(x)) - b(x);", -- "(a(x) + b(x) + c(x) + d(x)) - (a(x) + d(x));", -- "(a(x) + b(x) + c(x) + d(x)) - (b(x) + d(x));", -- "(d(x) + b(x) + c(x) + a(x)) - (a(x) + d(x));", -- "(d(x) + b(x) + c(x) + a(x)) - (b(x) + d(x));", -- "(q •PLUS 1) •TIMES n;", -- "a •MINUS 1;", "a;"]; for form in forms loop tree := parze_expr(form)(2); anode_map := find_algebraic_nodes(tree); for [plop,nodes] in anode_map, node in nodes loop print("algebraic node: ",unparse(node)); end loop; for [plop,nodes] in anode_map, node in nodes loop print("algebraic identity: ",unparse(generate_algebraic_identity(node))); end loop; -- print(re_nest(standardize_subtree(tree,"ast_add"))); -- print(re_nest(standardize_subtree(tree,alg_of(tree(1))))); -- print(unparse(re_nest(standardize_subtree(tree,alg_of(tree(1))))),"\n"); -- print(unparse(canorder_subtree(tree)),"\n"); -- print(unparse(generate_algebraic_identity(tree)),"\n"); end loop; end do_tests2; end test;