123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345 |
- % ----------------------------------------------------------------------
- % $Id: acfsfmisc.red,v 1.7 1999/04/13 13:05:33 sturm Exp $
- % ----------------------------------------------------------------------
- % Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
- % ----------------------------------------------------------------------
- % $Log: acfsfmisc.red,v $
- % Revision 1.7 1999/04/13 13:05:33 sturm
- % Minor corrections in comments.
- %
- % Revision 1.6 1999/04/12 09:25:48 sturm
- % Removed procedure acfsf_canegrel and acfsf_anegrel.
- % Updated comments for exported procedures.
- %
- % Revision 1.5 1999/04/01 11:27:16 dolzmann
- % Added comment for acfsf_structat.
- %
- % Revision 1.4 1999/03/23 08:19:21 dolzmann
- % Changed copyright information.
- % Added fluids for the rcsid of the file and for the copyright information.
- %
- % Revision 1.3 1999/03/21 13:40:39 dolzmann
- % Added procedure acfsf_canegrel and acfsf_anegrel which were commented out.
- %
- % Revision 1.2 1997/08/24 16:18:40 sturm
- % Added service rl_surep with black box rl_multsurep.
- % Added service rl_siaddatl.
- %
- % Revision 1.1 1997/08/22 17:30:40 sturm
- % Created an acfsf context based on ofsf.
- %
- % ----------------------------------------------------------------------
- lisp <<
- fluid '(acfsf_misc_rcsid!* acfsf_misc_copyright!*);
- acfsf_misc_rcsid!* :=
- "$Id: acfsfmisc.red,v 1.7 1999/04/13 13:05:33 sturm Exp $";
- acfsf_misc_copyright!* := "Copyright (c) 1995-1999 A. Dolzmann and T. Sturm"
- >>;
- module acfsfmisc;
- % Algebraically closed field standard form other. Submodule of [acfsf].
- procedure acfsf_termprint(u);
- % Algebraically closed field term print. [u] is a
- % term. The return value is not specified. Prints [u] AM-like.
- <<
- sqprint !*f2q u where !*nat=nil;
- ioto_prin2 nil
- >>;
- procedure acfsf_clnegrel(r,flg);
- % Algebraically closed field conditionally logically negate
- % relation. [r] is a relation. Returns for [flg] equal to [nil] a
- % relation $R$ such that for terms $t_1$, $t_2$ we have
- % $R(t_1,t_2)$ equivalent to $\lnot [r](t_1,t_2)$. Returns [r] for
- % non-[nil] [flg].
- if flg then r else acfsf_lnegrel r;
- procedure acfsf_lnegrel(r);
- % Algebraically closed field logically negate relation. [r] is a
- % relation. Returns a relation $R$ such that for terms $t_1$, $t_2$
- % we have $R(t_1,t_2)$ equivalent to $\lnot [r](t_1,t_2)$.
- if r eq 'equal then 'neq
- else if r eq 'neq then 'equal
- else rederr {"acfsf_lnegrel: unknown operator ",r};
- procedure acfsf_fctrat(atf);
- % Algebraically closed field factorize atomic formula. [atf] is an
- % atomic formula. Returns the factorized left hand side of [atf] as
- % a list $(...,(f_i . n_i),...)$, where the $f_i$ are the factors
- % as SF's and the $n_i$ are the corresponding multiplicities. The
- % integer content is dropped.
- cdr fctrf acfsf_arg2l atf;
- procedure acfsf_negateat(f);
- % Algebraically closed field negate atomic formula. [f] is an
- % atomic formula. Returns an atomic formula equivalent to $\lnot
- % [f]$.
- acfsf_mkn(acfsf_lnegrel acfsf_op f,acfsf_argn f);
- procedure acfsf_varlat(atform);
- % Algebraically closed field variable list of atomic formula.
- % [atform] is an atomic formula. Returns the set of variables
- % contained in [atform] as a list.
- kernels acfsf_arg2l(atform);
- procedure acfsf_varsubstat(atf,new,old);
- % Algebraically closed substitute variable for variable in atomic
- % formula. [atf] is an atomic formula; [new] and [old] are
- % variables. Returns [atf] with [new] substituted for [old].
- acfsf_0mk2(acfsf_op atf,numr subf(acfsf_arg2l atf,{old . new}));
- procedure acfsf_ordatp(a1,a2);
- % Algebraically closed field order predicate for atomic formulas.
- % [a1] and [a2] are atomic formulas. Returns [T] iff [a1] is
- % strictly less than [a2] wrt. some syntactical ordering; returns
- % [nil] else. The specification that [nil] is returned if
- % $[a1]=[a2]$ is used in [acfsf_subsumeandcut].
- begin scalar lhs1,lhs2;
- lhs1 := acfsf_arg2l a1;
- lhs2 := acfsf_arg2l a2;
- if lhs1 neq lhs2 then return ordp(lhs1,lhs2);
- return acfsf_ordrelp(acfsf_op a1,acfsf_op a2)
- end;
- procedure acfsf_ordrelp(r1,r2);
- % Algebraically closed field standard form relation order
- % predicate. [r1] and [r2] are acfsf-relations. Returns a [T] iff
- % $[r1] <= [r2]$.
- r1 eq r2 or r1 eq 'equal;
- procedure acfsf_a2cdl(atml);
- % Algebraically closed field atomic formulas to case distinction
- % lists. [atml] is a multiplicity list of atomic formulas. Returns
- % a list $(...,(t_i = 0, t_i \neq 0),...)$ of case distinctions
- % lists, where the $t_i$ are the right hand side terms of the
- % atomic formulas in [atml].
- begin scalar x;
- return for each pr in atml collect <<
- x := acfsf_arg2l car pr;
- {acfsf_0mk2('equal,x),acfsf_0mk2('neq,x)}
- >>
- end;
- procedure acfsf_t2cdl(term);
- % Algebraically closed field term to case distinction list. [term]
- % is a term. Returns a case distinction list $([term] = 0, [term]
- % \neq 0)$ wrt. [term].
- {acfsf_0mk2('equal,term),acfsf_0mk2('neq,term)};
- procedure acfsf_subat(al,f);
- % Algebraically closed field substitute into atomic formula. [al]
- % is an ALIST $(..., (v_i . t_i), ...)$, where the $v_i$ are
- % kernels, and the $t_i$ are Lisp prefix terms; [f] is an atomic
- % formula. Returns [f] with $t_i$ substituted for each occurrence
- % of $v_i$. The $t_i$ must be such that the substitution does not
- % yield parametric denominators.
- begin scalar nlhs;
- nlhs := subf(acfsf_arg2l f,al);
- if not domainp denr nlhs then
- rederr "parametric denominator after substitution";
- return acfsf_0mk2(acfsf_op f,numr nlhs)
- end;
- procedure acfsf_subalchk(al);
- % Algebraically closed field substitution ALIST check. [al] is an
- % ALIST $(..., (v_i . t_i), ...)$, where the $v_i$ are kernels, and
- % the $t_i$ are Lisp prefix terms. The return value is unspecified.
- % Raises an error if some $t_i$ contains a parametric denominator.
- for each x in al do
- if not domainp denr simp cdr x then
- rederr "parametric denominator in substituted term";
- procedure acfsf_eqnrhskernels(x);
- % Algebraically closed field equation right hand side kernels. [x]
- % is an equation. Returns the set of kernels contained in the right
- % hand side of [x] as a list.
- nconc(kernels numr w,kernels denr w) where w=simp cdr x;
- procedure acfsf_getineq(f,bvl);
- % Algebraically closed field generate theory get inequalities. [f]
- % is a formula; [bvl] is a list of variables. Returns the list of
- % all inequalities occuring in [f] that do not contain any of the
- % variables in [bvl].
- begin scalar atml,atf,cdl;
- atml := cl_atml f;
- while atml do <<
- atf := caar atml;
- atml := cdr atml;
- if acfsf_op atf eq 'neq and
- null intersection(bvl, kernels acfsf_arg2l atf) then
- cdl := atf . cdl
- >>;
- return cdl
- end;
- procedure acfsf_structat(at,al);
- % Algebraically closed field structure of an atomic formula. [at]
- % is an atomic formula $R(t,0)$; [al] is an ALIST. Returns an
- % atomic formula. [al] is of the form $(..., (t_i . v_i), ...)$,
- % where the $t_i$ are SF's and the $v_i$ are variables. The left
- % hand side $t$ of [at] matches one of the $t_i$ in [al]. Returns
- % the atomic formula $R(v_i,0)$.
- begin scalar lhs;
- lhs := acfsf_arg2l at;
- if domainp lhs then
- return at;
- return acfsf_0mk2(acfsf_op at, numr simp cdr assoc(lhs,al))
- end;
- procedure acfsf_ifstructat(at,al);
- % Algebraically closed field irreducible factor structure of an
- % atomic formula. [at] is an atomic formula $R(t,0)$ where $t = c
- % ... s_j ...$ is a factorization of $t$ into irreducible factors;
- % [al] is an ALIST. Returns an atomic formula. [al] is of the form
- % $(..., (t_i . v_i), ...)$, where the $t_i$ are SF's and the $v_i$
- % are variables. Each factor $s_j$ of the left hand side $t$ of
- % [at] matches one of the $t_i$ in [al]. Returns the atomic formula
- % $R(c ... v_i ..., 0)$.
- begin scalar w,r;
- w := fctrf acfsf_arg2l at;
- r := car w;
- for each x in cdr w do
- r := multf(r,expf(numr simp cdr assoc(car x,al),cdr x));
- return acfsf_0mk2(acfsf_op at,r)
- end;
- procedure acfsf_termmlat(at);
- % Algebraically closed field term multiplicity list of atomic
- % formula. [at] is an atomic formula. Returns the multiplicity list
- % of all non-zero terms in [at].
- if acfsf_arg2l at then
- {(acfsf_arg2l at . 1)};
- procedure acfsf_decdeg(f);
- % Algebraically closed field decrease degrees. [f] is a formula.
- % Returns a formula equivalent to [f], hopefully decreasing the
- % degrees of the bound variables.
- acfsf_decdeg0 cl_rename!-vars f;
- procedure acfsf_decdeg0(f);
- begin scalar op,w,gamma,newmat;
- op := rl_op f;
- if rl_boolp op then
- return rl_mkn(op,for each subf in rl_argn f collect
- acfsf_decdeg0 subf);
- if rl_quap op then
- return rl_mkq(op,rl_var f,
- car acfsf_decdeg1(acfsf_decdeg0 rl_mat f,{rl_var f}));
- % [f] is not complex.
- return f
- end;
- procedure acfsf_decdeg1(f,vl);
- % Algebraically closed field decrease degrees. [f] is a formula;
- % [vl] is either a list of variables $v$ that do not occur boundly
- % in [f], or the identifier [fvarl]. Returns a pair $(\phi . l)$;
- % $l$ is a list of pairs $(..., (v_i . d_i), ...)$, with $v_i \in
- % [vl]$ and integer $d_i$; $\phi$ is obtained from [f] by replacing
- % powers $v_i^{d_i}$ by $v_i$. We have $\exists [vl] ([f])$
- % equivalent to $\exists [vl] (\phi)$. [fvarl] selects the list of
- % all free variables in [f] as [vl].
- begin scalar dvl; integer n;
- if vl eq 'fvarl then
- vl := cl_fvarl1 f;
- for each v in vl do <<
- n := acfsf_decdeg2(f,v);
- if n>1 then <<
- f := acfsf_decdeg3(f,v,n);
- dvl := (v . n) . dvl
- >>
- >>;
- return f . dvl
- end;
- procedure acfsf_decdeg2(f,v);
- % Algebraically closed field standard form decrement degree
- % subroutine. [f] is a formula; [v] is a variable. Returns an
- % INTEGER $n$. The degree of [v] in [f] can be decremented using
- % the substitution $[v]^n=v$.
- begin scalar a,w,atl,dgcd,!*gcd,oddp;
- !*gcd := T;
- atl := cl_atl1 f;
- dgcd := 0;
- while atl and dgcd neq 1 do <<
- a := car atl;
- atl := cdr atl;
- w := acfsf_ignshift(a,v);
- if null w then << % [w neq 'ignore]
- a := sfto_reorder(acfsf_arg2l a,v);
- while (not domainp a) and (mvar a eq v) and dgcd neq 1 do <<
- dgcd := gcdf(dgcd,ldeg a);
- a := red a
- >>
- >>
- >>;
- if dgcd = 0 then
- return 1;
- return dgcd
- end;
- procedure acfsf_ignshift(at,v);
- % Orderd field standard form ignore shift. [at] is an atomic
- % formula; [v] is a variable. Returns [nil] or ['ignore].
- begin scalar w;
- w := sfto_reorder(acfsf_arg2l at,v);
- if not domainp w and null red w and mvar w eq v then
- return 'ignore
- end;
- procedure acfsf_decdeg3(f,v,n);
- % Algebraically closed field standard form decrement degree. [f] is
- % a formula; [v] is a variable; [n] is an integer. Returns a
- % formula.
- cl_apply2ats1(f,'acfsf_decdegat,{v,n});
- procedure acfsf_decdegat(atf,v,n);
- % Algebraically closed field standard form decrement degree atomic
- % formula. [f] is an atomic formula; [v] is a variable; [n] is an
- % integer. Returns an atomic formula.
- if acfsf_ignshift(atf,v) then
- atf
- else
- acfsf_0mk2(acfsf_op atf,sfto_decdegf(acfsf_arg2l atf,v,n));
- procedure acfsf_multsurep(at,atl);
- % Algebraically closed field multplicative sure predicate. [at] is
- % an atomic formula; [atl] is a theory. Tries to prove [at] wrt.
- % [atl]. Returns non-[nil] in case of success.
- if acfsf_op at eq 'equal then
- acfsf_multsurep!-equal(at,atl)
- else
- acfsf_multsurep!-neq(at,atl);
- procedure acfsf_multsurep!-equal(at,atl);
- begin scalar c,a;
- c := acfsf_arg2l at;
- while atl do <<
- a := car atl;
- atl := cdr atl;
- if acfsf_op a eq 'equal and quotf(c,acfsf_arg2l a) then <<
- a := 'found;
- atl := nil
- >>
- >>;
- return a eq 'found
- end;
- procedure acfsf_multsurep!-neq(at,atl);
- begin scalar c,a;
- c := acfsf_arg2l at;
- while atl do <<
- a := car atl;
- atl := cdr atl;
- if acfsf_op a eq 'neq and quotf(acfsf_arg2l a,c) then <<
- a := 'found;
- atl := nil
- >>
- >>;
- return a eq 'found
- end;
- endmodule; % [acfsfmisc]
- end; % of file
|