Nuprl Definition : ml-term-to-poly
ml-term-to-poly(t) ==
let ml_add_poly = λp,q.
let length = fix((λlength,l. if null(l) then 0 else let a.as = l in 1 + length(as) fi )) in
let lexaux = fix((λlexaux,n,l1,l2. ((n =z 0)
∨blet a.as = l1
in let b.bs = l2
in a <z b ∨b((a =z b) ∧b lexaux(n - 1)(as)(bs))))) in
let ml_lex = λl1,l2. let n1 = length(l1) in
let n2 = length(l2) in
n1 <z n2 ∨b((n1 =z n2) ∧b lexaux(n1)(l1)(l2)) in
let ml_monomial_le = λm1,m2. ml_lex(snd(m1))(snd(m2)) in
let revappend = fix((λrevappend,l,x. if null(l)
then x
else let a.b = l
in revappend(b)([a / x])
fi )) in
let ml_add_poly_prepend = fix((λml_add_poly_prepend,l,p,q.
if null(p)
then revappend(l)(q)
if null(q)
then revappend(l)(p)
else let p1.ps = p
in let q1.qs = q
in if ml_monomial_le(p1)(q1)
then if ...(q1)(p1)
then let cp,vs = p1
in ...
else ...(ps)([q1 /
qs])
fi
else ...([q1 /
l])([p1 /
ps])(qs)
fi
fi )) in
ml_add_poly_prepend([])(p)(q) in
let ml_minus_poly = λp.let map = fix((λmap,f,l. if null(l) then [] else let a.as = l in [f(a) / map(f)(as)] fi )) in
let ml_minus_monomial = λx.let c,vs = x
in <-c, vs> in
map(ml_minus_monomial)(p) in
let ml_mul_poly = λp,q.
let accumulate = fix((λaccumulate,f,b,l. if null(l)
then b
else let a.as = l
in accumulate(f)(f(b)(a))(as)
fi )) in
let insert_int = fix((λinsert_int,x,l. if null(l)
then [x]
else let a.as = l
in if x <z a + 1
then [x / l]
else let y = insert_int(x)(as) in
[a / y]
fi
fi )) in
let reduce = fix((λreduce,f,b,l. if null(l)
then b
else let a.as = l
in f(a)(reduce(f)(b)(as))
fi )) in
let merge_int = λas,bs. reduce(insert_int)(as)(bs) in
let ml_mul_monomials = λx.let a,vs = x
in λx1.let b,ws = x1
in <a * b, merge_int(vs)(ws)> in
let ml_mul_mono_poly = fix((λml_mul_mono_poly,m,p. if null(p)
then []
else let h.t = p
in let r = ml_mul_mono_poly(m)(t) in
let m' = ml_mul_monomials(m)(h) in
[m' / r]
fi )) in
if null(p) then []
if null(q) then []
else let p1.ps = p
in accumulate(λs,m. ml_add_poly(s)(ml_mul_mono_poly(m)(q)))(ml_mul_mono_poly(p1)(q))(ps)
fi in
let ml_rP_to_poly = fix((λml_rP_to_poly,stack,L. if null(L)
then stack
else let op.more = L
in if (op =z 1)
then let c.evenmore = more
in let x = if (c =z 0) then [] else [<c, []>] fi in
ml_rP_to_poly([x / stack])(evenmore)
if (op =z 2)
then let v.evenmore = more
in ml_rP_to_poly([[<1, [v]>] / stack])(evenmore)
if (op =z 3)
then let q.qq = stack
in let p.s = qq
in ml_rP_to_poly([ml_add_poly(p)(q) / s])(more)
if (op =z 4)
then let q.qq = stack
in let p.s = qq
in ml_rP_to_poly([ml_add_poly(p)(...(q)) /
s])(more)
if (op =z 5)
then let q.qq = stack
in let p.s = qq
in ml_rP_to_poly([ml_mul_poly(p)(q) / s])(more)
else let p.s = stack
in ml_rP_to_poly([ml_minus_poly(p) / s])(more)
fi
fi )) in
hd(ml_rP_to_poly([])(int_term_to_rP(t)))
Definitions occuring in Statement :
int_term_to_rP: int_term_to_rP(t),
spreadcons: spreadcons,
ml_apply: f(x),
hd: hd(l),
null: null(as),
cons: [a / b],
nil: [],
bor: p ∨bq,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
eq_int: (i =z j),
let: let,
pi1: fst(t),
pi2: snd(t),
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
multiply: n * m,
subtract: n - m,
add: n + m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
ml_apply: f(x),
pair: <a, b>,
cons: [a / b],
natural_number: $n,
eq_int: (i =z j),
ifthenelse: if b then t else f fi ,
let: let,
pi1: fst(t),
add: n + m,
spread: spread def,
spreadcons: spreadcons,
null: null(as),
lambda: λx.A[x],
fix: fix(F),
pi2: snd(t),
band: p ∧b q,
lt_int: i <z j,
bor: p ∨bq,
subtract: n - m,
nil: [],
minus: -n,
multiply: n * m,
hd: hd(l),
int_term_to_rP: int_term_to_rP(t)
FDL editor aliases :
ml-term-to-poly
Latex:
ml-term-to-poly(t) ==
let ml\_add$_{poly}$ = \mlambda{}p,q.
let length = fix((\mlambda{}length,l. if null(l)
then 0
else let a.as = l
in 1 + length(as)
fi )) in
let lexaux = fix((\mlambda{}lexaux,n,l1,l2. ((n =\msubz{} 0)
\mvee{}\msubb{}let a.as = l1
in let b.bs = l2
in a <z b
\mvee{}\msubb{}((a =\msubz{} b)
\mwedge{}\msubb{} lexaux(n - 1)(as)(bs))))) in
let ml$_{lex}$ = \mlambda{}l1,l2. let n1 = length(l1) in
let n2 = length(l2) in
n1 <z n2 \mvee{}\msubb{}((n1 =\msubz{} n2) \mwedge{}\msubb{} lexaux(n1)(l1)(l2)) in
let ml\_monomial$_{le}$ = \mlambda{}m1,m2. ml$_{lex\mbackslash{}f\000Cf7d$(snd(m1))(snd(m2)) in
let revappend = fix((\mlambda{}revappend,l,x. if null(l)
then x
else let a.b = l
in revappend(b)([a / x])
fi )) in
let ml\_add\_poly$_{prepend}$ = fix((\mlambda{}ml\_add\_poly$\mbackslash{}ff\000C5f{prepend}$,l,p,q.
if null(p)
then ...(l)(q)
if null(q)
then ...(l)(p)
else let p1.ps = p
in let q1.qs =
q
in if ...
then ...
else ...
fi
fi )) in
ml\_add\_poly$_{prepend}$([])(p)(q) in
let ml\_minus$_{poly}$ = \mlambda{}p.let map = fix((\mlambda{}map,f,l. if null(l)
then []
else let a.as = l
in [f(a) / map(f)(as)]
fi )) in
let ml\_minus$_{monomial}$ = \mlambda{}x.let c,vs = x
in <-c, vs> in
map(ml\_minus$_{monomial}$)(p) in
let ml\_mul$_{poly}$ = \mlambda{}p,q.
let accumulate = fix((\mlambda{}accumulate,f,b,l. if null(l)
then b
else let a.as = l
in accumulate(f)(f(b)(a))(as)
fi )) in
let insert$_{int}$ = fix((\mlambda{}insert$_{int\mbackslash{}ff\000C7d$,x,l. if null(l)
then [x]
else let a.as = l
in if x <z a + 1
then [x / l]
else ...
fi
fi )) in
let reduce = fix((\mlambda{}reduce,f,b,l. if null(l)
then b
else let a.as = l
in f(a)(reduce(f)(b)(as))
fi )) in
let merge$_{int}$ = \mlambda{}as,bs. reduce(insert$_\mbackslash{}ff\000C7bint}$)(as)(bs) in
let ml\_mul$_{monomials}$ = \mlambda{}x.let a,vs = x
in \mlambda{}x1.let b,ws = x1
in <a * b, merge$_{int}\mbackslash{}ff\000C24(vs)(ws)> in
let ml\_mul\_mono$_{poly}$ = fix((\mlambda{}ml\_mul\_mono$_\000C{poly}$,m,p. if null(p)
then []
else let h.t = p
in ...
fi )) in
if null(p)
then []
if null(q)
then []
else let p1.ps = p
in accumulate(\mlambda{}s,m. ml\_add$_{poly}$(s)(ml\_mul\_mon\000Co$_{poly}$(m)(q)))(...(p1)(q))(ps)
fi in
let ml\_rP\_to$_{poly}$ = fix((\mlambda{}ml\_rP\_to$_{poly}$,stack,L. \000Cif null(L)
then stack
else let op.more = L
in if (op =\msubz{} 1)
then let c.evenmore = more
in let x = if (c =\msubz{} 0)
then []
else [<c, []>]
fi in
ml\_rP\_to$_{poly\mbackslash{}f\000Cf7d$([x /
stack])(...)
if (op =\msubz{} 2)
then let v.evenmore = more
in ml\_rP\_to$_{poly}\mbackslash{}\000Cff24([[ə, [v]>] /
stack])(evenmore)
if (op =\msubz{} 3)
then let q.qq = stack
in let p.s = qq
in ml\_rP\_to$_{poly\mbackslash{}ff\000C7d$([...(p)(q) /
s])(more)
if (op =\msubz{} 4)
then let q.qq = stack
in let p.s = qq
in ml\_rP\_to$_{poly\mbackslash{}ff\000C7d$([...(p)(...) /
s])(more)
if (op =\msubz{} 5)
then let q.qq = stack
in let p.s = qq
in ml\_rP\_to$_{poly\mbackslash{}ff\000C7d$([...(p)(q) /
s])(more)
else let p.s = stack
in ml\_rP\_to$_{poly}\mbackslash{}ff\000C24([ml\_minus$_{poly}$(p) /
s])(more)
fi
fi )) in
hd(ml\_rP\_to$_{poly}$([])(int\_term\_to\_rP(t)))
Date html generated:
2017_09_29-PM-05_55_19
Last ObjectModification:
2017_05_12-PM-11_47_48
Theory : omega
Home
Index