読者です 読者をやめる 読者になる 読者になる

maximaのロジックシステム(6)

 http://d.hatena.ne.jp/ehito/20140506/1399341060 で述べた「分母≠0の付帯」という慣習を実装したCASはあるのでしょうか? 例えば,Mathematica

In[1]:= Reduce[ForAll[{x, y, z}, y == z/x, Not[x == 0]], Reals]
Out[1]= True

In[2]:= Reduce[ForAll[{x, y}, y == x/x, Not[x == 0]], Reals]
Out[2]= False

In[3]:= Reduce[ForAll[{x, y}, y == 0/x, Not[x == 0]], Reals]
Out[3]= False

と返し,RedLog/REDUCE(on rlnzden,rladdcond),Mapleも同様です.原因はロジック以前に,x/x,0/xがそれぞれ1,0に,一般には(k*x)/xがkにsimplifyされるからであり,これを制止するには,Mathematicaの場合,Hold,Unevaluatedとの合成といった手があるわけですが,これでは約分以外の処理も進みません.

 ではどうするか...maxima上で実装してみました.

adddm(f):=block([dmX,dmY],
  if atom(f) then return(f),
  if is(op(f)="/") then 
    (part(f,1)+dmX^2-1+(1-dmX)*(1+dmX))
   /(part(f,2)+dmY+dmY/part(f,2)-dmY*(1+1/part(f,2))) else f)$
SF():=simp:false$
nzden(f):=block([g:scanmap(adddm,f,bottomup)],simp:true,qe([],g))$
nzdenqe(l,f):=block([g:scanmap(adddm,f,bottomup)],simp:true,qe(l,g))$

入力例.SF()$nzdenが関数名だと思って下さい.

SF()$nzden(y=x/x);
SF()$nzden(x=x^2/x);
SF()$nzden((1/a+1/b)*(a*b)/(a+b)=((1-x)*(1-x))/(1-x)+(1+x)/((1+x)*(1+x^2))+c);

SF()$nzden(f=1/(x/y));
SF()$nzden(f=1/(x/(y/z)));
SF()$nzden(f=1/(1+x/(y/z)));
SF()$nzden(f=1/(x/(y/(z/w))));
SF()$nzden(f=1/(1+x/(1+y/(1+z/w))));
SF()$nzden(f=(x/y)/(x/y));
SF()$nzden(f=(x/y)/(z/w));

SF()$nzden(y=0/x);
SF()$nzden((0<=x^4/x)%eq(0<x));
SF()$nzden(0/(1-x)<1/x);

qe([[A,x]],(a<=x^2/x) %eq (b<x));
SF()$nzdenqe([[A,x]],(a<=x^2/x) %eq (b<x));

SF()$f:nzden(a<=x^2/x)$
qe([[A,a],[A,b]], qe([[A,x]],(f) %eq (b<x)) %eq ((a=0) %and (b=0)));
kill(f)$