Nuprl Definition : mul-polynom

mul-polynom(n;p;q)
==r eval pp = p in
    eval qq = q in
      if poly-zero(n;pp) then pp
      if poly-zero(n;qq) then qq
      else eval zero = polyconst(n;0) in
           if n=0
              then pp * qq
              else eval m = n - 1 in
                   eager-accum(z,a.add-polynom(n;tt;if null(z) then [] else z @ [polyconst(m;0)] fi ;if poly-zero(m;a)
                   then []
                   else map(λx.mul-polynom(m;a;x);qq)
                   fi );zero;pp)
      fi 
mul-polynom(n;p;q) ==
  fix((λmul-polynom,n,p,q. eval pp = p in
                           eval qq = q in
                             if poly-zero(n;pp) then pp
                             if poly-zero(n;qq) then qq
                             else eval zero = polyconst(n;0) in
                                  if n=0
                                     then pp * qq
                                     else eval m = n - 1 in
                                          eager-accum(z,a.add-polynom(n;tt;if null(z)
                                          then []
                                          else z @ [polyconst(m;0)]
                                          fi ;if poly-zero(m;a)
                                          then []
                                          else map(λx.(mul-polynom m a x);qq)
                                          fi );zero;pp)
                             fi )) 
  n 
  p 
  q


Definitions occuring in Statement :  polyconst: polyconst(n;k),  add-polynom: add-polynom(n;rmz;p;q),  poly-zero: poly-zero(n;p),  eager-accum: eager-accum(x,a.f[x; a];y;l),  null: null(as),  map: map(f;as),  append: as @ bs,  cons: [a / b],  nil: [],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  btrue: tt,  int_eq: if a=b  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  multiply: n * m,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  int_eq: if a=b  then c  else d,  multiply: n * m,  callbyvalue: callbyvalue,  subtract: n - m,  eager-accum: eager-accum(x,a.f[x; a];y;l),  add-polynom: add-polynom(n;rmz;p;q),  btrue: tt,  null: null(as),  append: as @ bs,  cons: [a / b],  polyconst: polyconst(n;k),  natural_number: $n,  ifthenelse: if b then t else f fi ,  poly-zero: poly-zero(n;p),  nil: [],  map: map(f;as),  lambda: λx.A[x],  apply: f a
FDL editor aliases :  mul-polynom
Latex:
mul-polynom(n;p;q)
==r  eval  pp  =  p  in
        eval  qq  =  q  in
            if  poly-zero(n;pp)  then  pp
            if  poly-zero(n;qq)  then  qq
            else  eval  zero  =  polyconst(n;0)  in
                      if  n=0
                            then  pp  *  qq
                            else  eval  m  =  n  -  1  in
                                      eager-accum(z,a.add-polynom(n;tt;if  null(z)
                                      then  []
                                      else  z  @  [polyconst(m;0)]
                                      fi  ;if  poly-zero(m;a)  then  []  else  map(\mlambda{}x.mul-polynom(m;a;x);qq)  fi  );zero;pp)
            fi 

Latex:
mul-polynom(n;p;q)  ==
    fix((\mlambda{}mul-polynom,n,p,q.  eval  pp  =  p  in
                                                      eval  qq  =  q  in
                                                          if  poly-zero(n;pp)  then  pp
                                                          if  poly-zero(n;qq)  then  qq
                                                          else  eval  zero  =  polyconst(n;0)  in
                                                                    if  n=0
                                                                          then  pp  *  qq
                                                                          else  eval  m  =  n  -  1  in
                                                                                    eager-accum(z,a.add-polynom(n;tt;if  null(z)
                                                                                    then  []
                                                                                    else  z  @  [polyconst(m;0)]
                                                                                    fi  ;if  poly-zero(m;a)
                                                                                    then  []
                                                                                    else  map(\mlambda{}x.(mul-polynom  m  a  x);qq)
                                                                                    fi  );zero;pp)
                                                          fi  )) 
    n 
    p 
    q


Date html generated: 2017_09_29-PM-06_00_46
Last ObjectModification: 2017_04_26-PM-02_05_04

Theory : integer!polynomials


Home Index