diff --git a/src/prover_phases/RecurrencePolynomial.ml b/src/prover_phases/RecurrencePolynomial.ml index cc02f5289..13ee1c2a9 100644 --- a/src/prover_phases/RecurrencePolynomial.ml +++ b/src/prover_phases/RecurrencePolynomial.ml @@ -96,7 +96,8 @@ and op = | D of var | XD of var | X of op list (* never X(X p · q) or X(C p · q) or X(A I); always X(_@[A _]) *) -| O of (var*poly)list +| O1 of var +| O of (var*poly)list (* O[v,[[A(V v)];[A I]]] is allowed, distinct form of O1 v *) let debug_poly_of_term = ref(Obj.magic()) let debug_free_variables = ref(Obj.magic()) @@ -115,16 +116,16 @@ let ( *:)c = map(( *.)c) let const_op_poly n = Z.(if equal n zero then [] else if equal n one then [[]] else [[C n]]) let const_eq_poly n = Z.(if equal n zero then [] else if equal n one then [[A I]] else [[C n; A I]]) (* Other safe constructors, except that one for X comes after ordering and general compositions after arithmetic, and A-T-constructor comes after variable and embedding accessors. *) -let var_poly i = [A(V i)] -let shift i = O[i,[var_poly i; [A I]]] -let mul_var i = X(var_poly i) +let var_poly ?(plus=Z.zero) i = [[A(V i)]] @ const_eq_poly plus +let shift i = O1 i +let mul_var i = X[A(V i)] -(* Distinguishes standard shift indeterminates from general substitutions. *) -let is1shift = function O[i,[[A(V j)];[A I]]] -> i=j | _ -> false -(* Distinguishes multishift indeterminates from general substitutions. *) -let is_multishift = function O f -> f |> for_all(function +(* Distinguishes multi- and 1-shift indeterminates from general substitutions and other indeterminates. *) +let is_shift = function O f -> f |> for_all(function | i, [[A(V j)]; ([A I] | [C _; A I])] -> i=j - |_->false) |_->false + | _->false) +|O1 _->true +| _->false (* Unused. See view_affine *) let is_affine = function O f -> f |> for_all(fun(_,f') -> f' |> for_all(function | [A I] | [C _; A I] | [A(V _)] | [C _; A(V _)] -> true @@ -223,7 +224,7 @@ let infinities r : 'r list ord_group = (* These are used to simplify defining orderings. They erase some structure from indeterminates that happens to be ignorable in all the orderings that are required in recurrence propagation. *) -type simple_indeterminate = [`D of var |`O of (var*poly) list |`S of var |`T of Term.t |`V of var] +type simple_indeterminate = [`D of var |`O of (var*poly) list |`O1 of var |`S of var |`T of Term.t |`V of var] (* Weight of monomial as a sum of given weights of (simple) indeterminates. Used in total_deg. *) let total_weight w weight = let rec recW i=i|> @@ -233,7 +234,8 @@ let total_weight w weight = let rec recW i=i|> | A(T(t,_)) -> weight(`T t) | D i -> weight(`D i) | S i -> weight(`S i) - | O f -> weight(`O f) (* sum' w (map(fun(n,fn)-> weight(`O(n,fn))) f) *) + | O f -> weight(`O f) (* sum' w (map(fun(n,fn)-> weight(`O(n,fn))) f) *) + | O1 i -> weight(`O1 i) | X f -> recW f | XD i -> w#plus (weight(`V i)) (weight(`D i)) )) w#o in recW @@ -242,11 +244,11 @@ let total_weight w weight = let rec recW i=i|> let total_deg = total_weight theZ ~=Z.one (* Shapes of indeterminates without parameters. - This is used to reduce the match cases in comparison tiebreaking. We can probably keep this as an internal detail. Nevertheless indeterminate_order is already made a mutable reference for future flexibility. *) -type indeterminate_shape = [`I|`C|`V|`O|`S|`D|`XD|`X|`T] -let indeterminate_order: indeterminate_shape list ref = ref [`I;`C;`V;`X;`O;`S;`D;`XD;`T] + This is used to reduce the match cases in comparison tiebreaking. The order of 5 least indeterminates and of the top `T might be important. We can probably keep this as an internal detail. Nevertheless indeterminate_order is already made a mutable reference for future flexibility. *) +type indeterminate_shape = [`I|`C|`V|`O1|`O|`S|`D|`XD|`X|`T] +let indeterminate_order: indeterminate_shape list ref = ref [`I;`C;`V;`X;`O1;`O;`S;`D;`XD;`T] -let indeterminate_shape = function C _->`C | S _->`S | D _->`D | XD _->`XD | O _->`O | X _->`X | A(V _)->`V | A I->`I | A(T _)->`T +let indeterminate_shape = function C _->`C | S _->`S | D _->`D | XD _->`XD | O _->`O | O1 _->`O1 | X _->`X | A(V _)->`V | A I->`I | A(T _)->`T (* Monomial and other orders TODO What nonstandard invariants the order must satisfy? At least the C(oefficient)s must contribute last because ++ changes them while linearly merging monomial lists instead of full resorting. *) @@ -264,7 +266,7 @@ and tiebreak_by weights = rev %%> lex_list(fun x y -> if xwyw then 1 else match x,y with | A I, A I -> 0 | C x, C y -> Z.((compare***compare) (abs x, x) (abs y, y)) - | D x, D y | S x, S y | XD x, XD y | A(V x), A(V y) -> compare x y + | D x, D y | S x, S y | XD x, XD y | A(V x), A(V y) | O1 x, O1 y -> compare x y | X x, X y -> compare_mono_by weights x y | O x, O y -> lex_list(compare_var *** compare_poly_by weights) x y | A(T(x,_)), A(T(y,_)) -> Term.compare x y @@ -277,7 +279,10 @@ let indeterminate_weights: (op list -> simple_indeterminate -> int list) ref = r (* The main interface to monomial orders, conveniently reversed for sorting maximal monomial first. *) let rev_cmp_mono n m = compare_mono_by !indeterminate_weights m n (* Keep parameters to reread indeterminate_weights! *) -let sort_poly: poly->poly = sort rev_cmp_mono +let sort_poly: poly->poly = sort rev_cmp_mono + +(* Intramonomial order must be stable to avoid reconstructing monomials—only resorting them—when polynomial is retrieved from a clause embedding it. *) +let stable_cmp_mono = compare_mono_by ~= ~=[] (* Some indeterminate weights for common elimination operations *) @@ -306,9 +311,9 @@ and indet_eq x y = x==y or match x,y with | C a, C b -> Z.equal a b | A(T(t,tv)), A(T(s,sv)) -> t==s & if tv=sv then true else failwith("Term "^ Term.to_string t ^" must not be associated with both variables ["^ concat_view "] and [" (CCList.to_string((-^)"")) [tv;sv] ^"]") - | X f, X g -> mono_eq f g + | X f, X g -> mono_eq f g | O f, O g -> CCList.equal(CCPair.equal (=) poly_eq) f g - | a, b -> a = b + | a, b -> a = b (* note: O1∩O := ∅ *) let bit_rotate_right r b = (b lsr r) + (b lsl lnot r) (* for int lacking 1 bit and r>=0 *) @@ -390,8 +395,8 @@ and indet_to_string = function | D i -> subscript(var_name i) | XD i -> "ð"^subscript(var_name i) | S i -> "∑"^superscript(var_name i) -| X m -> mono_to_string m -| O[i,[[A(V j)];[A I]]] when i=j -> String.uppercase(var_name i) +| X m -> mono_to_string m +| O1 i -> String.uppercase(var_name i) | O f -> "{"^ concat_view "" (fun(i,fi)-> superscript(var_name i) ^ poly_view_string fi) f ^"}" let pp_poly = to_formatter poly_to_string @@ -498,10 +503,11 @@ let rec (><) p q = match p,q with let xy = [[x]]><[[y]] in (* Inputs nx and y::m are valid monomials, so if [[x;y]] is too, then simple concatenation puts indeterminates to the right order: *) (if poly_eq xy [[x;y]] then [nx@y::m] - (* Guarantee that all pushing products (A×_ => _×A) are computed before true argument products (_×A) — evaluate right product first to put any A fully right. (Is this certainly correct?) -  TODO The entire product A1×X(An) ends up X(An)×A1 instead of An because there is no other indeterminates keeping the simplification alive. This looks severe. If a workaround is not found, the whole encoding of arguments as A indeterminates should be reworked. Minimally unifiers must special case A. *) - else [n]><(xy><[m])) - ++ ([nx]><[y::m]) ++ (p> _×A) are computed before true argument products (_×A) — evaluate right product first to put any A fully right. +  TODO The entire product A1×X(An) ends up X(An)×A1 instead of An because there is no other indeterminates keeping the simplification alive. This looks severe. If a workaround is not found, the whole encoding of arguments as A indeterminates should be reworked. Minimally unifiers must special case A. +  Potential workaround is to special case short (1×1 factor?) products. Perhaps it suffices to evaluate [[A]]×_ as _×[[A]]. Anyway, correctness of this whole push-first method needs a justification. *) + else [n]><(xy><[m]) + ) ++ ([nx]><[y::m]) ++ (p> [[y;x]] | D i, X f -> [[X f; D i]] ++ x_[f] | XD i, X f -> [[X f; XD i]] ++ x_[f] - | D i, O f -> (if mem_assq i f then f else (i,[var_poly i])::f) (* identity ∘'s in f are implicit *) + | D i, O1 l -> [[y;x]] + | D i, O f -> (if mem_assq i f then f else (i, var_poly i)::f) (* identity ∘'s in f are implicit *) |> map(fun(n,fn)-> x_ fn >< [o f @[D n]]) (* coordinatewise chain rule *) |> fold_left (++) _0 (* sum *) - | XD i, O f -> fold_left(++)_0 (map(fun(n,fn)-> (todo"X fn⁻¹") >< x_ fn >< [o f @[XD n]]) (if mem_assq i f then f else (i,[var_poly i])::f)) (* like previous *) + | XD i, O f -> fold_left(++)_0 (map(fun(n,fn)-> (todo"X fn⁻¹") >< x_ fn >< [o f @[XD n]]) (if mem_assq i f then f else (i, var_poly i)::f)) (* like previous *) | D i, XD j when i=j -> [[XD i; D i]; [D i]] - | O f, X g -> x_[g] >< [[O f]] + | (O _ | O1 _), X g -> x_[g] >< [[x]] | X(S i ::f), S j when i=j -> let _Si_Xf = [[S i]]><[[S i]]) ++ [[S i; X(S i :: f)]] ++ _Si_Xf + | O1 i, S j when i=j -> [[S i]] ++ const_op_poly Z.one | O[i,f], S j when i=j -> let c = const_mono f in map((@)(o[i,f--const_eq_poly c])) ([[S i]] ++ const_op_poly c) (* | O f, S i -> [o(filter((=)i % fst) f)] >< S i >< [o(filter((!=)i % fst) f)] (* TODO swap's semantics *) *) - | S l, O[i,[[A(V j)];[A I]]] when i=j&i=l -> [[S i]; C Z.minus_one :: eval_at Z.zero ~var:i; []] - | S l, O[i,[[A(V j)];[A I]]] when i=j -> [[y;x]] + | S l, O1 i when i=l -> [[S i]; C Z.minus_one :: eval_at Z.zero ~var:i; []] + | S l, O1 i -> [[y;x]] | S l, (X[A(V i)] | D i | XD i) when l!=i -> [[y;x]] - | O[i,[[C o]]], S l when i=l -> assert(is0 o); [[x]] - | O[i,[[C c; A I]]], S l when i=l -> Z.(if c < zero - then map(fun n -> eval_at~var:i (of_int n + c)) (range' 0 (Stdlib.abs(to_int_exn c))) - else map(fun n -> eval_at~var:i (of_int n)) (range' 0 (to_int_exn c))) - | O[i,[[A(V j)];[A I]]], O[l,[[A(V k)];[A I]]] when i=j & l=k & i>l -> [[y;x]] - | O f, O g when is_multishift x & is_multishift y & rev_cmp_mono [x] [y] <0 -> [[y;x]] - | O f, O g when not(is_multishift x) -> [o(map(map_snd((><)[[x]]))(*∘f*)g @ filter(fun(i,_) -> not(mem i (map fst g)))(*implicit defaults*)f)] + | O[i,[[C o]]], S j when i=j -> assert(is0 o); [[x]] + | O[i,[[C c; A I]]], S j when i=j -> map Z.(fun n -> eval_at~var:i (of_int n + min c zero)) (range' 0 (abs(Z.to_int_exn c))) + | O f, O1 i when not(is_shift x) -> [[x]]><[o[i, var_poly i ~plus:Z.one]] (*apply below*) + | O f, O g when not(is_shift x) -> [o(map(map_snd((><)[[x]]))(*∘f*)g @ filter(fun(i,_) -> not(mem i (map fst g)))(*implicit defaults*)f)] + | x, y when is_shift x & is_shift y & stable_cmp_mono [x] [y] > 0 -> [[y;x]] | D i, D l | XD i, XD l | S i, S l | X[A(V i)], X[A(V l)] when i>l -> [[y;x]] - | X f, X g when rev_cmp_mono f g < 0 -> [[y;x]] (* Assumes commutative product! *) - | X f, A _ when rev_cmp_mono f [y] < 0 -> mul_indet[[y]]><[f] (* Assumes commutative product! *) + | X f, X g when stable_cmp_mono f g > 0 -> [[y;x]] (* Assumes commutative product! *) + | X f, A _ when stable_cmp_mono f [y] > 0 -> mul_indet[[y]]><[f] (* Assumes commutative product! *) | D _, A I -> [] | D i, A(V n) -> const_eq_poly Z.(if i=n then one else zero) - | O f, A I -> const_eq_poly Z.one + | (O _ | O1 _), A I -> const_eq_poly Z.one + | O1 i, A(V j) when i=j -> var_poly i ~plus:Z.one + | O1 i, A(V l) -> [[y]] | O f, A(V n) -> get_or~default:[[y]] (assq_opt n f) | O f, A(T(_,v)) -> [o(filter(fun(i,_)-> mem i v) f) @ [y]] (* No recursive call to >< in order to avoid endless loop. *) + | O1 i, A(T(_,v)) when not(mem i v) -> [[y]] | A _, A _ -> invalid_argument("indeterminate_product ("^ indet_to_string x ^") ("^ indet_to_string y ^")") | A _, y -> [[y;x]] (* Push A from left to right. Caller must push A fully right before _,A multiplication! *) | x, y -> [[x;y]] @@ -568,6 +577,9 @@ end (* Law product(a@b) = product a >< product b requires to choose to use const_op_poly. *) let product = fold_left (><) (const_op_poly Z.one) +[@@@warning "-52"](* Allow match Failure"hd" but let's check it works: *) +let()= try hd[] with Failure"hd"->() | e->print_endline("Invalid build: Fix RecurrencePolynomial.unifiers to catch "^ Printexc.to_string e) + (* Unification and superposition *) let rec unifiers m' n' = @@ -579,13 +591,13 @@ let rec unifiers m' n' = | x::m, x'::n when indet_eq x x' -> loop(m,n) | x::m, y::n when join_normalizes x y -> (* This'd be faster if monomials were encoded in reverse. Only downside would be unintuitivity. *) - (match rev(hd([[y]]><[rev(x::m)])) with + (match rev(hd([[y]]><[rev(x::m)])) with (* note: hd({x↦0}·xMₓ) fails but M₀=... could be useful *) | y'::xm when indet_eq y y' -> let u,v = loop(xm,n) in u@[y], v | _ -> raise Exit) | m, y::n when m=[] or join_normalizes y (hd m) -> CCPair.swap(loop(y::n, m)) | _ -> raise Exit in - try Some(loop(rev m', rev n')) with Exit -> None + try Some(loop(rev m', rev n')) with Exit | Failure"hd" -> None let lead_unifiers = curry(function x::_, y::_ -> unifiers x y | _ -> None) @@ -617,12 +629,12 @@ end) (* Features for a rewriting index testing various sums of operator degrees. Only for !=0 polynomials. *) let default_features() = (* () because of type variables *) - let sum value = sum_list % map value % hd in - [(* TODO double check that these are correctly increasing *) + let sum value = sum_list % map value % hd in [ "total degree", sum~=1; - "shift degree", sum(function O _ -> 1 | _ -> 0); + "shift degree", sum(function O1 _ -> 1 | _ -> 0); "coefficient degree", sum(function X _ -> 1 | _ -> 0); - "1ˢᵗ var. degree", sum(function O[0,_] | X[A(V 0)] -> 1 | _ -> 0); + "multishift degree", sum(function O _ -> 1 | _ -> 0); + (* "1ˢᵗ var. degree", sum(function O[0,_] | X[A(V 0)] -> 1 | _ -> 0); *) (* then: multiset of indeterminates... except that only ID multisets are supported *) ] @@ -641,10 +653,9 @@ and free_variables p' = Int_set.(let rec monoFV = function | x::m -> union (monoFV m) (match x with | O f -> assert false (* was prior case *) | C _ | A I -> empty - (* Do operators make explicit all implicit dependencies in argument terms? If not, below is wrong! *) - | A(V i) | S i | D i | XD i -> singleton i + | O1 i | A(V i) | S i | D i | XD i -> singleton i | X f -> monoFV f - | A(T(_,v)) -> of_list v (*map_or ~default:empty free_variables (poly_of_term t)*) + | A(T(_,v)) -> of_list v ) in union_map monoFV p') @@ -653,7 +664,7 @@ let _=debug_free_variables:=free_variables' (* Output ϱ,σ,raw. Renaming substitution indeterminate ϱ satisfies dom ϱ = vs\taken and img ϱ ∩ vs∪taken = ∅. Substitution indeterminate σ undoes ϱ meaning [σ]><[ϱ]>

incr(force m); (c, !(force m))::pairs) collide []) with | [] -> [], [], [] @@ -668,7 +679,7 @@ let view_affine f = try f|>map(fun(i,p) -> let put vs sh = (* i ↦ vs+sh = variable list + shift constant *) shift.(i) <- sh; - if not(vs=[var_poly i]) then (* identity variable mapping gets encoded by [||] always *) + if not(vs = var_poly i) then (* identity variable mapping gets encoded by [||] always *) matrix.(i) <- fold_left (fun row -> function | [A(V n)] -> row.(n) <- 1; row | [C a; A(V n)] -> row.(n) <- Z.to_int_exn a; row @@ -729,7 +740,7 @@ let to_poly_poly: (poly * op list) list -> poly = (* Turn general formula into a recurrence in operator polynomial representation by embedding other parts into argument terms. *) let oper_coef_view: poly -> poly = to_poly_poly % coef_view(function | C _ | X[A(V _)] -> true - | x -> is_multishift x) + | x -> is_shift x) (* Parsing polynomials from strings—primarily for testing *) diff --git a/src/prover_phases/TypeTests.ml b/src/prover_phases/TypeTests.ml index b4a586b21..dcae4fa21 100755 --- a/src/prover_phases/TypeTests.ml +++ b/src/prover_phases/TypeTests.ml @@ -191,6 +191,7 @@ and indeterminate x = union 0 [ [int]; [int]; [monomial]; + [int]; [list(tuple[int;polynomial])]] x and op_atom x = union 1 [[int]; [term; list int]] x @@ -297,6 +298,9 @@ add_pp exception' Printexc.(fun e -> "("^ clever_view "," str (tl(fields e)) ^")" else ""); +(* low priority *) +add_pp indeterminate (digits_in wide % RecurrencePolynomial.indet_to_string); + add_pp decimal string_of_float; (* Quote number and invisible strings. *) add_pp string (fun s -> if None != int_of_string_opt(String.trim s ^ "0") then "“"^s^"”" else s); diff --git a/src/prover_phases/summation_equality.ml b/src/prover_phases/summation_equality.ml index b042ad2a2..5db2f542a 100755 --- a/src/prover_phases/summation_equality.ml +++ b/src/prover_phases/summation_equality.ml @@ -255,7 +255,7 @@ let filter_map_recurrences map_poly = Iter.filter_map(fun c -> with Invalid_argument _ -> None) (* Filter those clauses that have eligible polynomial whose every term M f, where term f represents an expression from polylist, has normal operator monomial M (that consist only of multipliers and 1-shifts). Moreover the leading term must have such form M f. After the filtering, unembed all other polynomials outside polylist. - Notes: The ordering of the embedded polynomial term f can be problematic. The polynomial structure of f does not automatically contribute to the ordering. Hence requiring, that M f leads, silently discards recurrences that forgot to take f into account in the ordering. However at least propagation to addition and affine forms relies to the presence of the requirement that M f leads. Now try making leading requirement optional via parameter. *) + Notes: The ordering of the embedded polynomial term f can be problematic. The polynomial structure of f does not automatically contribute to the ordering. Hence requiring, that M f leads, silently discards recurrences that forgot to take f into account in the ordering. However at least propagation to addition and affine forms relies to the presence of the requirement that M f leads. Hence leading requirement is made optional via parameter. *) let filter_recurrences_of ?(lead=true) polylist = filter_map_recurrences R.(fun p -> if_~= (let wanted_terms = p |> map_monomials(fun m -> match terms_in[m] with | [t] when mem ~eq:(CCOpt.equal poly_eq) (poly_of_term t) (map CCOpt.pure polylist) -> [m] @@ -289,12 +289,13 @@ let add_new_rec p c = PolyMap.add recurrence_table p let rec propagate_recurrences_to f = match PolyMap.find_opt recurrence_table f with | Some r -> r | None -> - let r = Iter.to_rev_list(match "propagating to "| propagate_oper_affine f - | [X q :: p] -> propagate_times [q] [p] - | [S i :: p] -> propagate_sum i [p] - | [O s :: p] -> propagate_subst s [p] - | [C _ :: p] -> propagate_const f + | [X q :: p] -> propagate_times [q] [p] + | [C _ :: p] -> propagate_const f + | [S i :: p] -> propagate_sum i [p] + | [O s :: p] -> propagate_subst s [p] + | [O1 i :: p] -> Iter.of_list(propagate_recurrences_to([o[i, var_poly i ~plus:Z.one]]><[p])) | _ -> Iter.empty) in PolyMap.add recurrence_table f r; @@ -324,30 +325,30 @@ and propagate_times f g = let rename, merge, _ = R.rename_apart ~taken:(R.free_variables f) (R.free_variables g) in (* 2. create Rᶠ·ϱg and f·ϱRᵍ *) let disjoint_recurrences = R.( - map(map_poly_in_clause(fun r -> r> mul_indet r><[rename]> mul_indet f><[rename]> Iter.of_list disjoint_recurrences (* 3. propagate to substitution σ(f·ϱg) when σ!=id *) | [O m] -> - let f_x_g' = R.(mul_indet f><[rename]>< g) in + let f_x_g' = "product breakdown "^str[R.o m]|<[rename]>< g) in PolyMap.add recurrence_table f_x_g' disjoint_recurrences; propagate_subst m f_x_g' | _ -> assert false (* impossible result from R.rename_apart *) and propagate_sum i f = let is_f t = R.(CCOpt.equal poly_eq (Some f) (poly_of_term t)) in - let sum_blocker = function (* gives elimination priorities: [] is good, [1] is bad *) - |`T t when not(is_f t) -> [] - |`V v when v!=i -> [] - |`O[u, R.[[A(V v)];[A I]]] when v=u -> [] - | _ -> [1] + let sum_blocker = function (* gives elimination priorities: 0 is good, 1 is bad *) + |`T t when not(is_f t) -> 0 + |`V v when v!=i -> 0 + |`O1 _ -> 0 + | _ -> 1 in let sumf = R.(let _,sumf,_ = poly_as_lit_term_id([[S i]]>< of_term f_term) -- sumf) in Iter.of_list(propagate_recurrences_to f) - |> saturate_with_order(R.elim_indeterminate' sum_blocker) + |> saturate_with_order(R.elim_indeterminate sum_blocker) |> Iter.map(map_poly_in_clause R.((><)[[S i]])) (* Replace each ∑ᵢf by the embedding sumf by rewriting with temporary polynomial ∑ᵢf-sumf. *) |> Iter.cons embed_sumf_rewriter @@ -365,7 +366,7 @@ and propagate_subst s f = (* 4. replace each compound shift by a 1-shift, and substitute multipliers *) let _,f_term,_ = R.poly_as_lit_term_id f in let _,sf_term,_ = R.(poly_as_lit_term_id([o s]> (* If 𝕊ⱼ=Sⱼ, we skip it, which makes saturation faster, but primarily this is to dodge the issue of telling 𝕊ⱼ and Sⱼ apart. *) let changedShift = filter(fun j -> exists R.(fun i -> m@.(i,j) != if i=j then 1 else 0) (Int_set.to_list dom)) in - let multishifts_and_equations = changedShift(Int_set.to_list(R.rangeO s)) |> map R.(fun j -> + let multishifts_and_equations = (*changedShift*)(Int_set.to_list(R.rangeO s)) |> map R.(fun j -> let on_dom f = map f (Int_set.to_list dom) in (* 𝕊ⱼ = ∏ᵢ Sᵢ^mᵢⱼ = O[0,m₀ⱼ;...;i,mᵢⱼ;...] where j runs over range and i over domain *) - let ss_j = hd(o(on_dom(fun i -> i, [var_poly i]++const_eq_poly(Z.of_int(m@.(i,j)))))) in - (* TODO Recurrence polynomial data structure needs an additional marker to distinguish compound shifts from ordinary ones in all corner cases including permutations. -  We can tolerate a confusion between single and multi for a shift w.r.t. a new variable. This relaxation is good to keep in mind when transforming multishifts to 1-shifts. *) - let ss_j = if not(is1shift ss_j) then ss_j - else if not(Int_set.mem j dom) then shift j (* use final form immediately *) - else failwith("Unimplemented: "^ string_of_int j^"ᵗʰ compound shift cannot be distinguished from 1-shift when propagating to substitution "^ poly_to_string[o s] ^" of "^ poly_to_string f) in + let ss_j = hd(o(on_dom(fun i -> i, var_poly i ~plus:(Z.of_int(m@.(i,j)))))) in let eq_j = product(on_dom(fun i -> pow' poly_alg [[shift i]] (max 0 (m@.(i,j))))) -- product([[ss_j]] :: on_dom(fun i -> pow' poly_alg [[shift i]] (- min 0 (m@.(i,j))))) in ((ss_j, shift j), j), eq_j ) in (* We must eliminate all domain shifts except ones skipped above: dom\( rangeO s \ {j | ∃ ss_j} ) *) - let elimIndices = Int_set.(diff dom (diff (R.rangeO s) (of_list(List.map(snd%fst) multishifts_and_equations)))) in + let elimIndices = Int_set.(diff dom (diff (R.rangeO s) (of_list(List.map(snd%fst) multishifts_and_equations)))) in + let elimIndices = dom in (* fixed ✓; TODO inline *) (* * * * Clause prosessing chain: turn recurrences of f to ones of “s'f”, add 𝕊=∏S, eliminate S, push ∘s i.e. map 𝕊ⱼ↦Sⱼ, and filter *) propagate_recurrences_to f |> map(map_poly_in_clause R.(map_submonomials(fun n -> CCOpt.if_~=(poly_eq f [n]) s'f))) |> Iter.of_list (* Above is undone via s'f_term ↦ sf_term at substitution push. *) |> Iter.append(Iter.of_list(map (definitional_poly_clause % snd) multishifts_and_equations)) - |> saturate_with_order(fun m' -> function - |`O[i,R.[[A(V j)];[A I]]] when i=j & Int_set.mem i elimIndices -> - (* Eliminate 1-shifts ...except that multishift could be simplified to 1-shift in case an excess argument term does not depend on some of the multishifted variables—a valid result of such simplification won't be penaliced. *) - if multishifts_and_equations |> exists R.(function(((O ss,_),_),_)-> (* ∃𝕊 *) - Int_set.(match assq_opt i ss with Some[[A(V j)];[A I]] when i=j -> (* 𝕊i = i+1 *) - equal (of_list[i]) (inter (free_variables[m']) (of_list(List.map fst ss))) (* Sᵢ goes as well *) - |_->false) |_->false) - then [] else [1] - | _ -> []) + |>((|<)"pre saturation") + |> saturate_with_order R.(elim_indeterminate(function`O1 i when Int_set.mem i elimIndices -> 1 |_-> 0)) + |>((|<)"post saturation") |> Iter.filter_map(fun c -> try Some(c |> map_poly_in_clause R.(fun p -> let cache_t_to_st = HT.create 4 in let p = if equational p then p else p>< of_term s'f_term in @@ -425,14 +416,14 @@ and propagate_subst s f = HT.add cache_t_to_st t st; `Go,st (* Replace Mᵢ=X[A(V i)] by ∑ⱼmᵢⱼMⱼ. *) | X[A(V i)] -> `Go, fold_left (++) _0 (map(fun j -> const_op_poly(Z.of_int(m@.(i,j))) >< [[mul_var j]]) (Int_set.to_list(rangeO s))) - (* Discard clauses still containing shifts that were to be eliminated. Since elimIndices ⊆ dom, we keep shifts of new variables that the below case interpretates as multishifts that need no further transforming. *) - | O[i,[[A(V j)];[A I]]]as x when i=j & Int_set.mem i elimIndices -> raise Exit - | O[i,[[A(V j)];[A I]]]as x when i=j -> `Go,[[x]] + (* Discard clauses still containing shifts that were to be eliminated. Pass commuting shifts—but aren't the rest also bad and to be eliminated? TODO *) + | O1 i when Int_set.mem i elimIndices -> raise Exit + | O1 i as x when not(Int_set.mem i (rangeO s)) -> `Go,[[x]] (* Replace 𝕊ⱼ by Sⱼ by looking it up from multishifts_and_equations. *) | O _ as x -> (match assoc_opt ~eq:indet_eq x (map(fst%fst) multishifts_and_equations) with | Some sx -> `Go, [[sx]] | None -> `End, [o s]><[upcoming]) - | _ -> `End, [o s]><[upcoming] + | _ -> `End, [o s]><[upcoming] in transf)))) with Exit -> None) |> filter_recurrences_of~lead:false [get_exn(R.poly_of_term sf_term)(* safe by definition of sf_term *)] @@ -446,27 +437,12 @@ let declare_recurrence r = add_new_rec let sum_equality_inference clause = try (* for testing ↓ *) let (!) = R.poly_of_string in - let eq0' p = make_clause (map R.polyliteral p) ~=Proof.Step.trivial in - let split_or k d s = match String.split_on_char k s with - | [a;b] -> a,b | [a] -> if k='.' then d,a else a,d | _ -> raise Exit in - let eq0 ss = eq0' R.[fold_left (++) _0 (List.map(fun cmt -> - let c,mt = split_or '.' "1" (String.trim cmt) in - let m,t = split_or '\'' "" mt in - Z.of_string c *: poly_of_string m >< of_term~vars:(todo"vars in eq0")(have t [] int) - ) (String.split_on_char '+' ss))] in - (* declare_recurrence !"NNf-Nf-f"; declare_recurrence !"Ng-ng-g"; propagate_recurrences_to !"nf"; (* OK *) propagate_recurrences_to !"g+f"; (* OK *) propagate_recurrences_to !"g+nf"; (* diverge? *) - propagate_recurrences_to !"∑ᵐb"; (* OK *) - - propagate_recurrences_to !"{ᵐm-n-1}b"; (* OK *) - propagate_recurrences_to !"∑ⁿ{ᵐm-n-1}b"; (* OK *) - propagate_recurrences_to !"{ⁿm}∑ⁿ{ᵐm-n-1}b"; (* OK *) - propagate_recurrences_to !"{ⁿm}∑ⁿ{ᵐm-n-1}b - ∑ᵐb"; (* OK *) *) ["z","xn"; "q","x"; "b","mn"; "c","mn"; "f","m"; "g","mn"; "γ","mn"] |> map(uncurry(HS.add R.variable_dependency)); @@ -474,6 +450,7 @@ let sum_equality_inference clause = try declare_recurrence !"Nz-xz "; (* zₓₙ = xⁿ *) declare_recurrence !"MMf-Mf-f "; (* fₘ = mᵗʰ Fibonacci *) declare_recurrence !"xXq+Xq-q "; (* qₓ = x!⁻¹ *) + declare_recurrence !"{ˣ0}q-1 "; (* q₀ = 1 *) declare_recurrence !"mMb-nMb+Mb-mb-b "; (* binomial coefficient: *) declare_recurrence !"nNb+Nb-mb-nb "; (* bₘₙ = (ₙͫ ) *) declare_recurrence !"MNc-nNc-Nc-c "; (* Stirling cₘₙ = {ₙͫ } *) @@ -488,22 +465,23 @@ let sum_equality_inference clause = try "{ˣx+y}{ⁿm}z - {ⁿm+1}∑ⁿBZ{ˣy}{ⁿm-n}z ";(*6 binomial *) "{ᵐn+1}f - {ᵐn+1}∑ᵐ{ⁿn-m}b ";(*7 Fibonacci *) "γ - {ˣm}∑ˣ{ᵐm-1-x}g ";(*8 presented *) - "0 - {ᵐm-1-x}g ";(*9 debug *) + "0 - F{ˣm}q ";(*9 debug *) |]in(* (p,)r,e,i: ✓ - c,b,A,F,S: leviää etenkin bₘₙ kanssa (? ja sijoituksille jäi aikoinaan kaavoja löytymättä ?) + c,b,A,F,S: leviää *) let rec go() = print_string"tutki: "; init_rec_table(); - let cmd = read_line() in - if String.length cmd == 1 then( - let p = (!)tests.(int_of_string cmd) in + let tutki str = + let p = (!)str in print_endline("Tutkitaan " ^ R.poly_to_string p); ctrl_C_stoppable(fun()-> propagate_recurrences_to p; - ~ + ~ let p,p' = poly_of_string@@(p,p') in print_endline(match lead_unifiers p p' with | None -> "Samastumattomat "^ poly_to_string p ^", "^ poly_to_string p' @@ -512,95 +490,15 @@ let sum_equality_inference clause = try ^match CCOpt.or_~else_:(leadrewrite p p')(leadrewrite p' p) with | Some r -> "rw. "^ poly_to_string r | None -> "") - | x -> print_endline("Paloja jaettaessa pilkusta pitää tulla 2 eikä " ^ string_of_int(length x))); + | [""] -> exit 0 + | [s] -> tutki s + | x -> print_endline("Madosta jaettaessa pitää paloja tulla max 2 eikä " ^ string_of_int(length x))); go() - in go(); - exit 1; - let seeSatur pp = ((~<) % Iter.to_list % saturate_with_order~= ~=[1] % Iter.of_list % map eq0) pp in - seeSatur["vvvvv"; "vv-1"]; - seeSatur["yyx-x-y"; "yxx-x-1"]; - seeSatur[ - "3vvvvvvvvvvvvvvvvvvv"; "3vvvvvvvvv + 1"; - (* eq0"x + y-v"; eq0"xx + yy-vv"; *) - (* eq0"xx + 3x + 1"; eq0"yy + 3y + 1"; eq0"xxxxx + yyyyy"; *) - - (* eq0"2nN-m + 3"; eq0"NM + 2m"; *) - (* eq0"2nnNN-nN + 3"; eq0"NNN + 2nN"; *) - - (* eq0"Xb-b-Xf"; eq0"h-b + g"; *) - (* eq0"Xg-g-Xf"; *) - (* eq0"-XXg + g + XXf + Xf"; *) - - (* eq0"Yb-2b"; eq0"-4g + yyb + yb"; *) - (* eq0"xXb-yXb + Xb-xb-b"; eq0"yYb + Yb-xb + yb"; eq0"f-yyb"; *) - (* Change priority for ↓ *) - (* eq0"xXf-yXf + Xf-xf-f"; eq0"yyYf-yxf + yyf-xf + yf"; *) - - (* eq0"-XxxX∑f+3xxX∑f+9xX∑f+6X∑f-2xx∑f-6x∑f-4∑f"; eq0"xXg-2xg-4g"; eq0"h-∑f+g"; *) - - ]; - exit 1 + in go() (* tl(tl[clause;clause]) *) with e -> print_endline Printexc.((*get_backtrace() ^"\n"^ *)match e with Failure m -> m | e -> to_string e); exit 1 -(* Fibonacci ongelmatulosteotos: -summation_equality line 292 ≣̲̇26 propagating to {ᵐn＋１͘}fₘ -CCOption.pp line 9 ≣̲̇49 rw.M－N - NMfₘ－Mfₘ－fₘ -CCOption.pp line 9 ≣̲̇50 rw.M－N - -Mfₘ＋N²fₘ－fₘ -CCOption.pp line 9 ≣̲̇50 rw.M－N - N²fₘ－Nfₘ－fₘ -RecurrencePolynomial line 605 ≣̲̇48 p̲p̲. -NMfₘ－Mfₘ＋N³fₘ -CCOption.pp line 9 ≣̲̇48 rw.M－N - -Mfₘ＋N³fₘ－N²fₘ -CCOption.pp line 9 ≣̲̇48 rw.M－N - N³fₘ－N²fₘ－Nfₘ -CCOption.pp line 9 ≣̲̇49 rw.N²fₘ－Nfₘ－fₘ - ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ -Nfₘ＋fₘ -CCOption.pp line 9 ≣̲̇49 rw.-Nfₘ＋fₘ - -Nfₘ -CCOption.pp line 9 ≣̲̇49 rw.-Nfₘ＋fₘ - -fₘ -RecurrencePolynomial line 605 ≣̲̇48 p̲p̲. Mfₘ－N²fₘ -CCOption.pp line 9 ≣̲̇47 rw.M－N - -N²fₘ＋Nfₘ -CCOption.pp line 9 ≣̲̇48 rw.-Nfₘ＋fₘ - Nfₘ－fₘ -CCOption.pp line 9 ≣̲̇49 rw.-fₘ - -Nfₘ＋２fₘ -CCOption.pp line 9 ≣̲̇49 rw.-Nfₘ＋fₘ - fₘ -CCOption.pp line 9 ≣̲̇50 rw.-fₘ - 0 -RecurrencePolynomial line 605 ≣̲̇48 p̲p̲. -Nfₘ -CCOption.pp line 9 ≣̲̇47 rw.-fₘ - -Nfₘ＋fₘ -CCOption.pp line 9 ≣̲̇48 rw.-fₘ - -Nfₘ＋２fₘ -CCOption.pp line 9 ≣̲̇49 rw.-fₘ - -Nfₘ＋３fₘ -CCOption.pp line 9 ≣̲̇50 rw.-fₘ - -Nfₘ＋４fₘ -*) -(* Stirling ongelmatulosteotos: -summation_equality line 292 ≣̲̇28 propagating to {ⁿx}cₙₘ -CCOption.pp line 9 ≣̲̇51 rw.N－X - XMcₙₘ－nNcₙₘ－Ncₙₘ－cₙₘ -RecurrencePolynomial line 605 ≣̲̇50 p̲p̲. -nN²cₙₘ－２N²cₙₘ＋X²Mcₙₘ－Ncₙₘ -CCOption.pp line 9 ≣̲̇50 rw.N－X - -２N²cₙₘ＋X²Mcₙₘ－nXNcₙₘ－Ncₙₘ -CCOption.pp line 9 ≣̲̇51 rw.N－X - X²Mcₙₘ－nXNcₙₘ－２XNcₙₘ－Ncₙₘ -CCOption.pp line 9 ≣̲̇51 rw.XMcₙₘ－nNcₙₘ－Ncₙₘ－cₙₘ - -XNcₙₘ－Ncₙₘ＋cₙₘ -CCOption.pp line 9 ≣̲̇52 rw.N－X - -Ncₙₘ－X²cₙₘ＋cₙₘ -CCOption.pp line 9 ≣̲̇52 rw.N－X - -X²cₙₘ－Xcₙₘ＋cₙₘ -*) - (* Setup to do when MakeSumSolver(...) is called. *);; MainEnv.add_unary_inf "recurrences for ∑" sum_equality_inference end