Email Gateway (Aug 19 2022 at 12:38): Email Gateway (Aug 19 2022 at 12:38):From: Walther Neuper <wneuper@ist.tugraz.at>
the definition
definition pcompose :: "'a::comm_semiring_0 poly => 'a poly => 'a poly"
where
"pcompose p q = fold_coeffs (λa c. [:a:] + q * c) p 0"
is not yet used --- what is the purpose of it ?
Walther
Email Gateway (Aug 19 2022 at 12:44):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Walther,
The english Wikipedia defines composition of polynomials as follows: »A
composition of two polynomials is a polynomial, which is obtained by
substituting a variable of the first polynomial by the second
polynomial.« I did not try do match that definition mentally against
the Isabelle definition above, but maybe that's it. You might want to
check it for your own.
Cheers,
Florian
Email Gateway (Aug 19 2022 at 12:44):From: Walther Neuper <wneuper@ist.tugraz.at>
On 11/28/2013 09:22 AM, Florian Haftmann wrote:
Hi Walther,
Am 23.11.2013 15:24, schrieb Walther Neuper:
the definition
definition pcompose :: "'a::comm_semiring_0 poly => 'a poly => 'a poly"
where
"pcompose p q = fold_coeffs (λa c. [:a:] + q * c) p 0"is not yet used --- what is the purpose of it ?
The english Wikipedia defines composition of polynomials as follows: »A
composition of two polynomials is a polynomial, which is obtained by
substituting a variable of the first polynomial by the second
polynomial.« I did not try do match that definition mentally against
the Isabelle definition above, but maybe that's it. You might want to
check it for your own.
value "pcompose [:1,1,1::int:] [:1,1::int:]" --"Poly [3, 3, 1]"
(*substitute for x in (1+x+x^2) by (1+x) = 1 + (1+x) + (1+x)^2 = 3 + 3x + x^2 *)
Cheers,
Florian
Thank you very much -- suppose, this was the last simple question, a new
round of
questions is on the way ;-)
Walther
Last updated: Apr 23 2024 at 20:15 UTC