Nuprl Definition : mult-polynom

mult-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
                   cbv_list_accum(z,a.eval zero' = polyconst(m;0) in
                                      eval z' = if null(z) then [] else eager-append(z;[zero']) fi  in
                                      eval aq = if poly-zero(m;a) then [] else map-rev(λx.mult-polynom(m;a;x);qq) fi  in
                                        add-polyn(n;z';aq);zero;pp)
      fi 
mult-polynom(n;p;q) ==
  fix((λmult-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
                                           cbv_list_accum(z,a.eval zero' = polyconst(m;0) in
                                                              eval z' = if null(z)
                                                                        then []
                                                                        else eager-append(z;[zero'])
                                                                        fi  in
                                                              eval aq = if poly-zero(m;a)
                                                                        then []
                                                                        else map-rev(λx.(mult-polynom m a x);qq)
                                                                        fi  in
                                                                add-polyn(n;z';aq);zero;pp)
                              fi )) 
  n 
  p 
  q


Definitions occuring in Statement :  polyconst: polyconst(n;k),  add-polyn: add-polyn(n;p;q),  poly-zero: poly-zero(n;p),  map-rev: map-rev(f;L),  cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),  null: null(as),  eager-append: eager-append(as;bs),  cons: [a / b],  nil: [],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  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,  subtract: n - m,  cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),  polyconst: polyconst(n;k),  natural_number: $n,  null: null(as),  eager-append: eager-append(as;bs),  cons: [a / b],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  poly-zero: poly-zero(n;p),  nil: [],  map-rev: map-rev(f;L),  lambda: λx.A[x],  apply: f a,  add-polyn: add-polyn(n;p;q)
FDL editor aliases :  mult-polynom
Latex:
mult-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
                                      cbv\_list\_accum(z,a.eval  zero'  =  polyconst(m;0)  in
                                                                            ...;zero;pp)
            fi 

Latex:
mult-polynom(n;p;q)  ==
    fix((\mlambda{}mult-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
                                                                                    cbv\_list\_accum(z,a.eval  zero'  =  polyconst(m;0)  in
                                                                                                                          eval  z'  =  if  null(z)
                                                                                                                                              then  []
                                                                                                                                              else  eager-append(z;[zero'])
                                                                                                                                              fi    in
                                                                                                                          eval  aq  =  if  poly-zero(m;a)
                                                                                                                                              then  []
                                                                                                                                              else  map-rev(\mlambda{}x.(... 
                                                                                                                                                                                m 
                                                                                                                                                                                a 
                                                                                                                                                                                x);qq)
                                                                                                                                              fi    in
                                                                                                                              add-polyn(n;z';aq);zero;pp)
                                                          fi  )) 
    n 
    p 
    q


Date html generated: 2017_09_29-PM-06_00_43
Last ObjectModification: 2017_04_27-PM-05_50_12

Theory : integer!polynomials


Home Index