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)$