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

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

 ちょっとした経緯があり,maximaに,有理数体上の有理式を項とし,=,<,>,≦,≧を2項述語記号とする(量化記号のない)論理式を有理整数環上の多項式を項とする論理式に変換するコマンドtoimplxを実装してみました.

 論理記号は,否定negx,選言orx,連言andx,等価eqxの全てを含意implxに帰着させるスタイルです.

infix(implx);
infix(orx);
infix(andx);
infix(eqx);
matchdeclare(aa,true,bb,true); 
negx(aa):=(aa)implx(0=1);
aa orx bb:=(negx(aa))implx(bb);
aa andx bb:=negx((negx(aa))orx(negx(bb)));
aa eqx bb:=((aa)andx(bb))orx((negx(bb))andx(negx(aa)));

defrule(sf1,aa>=bb,bb<=aa);
defrule(sf2,aa>bb,bb<aa);
defrule(fr1,aa=bb,xthru(aa)=xthru(bb));
defrule(fr2,aa<bb,xthru(aa)<xthru(bb));
defrule(fr3,aa<=bb,xthru(aa)<=xthru(bb));

matchdeclare(rr,lambda([x],is(denom(x)#1)),cc,true);
defrule(cd1,rr=cc,(num(rr)=cc*denom(rr)) andx (negx(denom(rr)=0)));
defrule(cd2,cc=rr,(num(rr)=cc*denom(rr)) andx (negx(denom(rr)=0)));
defrule(cd3,cc<=rr, 
       ( (0<denom(rr)) andx (cc*denom(rr)<=num(rr)) ) orx
       ( (denom(rr)<0) andx (num(rr)<=cc*denom(rr)) ) );
defrule(cd4,cc<rr, 
       ( (0<denom(rr)) andx (cc*denom(rr)<num(rr)) ) orx
       ( (denom(rr)<0) andx (num(rr)<cc*denom(rr)) ) );
defrule(cd5,rr<=cc, 
       ( (denom(rr)<0) andx (cc*denom(rr)<=num(rr)) ) orx
       ( (0<denom(rr)) andx (num(rr)<=cc*denom(rr)) ) );
defrule(cd6,rr<cc, 
       ( (denom(rr)<0) andx (cc*denom(rr)<num(rr)) ) orx
       ( (0<denom(rr)) andx (num(rr)<cc*denom(rr)) ) );

toimplx1(x):=applyb1(x,sf1,sf2,fr1,fr2,fr3,cd1,cd2,cd3,cd4,cd5,cd6);
toimplx(x):=toimplx1(toimplx1(x));

 結合の強さはデフォルトのままなので,項は丸カッコで挟む必要があります.また,非等号#は用いず,negxで等式を否定して下さい.

 入出力例

toimplx(y=1/x);
(%o51) (1=x*y) implx (0=1) implx (0=1) implx ((x=0) implx (0=1) implx (0=1)) implx (0=1)

toimplx(negx(y=1/x));
(%o52) (1=x*y) implx (0=1) implx (0=1) implx ((x=0) implx (0=1) implx (0=1)) implx (0=1)
 implx (0=1)

toimplx((0<=1/x)eqx(a<x));
(%o53) (0<x) implx (0=1) implx (0=1) implx ((0<=1) implx (0=1)) implx (0=1) implx (0=1) implx 
((x<0) implx (0=1) implx (0=1) implx ((1<=0) implx (0=1)) implx (0=1)) implx (0=1) implx (0=1)
 implx ((a<x) implx (0=1)) implx (0=1) implx (0=1) implx ((a<x) implx (0=1) implx (0=1) implx 
(0=1) implx ((0<x) implx (0=1) implx (0=1) implx ((0<=1) implx (0=1)) implx (0=1) implx (0=1)
 implx ((x<0) implx (0=1) implx (0=1) implx ((1<=0) implx (0=1)) implx (0=1)) implx (0=1)
 implx (0=1)) implx (0=1))

toimplx(((0<x) andx (0<y)) implx (x/y+y/x>=c));
(%o54) (0<x) implx (0=1) implx (0=1) implx ((0<y) implx (0=1)) implx (0=1) implx ((0<x*y)
 implx (0=1) implx (0=1) implx ((c*x*y<=y^2+x^2) implx (0=1)) implx (0=1) implx (0=1) implx 
((x*y<0) implx (0=1) implx (0=1) implx ((y^2+x^2<=c*x*y) implx (0=1)) implx (0=1)))