Personal tools
You are here: Home Projects SETL SETL2 Source code EtnaNova_ELEM_supplement.stl
Document Actions

EtnaNova_ELEM_supplement.stl

by Paul McJones last modified 2021-02-26 20:21
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;

« November 2024 »
Su Mo Tu We Th Fr Sa
1 2
3 4 5 6 7 8 9
10 11 12 13 14 15 16
17 18 19 20 21 22 23
24 25 26 27 28 29 30
 

Powered by Plone CMS, the Open Source Content Management System

This site conforms to the following standards: