# Re: [isabelle] Formal_Power_Series.thy and inversion

`First of all: There are no non-total functions in HOL. If you take the
``first element of the empty list, if you divide by zero, if you evaluate
``0^0, you always get /some/ result; there is just no other way in that
``logic. The question is: What result do you get?
`

`One approach is to leave it unspecified (e.g. using HOL's "undefined" or
``something like that), then you simply don't know or care (logically)
``what that element is. But it still /is/ an element (i.e. 1/0 is a real
``number, you just don't know which number), and it's always the same
``number, so e.g. "1/0 - 1/0 = 0" holds.
`

`In my experience, it is usually a lot less painful to adopt conventions
``like "x / 0 = 0 for all x". This diverges from mathematical convention,
``but as I said, you simply cannot have âcompletely undefinedâ expressions
``in HOL, and if you must return some value, you might as well choose a
``convenient one. Choosing "x / 0 = 0" has the advantage that a number of
``nice properties of division still hold without additional conditions,
``which makes rewriting arithmetic terms less painful. Of course, as an
``Isabelle user, you have to /know/ what this means.
`

`A similar issue is the sum over an infinite set, which is always 0 in
``Isabelle. One may naÃvely expect that "(ânâ{1..}. 1/n^2) = ÏÂ/6", but it
``is in fact zero by definition, and if one wants an actual infinite sum,
``one has to use another concept of "sum", e.g. "suminf"/"sums" or the
``measure-theoretic one.
`

`Therefore, the justification of choosing fps_inv as 0 for inputs that
``don't have an inverse is simply that it you can't return a "proper"
``result, so you might as well return a "convenient" dummy result.
`

`Second, I think you may be confused by what fps_inv actually is. fps_inv
``is the /compositional/ inverse of formal power series. Therefore,
``cancelling "X * fps_inv X" to "1" makes no sense to me at all. In fact,
``"fps_inv X = X", and "X" plugged into "X" yields "X", which is the
``compositional identity, as expected.
`

`Perhaps you mean the /multiplicative/ inverse? This is simply "inverse
``X", which is defined like this:
`
fun natfun_inverse:: "'a fps â nat â 'a"
where
"natfun_inverse f 0 = inverse (f$0)"

`| "natfun_inverse f n = - inverse (f$0) * sum (Îi. f$i * natfun_inverse
``f (n - i)) {1..n}"
`

`definition fps_inverse_def: "inverse f = (if f $ 0 = 0 then 0 else
``Abs_fps (natfun_inverse f))"
`

`Thus, "inverse X" is indeed 0 in Isabelle. This is because X simply does
``not have an inverse in the ring of formal power series and we have to
``return something.
`

take X*(fps_inv X).
If I cancel first then I get =1

`If I evaluate (fps_inv X) first I get =0
`

`Okay, so you probably again mean "X * inverse X" here. You are correct
``that you can evaluate "inverse X" to "0", and then you get "X * 0 = 0".
``However, you can /not/ cancel "X * inverse X" to get "1". The law "f *
``inverse f = 1" only holds if "f $ 0 â 0", as you can see in this theorem:
`
lemma inverse_mult_eq_1':
assumes f0: "f$0 â (0::'a::field)"
shows "f * inverse f = 1"

`You can't do any better than this if you want to stay in the type "'a
``fps". If you want multiplicative inverses for all non-zero formal power
``series, you have to go to the ring of formal Laurent series, do your
``stuff there, and then go back to the ring of formal power series once
``you're done. This is perhaps a bit odd for a mathematician, but I'm
``afraid that's how things are in a typed logic like HOL.
`

`However, note that you can write things like "X^2 / X" in the ring of
``formal power series (as long as the coefficients are a field), which
``evaluates to "X" as expected. For "'a :: field fps", a power series
``divides another iff the subdegree of the former is smaller than that of
``the latter, and we have a full Euclidean ring structure on FPSs, i.e. we
``have well-behaved division and remainder operations "div" and "mod" just
``like on integers or polynomials. I think this is probably enough and
``probably less painful than going to formal Laurent series.
`

`Note that, due to somewhat unfortunate notation, "f / g" on formal power
``series is not the same as "f * inverse g". It is the same if g is a
``unit, but otherwise, "f / g" is essentially what you get when you
``compute "f / g" in the ring of formal Laurent series and then cut off
``all the terms with negative exponents, and "f mod g" is the remainder,
``i.e. "f - (f / g) * g".
`
If you only want to divide by powers of X, you can also use fps_shift.

How can I trust a system where 0=1, depending upon order evaluation?

`Well, you can't. Luckily, Isabelle is (hopefully) not such a system. It
``is a core principle of Isabelle that definitions should never be able to
``introduce inconsistencies.
`

Could you send me a copy?

`It's currently broken in ways that I don't understand, but I'll attempt
``to fix it and then I can send it to you. I'm not sure if it will be very
``helpful; it was never more than a small experiment.
`

Her article is behind a paywall I can't afford:
https://link.springer.com/article/10.1007/s10817-010-9195-9

`I know Amine's article and it really doesn't say very much about Laurent
``series. It essentially describes that one can define them as "'a fps
``fract" in the way I did in my experiment and nothing more. I don't think
``Amine ever actually had the time to build a library of facts about
``Laurent series.
`
Cheers,
Manuel

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*