Nuprl Definition : mul-polynom
mul-polynom(p;q)
==r if tree_leaf?(p)
then if tree_leaf-value(p)=0
then polyconst(0)
else if tree_leaf-value(p)=1
then q
else if tree_leaf?(q)
then eval a = tree_leaf-value(p) * tree_leaf-value(q) in
tree_leaf(a)
else eval a = mul-polynom(p;tree_node-left(q)) in
eval b = mul-polynom(p;tree_node-right(q)) in
tree_node(a;b)
fi
if tree_leaf?(q)
then if tree_leaf-value(q)=0
then polyconst(0)
else if tree_leaf-value(q)=1
then p
else eval a = mul-polynom(tree_node-left(p);q) in
eval b = mul-polynom(tree_node-right(p);q) in
tree_node(a;b)
else eval aa = mul-polynom(tree_node-left(p);tree_node-left(q)) in
eval ab = mul-polynom(tree_node(tree_node-left(p);polyconst(0));tree_node-right(q)) in
eval ba = mul-polynom(tree_node-right(p);tree_node(tree_node-left(q);polyconst(0))) in
eval bb = mul-polynom(tree_node-right(p);tree_node-right(q)) in
eval mid = add-polynom(ab;ba) in
eval bb' = add-polynom(mid;tree_node(polyconst(0);bb)) in
tree_node(aa;bb')
fi
mul-polynom(p;q) ==
fix((λmul-polynom,p,q. if tree_leaf?(p)
then if tree_leaf-value(p)=0
then polyconst(0)
else if tree_leaf-value(p)=1
then q
else if tree_leaf?(q)
then eval a = tree_leaf-value(p) * tree_leaf-value(q) in
tree_leaf(a)
else eval a = mul-polynom p tree_node-left(q) in
eval b = mul-polynom p tree_node-right(q) in
tree_node(a;b)
fi
if tree_leaf?(q)
then if tree_leaf-value(q)=0
then polyconst(0)
else if tree_leaf-value(q)=1
then p
else eval a = mul-polynom tree_node-left(p) q in
eval b = mul-polynom tree_node-right(p) q in
tree_node(a;b)
else eval aa = mul-polynom tree_node-left(p) tree_node-left(q) in
eval ab = mul-polynom tree_node(tree_node-left(p);polyconst(0)) tree_node-right(q) in
eval ba = mul-polynom tree_node-right(p) tree_node(tree_node-left(q);polyconst(0)) in
eval bb = mul-polynom tree_node-right(p) tree_node-right(q) in
eval mid = add-polynom(ab;ba) in
eval bb' = add-polynom(mid;tree_node(polyconst(0);bb)) in
tree_node(aa;bb')
fi ))
p
q
Wellformedness Lemmas :
mul-polynom_wf2,
mul-polynom_wf
Definitions occuring in Statement :
add-polynom: add-polynom(p;q),
polyconst: polyconst(k),
tree_node-right: tree_node-right(v),
tree_node-left: tree_node-left(v),
tree_leaf-value: tree_leaf-value(v),
tree_leaf?: tree_leaf?(v),
tree_node: tree_node(left;right),
tree_leaf: tree_leaf(value),
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,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
multiply: n * m,
tree_leaf: tree_leaf(value),
ifthenelse: if b then t else f fi ,
tree_leaf?: tree_leaf?(v),
int_eq: if a=b then c else d,
tree_leaf-value: tree_leaf-value(v),
tree_node-left: tree_node-left(v),
apply: f a,
tree_node-right: tree_node-right(v),
callbyvalue: callbyvalue,
add-polynom: add-polynom(p;q),
polyconst: polyconst(k),
natural_number: $n,
tree_node: tree_node(left;right)
FDL editor aliases :
mul-polynom
Latex:
mul-polynom(p;q)
==r if tree\_leaf?(p)
then if tree\_leaf-value(p)=0
then polyconst(0)
else if tree\_leaf-value(p)=1
then q
else if tree\_leaf?(q)
then eval a = tree\_leaf-value(p) * tree\_leaf-value(q) in
tree\_leaf(a)
else eval a = mul-polynom(p;tree\_node-left(q)) in
eval b = mul-polynom(p;tree\_node-right(q)) in
tree\_node(a;b)
fi
if tree\_leaf?(q)
then if tree\_leaf-value(q)=0
then polyconst(0)
else if tree\_leaf-value(q)=1
then p
else eval a = mul-polynom(tree\_node-left(p);q) in
eval b = mul-polynom(tree\_node-right(p);q) in
tree\_node(a;b)
else eval aa = mul-polynom(tree\_node-left(p);tree\_node-left(q)) in
eval ab = mul-polynom(tree\_node(tree\_node-left(p);polyconst(0));tree\_node-right(q)) in
eval ba = mul-polynom(tree\_node-right(p);tree\_node(tree\_node-left(q);polyconst(0))) in
eval bb = mul-polynom(tree\_node-right(p);tree\_node-right(q)) in
eval mid = add-polynom(ab;ba) in
eval bb' = add-polynom(mid;tree\_node(polyconst(0);bb)) in
tree\_node(aa;bb')
fi
Latex:
mul-polynom(p;q) ==
fix((\mlambda{}mul-polynom,p,q. if tree\_leaf?(p)
then if tree\_leaf-value(p)=0
then polyconst(0)
else if tree\_leaf-value(p)=1
then q
else if tree\_leaf?(q)
then eval a = tree\_leaf-value(p)
* tree\_leaf-value(q) in
tree\_leaf(a)
else eval a = mul-polynom p tree\_node-left(q) in
eval b = mul-polynom p tree\_node-right(q) in
tree\_node(a;b)
fi
if tree\_leaf?(q)
then if tree\_leaf-value(q)=0
then polyconst(0)
else if tree\_leaf-value(q)=1
then p
else eval a = mul-polynom tree\_node-left(p) q in
eval b = mul-polynom tree\_node-right(p) q in
tree\_node(a;b)
else eval aa = mul-polynom tree\_node-left(p) tree\_node-left(q) in
eval ab = mul-polynom tree\_node(tree\_node-left(p);polyconst(0))
tree\_node-right(q) in
eval ba = mul-polynom tree\_node-right(p)
tree\_node(tree\_node-left(q);polyconst(0)) in
eval bb = mul-polynom tree\_node-right(p) tree\_node-right(q) in
eval mid = add-polynom(ab;ba) in
eval bb' = add-polynom(mid;tree\_node(polyconst(0);bb)) in
tree\_node(aa;bb')
fi ))
p
q
Date html generated:
2017_10_01-AM-08_33_02
Last ObjectModification:
2017_05_03-AM-11_09_46
Theory : integer!polynomial!trees
Home
Index