Nuprl Definition : add-polyn

add-polyn(n;p;q)
==r if (n =z 0)
    then p + q
    else if p = Ax then q
         otherwise if q = Ax then p otherwise eval rp = rev(p) in
                                              eval rq = rev(q) in
                                              eval cs = list_accum2(sofar,a,b.eval c = add-polyn(n - 1;a;b) in
                                                                              [c / sofar];sofar,a.[a / sofar];sofar,b.[b\000C / sofar];[];rp;rq) in
                                                rm-zeros(n - 1;cs)
    fi 
add-polyn(n;p;q) ==
  fix((λadd-polyn,n,p,q. if (n =z 0)
                        then p + q
                        else if p = Ax then q
                             otherwise if q = Ax then p
                                       otherwise eval rp = rev(p) in
                                                 eval rq = rev(q) in
                                                 eval cs = list_accum2(sofar,a,b.eval c = add-polyn (n - 1) a b in
                                                                                 [c / sofar];sofar,a.[a / sofar];sofar,b\000C.[b / 
                                                                                                    sofar];[];rp;rq) in
                                                   rm-zeros(n - 1;cs)
                        fi )) 
  n 
  p 
  q


Definitions occuring in Statement :  rm-zeros: rm-zeros(n;p),  list_accum2: list_accum2(x,a,b.f[x; a; b];x,a.g[x; a];x,b.h[x; b];y;as;bs),  reverse: rev(as),  cons: [a / b],  nil: [],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  isaxiom: if z = Ax then a otherwise b,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  add: n + m,  isaxiom: if z = Ax then a otherwise b,  reverse: rev(as),  list_accum2: list_accum2(x,a,b.f[x; a; b];x,a.g[x; a];x,b.h[x; b];y;as;bs),  callbyvalue: callbyvalue,  apply: f a,  cons: [a / b],  nil: [],  rm-zeros: rm-zeros(n;p),  subtract: n - m,  natural_number: $n
FDL editor aliases :  add-polyn
Latex:
add-polyn(n;p;q)
==r  if  (n  =\msubz{}  0)
        then  p  +  q
        else  if  p  =  Ax  then  q
                  otherwise  if  q  =  Ax  then  p
                                      otherwise  eval  rp  =  rev(p)  in
                                                          eval  rq  =  rev(q)  in
                                                          eval  cs  =  list\_accum2(sofar,a,b.eval  c  =  add-polyn(n  -  1;a;b)  in
                                                                                                                          [c  /  sofar];sofar,a.[a  /  sofar];sofar,b\000C.[b  / 
                                                                                                                                                                sofar];[];rp;rq)  in
                                                              rm-zeros(n  -  1;cs)
        fi 

Latex:
add-polyn(n;p;q)  ==
    fix((\mlambda{}add-polyn,n,p,q.  if  (n  =\msubz{}  0)
                                                then  p  +  q
                                                else  if  p  =  Ax  then  q
                                                          otherwise  if  q  =  Ax  then  p
                                                                              otherwise  eval  rp  =  rev(p)  in
                                                                                                  eval  rq  =  rev(q)  in
                                                                                                  ...
                                                fi  )) 
    n 
    p 
    q


Date html generated: 2017_09_29-PM-05_59_51
Last ObjectModification: 2017_04_27-PM-04_41_40

Theory : integer!polynomials


Home Index