% ----------------------------------------------------------------------
% $Id: dvfsfmisc.red,v 1.14 1999/04/05 11:23:43 dolzmann Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: dvfsfmisc.red,v $
% Revision 1.14 1999/04/05 11:23:43 dolzmann
% Fixed a bug in dvfsf_mkcanonic.
%
% Revision 1.13 1999/04/01 11:24:59 dolzmann
% Changed comments.
% Fixed a bug in dvfsf_varsubstat.
%
% Revision 1.12 1999/03/24 12:41:51 dolzmann
% Added and reformatted comments.
% Fixed a bug in dvfsf_fctrat: The alist of the left and right hand sides
% are merged instead of concatenated.
%
% Revision 1.11 1999/03/23 08:52:17 dolzmann
% Changed copyright information.
%
% Revision 1.10 1999/03/21 13:35:23 dolzmann
% Added black box implementation dvfsf_subsumption.
%
% Revision 1.9 1999/03/19 18:35:32 dolzmann
% Changed procedure dvfsf_varlat: p is not longer treated as a variable.
%
% Revision 1.8 1999/03/19 15:20:37 dolzmann
% Added procedures dvfsf_subat, dvfsf_subalchk, and dvfsf_eqnrhskernels
% for the CL implementation of the service rl_subfof.
%
% Revision 1.7 1999/03/19 12:17:47 dolzmann
% Added service rlmkcanonic.
%
% Revision 1.6 1999/01/17 16:24:01 dolzmann
% Changed copyright notice.
% Changed semantics of dvfsf_fctrat: Polynomials in p does not belong to
% the content.
% Added black boxes rl_termmlat, rl_structat, and rl_ifstructat.
% Added services rl_explats.
%
% Revision 1.5 1997/11/03 15:11:51 sturm
% Added BB implementation dvfsf_a2cdl.
%
% Revision 1.4 1996/10/07 11:32:06 sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.3 1996/07/15 14:08:09 sturm
% Fixed a bug in dvfsf_negateat.
%
% Revision 1.2 1996/07/13 11:40:36 dolzmann
% Added procedures dvfsf_dnf and dvfsf_cnf for Boolean normal form
% computation with subsumption.
% Removed procedure dvfsf_bnfsimpl.
%
% Revision 1.1 1996/07/08 12:15:22 sturm
% Initial check-in.
%
% ----------------------------------------------------------------------
lisp <<
fluid '(dvfsf_misc_rcsid!* dvfsf_misc_copyright!*);
dvfsf_misc_rcsid!* :=
"$Id: dvfsfmisc.red,v 1.14 1999/04/05 11:23:43 dolzmann Exp $";
dvfsf_misc_copyright!* :=
"Copyright (c) 1995-1999 by A. Dolzmann and T. Sturm"
>>;
module dvfsfmisc;
% Discretely valued field standard form miscellaneous. Submodule of [dvfsf].
procedure dvfsf_ordatp(a1,a2);
% Discretely valued field standard form ordering of atomic formulas
% predicate. [a1] and [a2] are atomic formulas. Returns [T] iff
% [a1] is less than or equal to [a2].
begin scalar w1,w2;
w1 := dvfsf_arg2l a1;
w2 := dvfsf_arg2l a2;
if w1 neq w2 then return ordp(w1,w2);
w1 := dvfsf_arg2r a1;
w2 := dvfsf_arg2r a2;
if w1 neq w2 then return ordp(w1,w2);
return dvfsf_ordrelp(dvfsf_op a1,dvfsf_op a2)
end;
procedure dvfsf_ordrelp(r1,r2);
% Discretely valued field standard form ordering of atomic formulas
% predicate. [a1] and [a2] are relations. Returns [T] iff [r1] is
% less than or equal to [r2].
not not (r2 memq (r1 memq '(equal neq div sdiv assoc)));
procedure dvfsf_varlat(atf);
% Discretely valued field standard form atomic formula list of
% variables. [atf] is an atomic formula. Returns the variables
% contained in [atf] as a list. The constant ['p] of our language
% is not considered as an variable.
delqip('p,union(kernels dvfsf_arg2l atf,kernels dvfsf_arg2r atf));
procedure dvfsf_varsubstat(atf,new,old);
% Discretely valued field standard form substitute variable for
% variable in atomic formula. [atf] is an atomic formula; [new] and
% [old] are variables. Returns an atomic formula equivalent to
% [atf] where [old] is substituted with [new].
dvfsf_mk2(dvfsf_op atf,numr subf(dvfsf_arg2l atf,{old . new}),
numr subf(dvfsf_arg2r atf,{old . new}));
procedure dvfsf_negateat(atf);
% Discretely valued field standard form negate atomic formula.
% [atf] is an atomic formula. Returns a quantifier-free positive
% formula that is equivalent to $\lnot [atf]$.
begin scalar op;
op := dvfsf_op atf;
if op eq 'equal then
return dvfsf_mkn('neq,dvfsf_argn atf);
if op eq 'neq then
return dvfsf_mkn('equal,dvfsf_argn atf);
if op eq 'div then
return dvfsf_mk2('sdiv,dvfsf_arg2r atf,dvfsf_arg2l atf);
if op eq 'sdiv then
return dvfsf_mk2('div,dvfsf_arg2r atf,dvfsf_arg2l atf);
if op eq 'assoc then
return dvfsf_mk2('nassoc,dvfsf_arg2l atf,dvfsf_arg2r atf);
if op eq 'nassoc then
return dvfsf_mk2('assoc,dvfsf_arg2l atf,dvfsf_arg2r atf);
end;
procedure dvfsf_fctrat(at);
% Discretely valued field standard form factorize atomic formula.
% [at] is an atomic formula $l \mathrel{\varrho} r$. Returns a list
% $(...,(f_i . d_i),...)$, where $f$ is an irreducible SF and $d$
% is a positive integer. We have $l r=c \prod_i g_i^{d_i}$ for an
% integer $c$.
begin scalar w1,w2;
w1 := cdr fctrf dvfsf_arg2l at;
w2 := cdr fctrf dvfsf_arg2r at;
return lto_almerge({w1,w2},'plus2)
end;
procedure dvfsf_v(z);
% Discretely valued field standard form valuation function. [z] is
% a non-zero integer. The fluid [dvfsf_p!*] must be fixed to a
% positive prime integer $p$. Returns the $p$-adic value of [z].
(if null cdr qrm then 1 + dvfsf_v car qrm else 0)
where qrm=qremf(z,dvfsf_p!*);
procedure dvfsf_dnf(f);
% Discretely valued field standard form conjunctive normal form.
% [f] is a formula. Returns a DNF of [f].
if !*rlbnfsac then
(cl_dnf f) where !*rlsiso=T
else
cl_dnf f;
procedure dvfsf_cnf(f);
% Discretely valued field standard form conjunctive normal form.
% [f] is a formula. Returns a CNF of [f].
if !*rlbnfsac then
(cl_cnf f) where !*rlsiso=T
else
cl_cnf f;
procedure dvfsf_subsumption(l1,l2,gor);
% Discretely valued field standard form subsume. [l1] and [l2] are
% lists of atomic formulas. Returns one of [keep1], [keep2], [nil].
if gor eq 'or then (
if dvfsf_subsumep!-and(l1,l2) then
'keep2
else if dvfsf_subsumep!-and(l2,l1) then
'keep1
) else % [gor eq 'and]
if dvfsf_subsumep!-or(l1,l2) then
'keep1
else if dvfsf_subsumep!-or(l2,l1) then
'keep2
else
nil;
procedure dvfsf_subsumep!-and(l1,l2);
% Discretely valued field standard form subsume [and] case. [l1]
% and [l2] are lists of atomic formulas.
begin scalar a;
while l2 do <<
a := car l2;
l2 := cdr l2;
if cl_simpl(a,l1,-1) neq 'true then a := l2 := nil
>>;
return a
end;
procedure dvfsf_subsumep!-or(l1,l2);
% Discretely valued field standard form subsume [or] case. [l1] and
% [l2] are lists of atomic formulas.
begin scalar a;
while l1 do <<
a := car l1;
l1 := cdr l1;
if cl_simpl(rl_smkn('or,l2),{a},-1) neq 'true then a := l1 := nil
>>;
return a
end;
procedure dvfsf_a2cdl(atml);
% Discretely valued field standard form atomic formula multiplicity
% list to case distinction list. [atml] is a list of atomic
% formulas with multiplicity. Returns a list, each containing a
% list of complete case distinctions.
begin scalar atf,termll,flag;
while atml do <<
atf := caar atml;
atml := cdr atml;
termll := dvfsf_argn atf . termll;
if not(dvfsf_op atf memq '(equal neq)) then flag := T
>>;
return if flag then
for each x in termll collect
{dvfsf_mk2('sdiv,car x,cadr x),
dvfsf_mk2('assoc,car x,cadr x),
dvfsf_mk2('sdiv,cadr x,car x)}
else
for each x in termll collect
{dvfsf_0mk2('equal,x),dvfsf_0mk2('neq,x)}
end;
procedure dvfsf_subat(al,f);
% Discretely valued field standard form substitute in atomic
% formula. [al] is ALIST for [subf()]; [f] is an atomic formula.
% Returns an atomic formula.
begin scalar nlhs,nrhs,w;
nlhs := subf(dvfsf_arg2l f,al);
nrhs := subf(dvfsf_arg2r f,al);
if (not domainp denr nlhs) or (not domainp denr nrhs) then
rederr "parametric denominator after substitution";
w := lcm(denr nlhs,denr nrhs);
return dvfsf_mk2(dvfsf_op f,
numr multsq(nlhs,!*f2q w),numr multsq(nrhs,!*f2q w))
end;
procedure dvfsf_subalchk(al);
% Discretely valued field standard form substitution alist check.
% [al] is an ALIST for [subf()]. Return value undefined. Raises an
% error if an illegal substituion is contained in [al].
for each x in al do
if not domainp denr simp cdr x then
rederr "parametric denominator in substituted term";
procedure dvfsf_eqnrhskernels(x);
% Discretely valued field standard form equation right hand side
% kernels. [x] is an equation. Returns a list of all kernels
% contained in the right hand side of [x].
nconc(kernels numr w,kernels denr w) where w=simp cdr x;
procedure dvfsf_structat(at,al);
% Discretely valued field standard form structure of an atomic
% formula. [at] is an atomic formula $([op],l,r)$; [al] is an
% ALIST. Returns an atomic formula. [al] is of the form $(...,(f_i
% . v_i),...)$ where $f_i$ is an SF and $v_i$ is a variable. Both
% the left hand side of [at] and the right hand side of [at] occurs
% as keys in [al]. Returns the atomic formula $[op](v_i,v_j)$,
% provided $l=f_i$ and $r=f_j$.
begin scalar lhs,rhs;
lhs := dvfsf_arg2l at;
rhs := dvfsf_arg2r at;
if not(domainp lhs) then
lhs := numr simp cdr assoc(lhs,al);
if not(domainp rhs) then
rhs := numr simp cdr assoc(rhs,al);
return dvfsf_mk2(dvfsf_op at,lhs,rhs)
end;
procedure dvfsf_ifstructat(at,al);
% Discretely valued field standard form irreducible factor
% structure of atomic formula. [at] is an atomic formula $(f\rho
% g)$, [al] is an A-LIST of the form $(...,( f_i . v_i ),...)$.
% Returns an atomic formula of the form $(z u_1 \cdots u_m \rho z'
% w_1 \cdots w_m)$. Each $u_i$ and each $w_i$ occur as a value in
% [al] with the keys $f'_i$ and $g'_i$, respectively, and we have
% $f=z f'_1 \cdots f'_m$ and $g'=z' w_1 \cdots w_m$ for integers
% $z$ and $z'$.
begin scalar lhs,rhs,rl,rr;
lhs := fctrf dvfsf_arg2l at;
rhs := fctrf dvfsf_arg2r at;
rl := car lhs;
for each x in cdr lhs do
rl := multf(rl,expf(numr simp cdr assoc(car x,al),cdr x));
rr := car rhs;
for each x in cdr rhs do
rr := multf(rr,expf(numr simp cdr assoc(car x,al),cdr x));
return dvfsf_mk2(dvfsf_op at,rl,rr)
end;
procedure dvfsf_termmlat(at);
% Discretely valued field standard form term multiplicity list of
% atomic formula. [at] is an atomic formula. Returns the
% multiplicity list off all non-zero terms in [at].
begin scalar r,w;
w := dvfsf_arg2l at;
if w then
r := (w . 1) . r;
w := dvfsf_arg2r at;
if w then
r := (w . 1) . r;
return r
end;
procedure dvfsf_explats(f);
% Discretely valued fields standard form explode z atomic formulas.
% [f] is a formula. Returns a formula equivalent to [at]. Explodes
% atomic formula contained in [f] in dependency of [!*rlsiexpl],
% [!*rlsiexpla] and the operator of the respective boolean level.
% Only atomic formulas of the form $z \mathrel{\varrho} 1$, where
% $z$ is an integer and $\varrho$ is one of ['assoc], ['nassoc]
% will be exploded.
cl_simpl(cl_apply2ats2(f,'dvfsf_explodezat,nil,nil),nil,-1);
procedure dvfsf_explodezat(at,sop);
% Discretely valued fields standard form explode z atomic formulas
% for atomic formulas. [at] is an atomic formula; [sop] is a
% boolean operator. Returns a formula equivalent to [at]. Explodes
% [at] in dependency of [!*rlsiexpl], [!*rlsiexpla], and [sop].
% Only atomic formulas of the form $z \mathrel{\varrho} 1$, where
% $z$ is an integer and $\varrho$ is one of ['assoc], ['nassoc]
% will be exploded.
begin scalar op,lhs,rhs;
lhs := dvfsf_arg2l at;
rhs := dvfsf_arg2r at;
if not(domainp lhs and rhs = 1) then
return at;
op := dvfsf_op at;
if not (op eq 'assoc or op eq 'nassoc) then
return at;
if !*rlsiexpla then
return dvfsf_explodezat1(op,lhs);
if !*rlsiexpl then <<
if op eq 'assoc and (sop eq 'and or null sop) then
return dvfsf_explodezat1(op,lhs);
if op eq 'nassoc and (sop eq 'or or null sop) then
return dvfsf_explodezat1(op,lhs);
>>;
return at
end;
procedure dvfsf_explodezat1(op,lhs);
% Discretely valued fields standard form explode z atomic formulas
% subroutine. [op] id one of ['assoc], ['nassoc]; [lhs] is an
% integer.
rl_smkn(if op eq 'assoc then 'and else 'or,
for each x in zfactor lhs collect dvfsf_mk2(op,car x,numr simp 1));
procedure dvfsf_mkcanonic(f);
% Discretely valued fields standard form make canonic. [f] is an
% variable free and quantifier free formula. Returns the unique and
% canonic representation of [f].
begin scalar facl,u,fu,xl,op,pr;
if rl_tvalp f then
return f;
facl := dvfsf_coeffacl(f);
if null facl then
return cl_simpl(f,nil,-1);
pr := nextprime lto_max facl;
u := cl_simpl(dvfsf_subp(f,pr),nil,-1)
where dvfsf_p!*=pr;
fu := cl_flip u;
xl := for each fac in facl join
if ((cl_simpl(dvfsf_subp(f,fac),nil,-1))
where dvfsf_p!*=fac) eq fu
then
{fac};
op := if u eq 'false then 'nassoc else 'assoc;
xl := sort(xl,'lessp);
return rl_smkn(if u eq 'false then 'or else 'and,
for each x in xl collect dvfsf_mk2(op,x,numr simp 1))
end;
procedure dvfsf_coeffacl(f);
% Discretely valued fields standard form coefficients factor list.
% [f] is a formula. Returns the list of all ireducicble factors of
% all integer coefficients.
begin scalar cfml;
cfml := cl_f2ml(f,'dvfsf_coeffaclat);
return for each x in cfml collect car x
end;
procedure dvfsf_coeffaclat(at);
% Discretely valued fields standard form coefficients factor list
% for atomic formulas. [f] is an atomic formula. Returns the list
% of all ireducicble factors of all integer coefficients.
lto_almerge({dvfsf_coeffaclf dvfsf_arg2l at,dvfsf_coeffaclf dvfsf_arg2r at},
'plus2);
procedure dvfsf_coeffaclf(f);
% Discretely valued fields standard form coefficients factor list
% for standard forms. [f] is an SF. Returns the list of all
% ireducicble factors of all integer coefficients.
if null f then
{}
else if domainp f then
dvfsf_coeffaclz f
else if mvar f eq ' p then
lto_almerge({dvfsf_coeffaclz lc f,dvfsf_coeffaclf red f},'plus2)
else
rederr "dvfsf_coeffaclf: unknown mvar";
procedure dvfsf_coeffaclz(z);
% Discretely valued fields standard form coefficients factor list
% for integers. [f] is an integer. Returns the list of all
% positive ireducicble factors upto 1 and -1.
if z=1 or z=-1 or z=0 then
{}
else if z < 0 then
zfactor (-z)
else
zfactor z;
procedure dvfsf_subp(f,p);
% Discretely valued fields standard form substitute for p. [f] is a
% formula, [p] is a prime integer. Returns a formula in which all
% occurences of ['p] are replaced by [p].
cl_apply2ats1(f,'cl_subpat,{{'p . p}});
procedure cl_subpat(at,al);
% Discretely valued fields standard form substitute for p for
% atomic formulas. [at] is an atomic formula, al is an ALIST
% describing the substitution of ['p] with an prime integer $p$.
% Returns a formula in which all occurences of ['p] are replaced by
% $p$.
dvfsf_mk2(dvfsf_op at,
numr subf(dvfsf_arg2l at,al),numr subf(dvfsf_arg2r at,al));
endmodule; % [dvfsfmisc]
end; % of file