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.