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

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

 また経緯があり,ロジカルな処理は(あまり)行わず,有理式の(それなりに)正確な簡約のみを行うratsimpx2を書きました.

 論理結合子 %implies,%or,%and は既にあるものとして,%neg,%replies,%eq を新規に導入しますが,出力に現れるのは先の3つのみです.また,入力には true,false も使えます.

defrule(fto01,false,0=1);
defrule(tto00,true,0=0);

map(infix,["%replies","%eq"]);
matchdeclare([aa,bb,cc],true); 
"%neg"(aa):=(aa)%implies(0=1);
"%replies"(aa,bb):=(bb)%implies(aa);
"%eq"(aa,bb):=((aa)%implies(bb))%and((bb)%implies(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)));
defrule(cd1,rr=cc,(num(rr)=cc*denom(rr)) %and (denom(rr)#0));
defrule(cd2,cc=rr,(num(rr)=cc*denom(rr)) %and (denom(rr)#0));
defrule(cd3,cc<=rr, 
       ( (0<denom(rr)) %and (cc*denom(rr)<=num(rr)) ) %or
       ( (denom(rr)<0) %and (num(rr)<=cc*denom(rr)) ) );
defrule(cd4,cc<rr, 
       ( (0<denom(rr)) %and (cc*denom(rr)<num(rr)) ) %or
       ( (denom(rr)<0) %and (num(rr)<cc*denom(rr)) ) );
defrule(cd5,rr<=cc, 
       ( (denom(rr)<0) %and (cc*denom(rr)<=num(rr)) ) %or
       ( (0<denom(rr)) %and (num(rr)<=cc*denom(rr)) ) );
defrule(cd6,rr<cc, 
       ( (denom(rr)<0) %and (cc*denom(rr)<num(rr)) ) %or
       ( (0<denom(rr)) %and (num(rr)<cc*denom(rr)) ) );

ratsimpx1(x):=applyb1(x,fto01,tto00,sf1,sf2,fr1,fr2,fr3,cd1,cd2,cd3,cd4,cd5,cd6);
ratsimpx2(x):=ratsimpx1(ratsimpx1(x));