Nuprl Definition : mul-polynom

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


Date html generated: 2017_04_20-AM-07_12_25
Last ObjectModification: 2017_04_17-PM-03_11_00

Theory : list_1


Home Index