Yes, there's lots of free and open-source computer algebra systems out there, of which Sage is probably the most-used. I have access to Mathematica and others on the school's computers, but I think it's obvious why I'd prefer something open-source -- a proof should be verifiable, and if you use a CAS computation for a proof, then your CAS's source code is implicitly part of the proof.
You see, I've got this program that I've written in Haskell that needs to do a bunch of comparisons of numbers made from logs. Lots of numbers like 2-3log32 floating around, you see[0]. Now, so far double precision has been more than enough, but as I compute farther that may well cease to be the case. So I downloaded an arbitrary-precision arithmetic library, ERA, which unfortunately is rather slower than just using doubles, but does the job... mostly.
There's actually a serious problem with ERA -- when I say "arbitrary precision", that means I want comparisons to be *correct*. If I ask whether than one number is less than a number, it should compute until it can tell. Unfortunately that's not what it does, meaning it doesn't do what I care about. 40 digits is better than what you'll get with doubles, and almost certainly good enough, but do I have a guarantee that it's good enough? No? Then I don't have a proof.
And of course there's a more fundamental problem: No matter what your arbitrary precision arithmetic library, there's no way you can verify equality in finite time by computing more digits! Currently in my program I've worked around this by doing such tests via integer arithmetic whenever equality is actually possible... but if I want this thing to accept more general inputs, I'm not going to be able to predict in advance when that could happen and route around it. No, if you want to verify equality, you need to be able to do symbolic computations, and that means a CAS. Well, either that or rolling my own linear-combination-of-logs type and then converting all comparisons to integer arithmetic (since I'm too lazy to learn what the fast algorithms might be). Seriously though, this thing is slow enough already.
So why not just use Sage? Well, there's a good chance I will, but... Sage is based on Python. Now I wrote this program in Haskell. No, rewriting it in another language doesn't in general bother me, but there's a reason I picked Haskell. You know what I like about Haskell? It's really easy to define nice, simple, algebraic datatypes. You know, like if you wanted to define linked lists -- they're built in so you don't need to, of course, but if you wanted to, it would just be something like
data List A = Nil | Cons A (List A)
...and boom, you've got linked lists, and you can start defining functions on them.
Python... well, it's been a long time since I looked at Python, but as I recall, it goes the object-oriented route when it comes to defining new datatypes. And, well, ew. I want immutable datatypes I can define simply and operate on algebraically. Does it even support union types? I doubt it. I mean, you can work without union types, but I'm thinking in terms of Haskell which makes them simple and convenient, and to me they just seem the right way to do things, rather than having members which might be null or whatever the equivalent is. Not to mention Python is dynamically typed, so you can't even tell whether you've written something meaningful until you run it.
Now I don't need much, I just need the ability to compare numbers with logarithms in them (and take their floors and ceilings), and get the comparison correct, guaranteed, in finite time. You shouldn't, strictly speaking, need a whole CAS for that; but it's the sort of thing that you don't tend to find outside of one. I don't think I see a Haskell package that can do it (though I suppose I could have missed it). I don't want to take the time learn how to do it myself, and I don't want to convert everything to integer arithmetic, because I'm afraid that would be slow -- well, unless that that *is* how a CAS would do it, in which case I assume it really is the best way.
In short, I like Haskell because it's so algebraic, it's a lot like just writing math, and I would like a CAS that also has that property -- not just when you're using its built-in data types, but when working with your own weird tree type which you've implemented as a union type and you want it to do compile-time type checking so you can be sure you've written something meaningful.
...I guess I mostly just want a CAS based on Haskell, when you get down to it. I guess ML would be fine too. :P Anyway, I don't suppose there are any open-source CAS'es out there that do what I want? Anyone know one that would be close, at any rate? Or am I just going to have to end up either using Sage or rolling my own slow comparisons?
-Harry
[0]I'll write about just what it does later. I'm sure the constant involved has tipped you off that it's related to integer complexity.
You see, I've got this program that I've written in Haskell that needs to do a bunch of comparisons of numbers made from logs. Lots of numbers like 2-3log32 floating around, you see[0]. Now, so far double precision has been more than enough, but as I compute farther that may well cease to be the case. So I downloaded an arbitrary-precision arithmetic library, ERA, which unfortunately is rather slower than just using doubles, but does the job... mostly.
There's actually a serious problem with ERA -- when I say "arbitrary precision", that means I want comparisons to be *correct*. If I ask whether than one number is less than a number, it should compute until it can tell. Unfortunately that's not what it does, meaning it doesn't do what I care about. 40 digits is better than what you'll get with doubles, and almost certainly good enough, but do I have a guarantee that it's good enough? No? Then I don't have a proof.
And of course there's a more fundamental problem: No matter what your arbitrary precision arithmetic library, there's no way you can verify equality in finite time by computing more digits! Currently in my program I've worked around this by doing such tests via integer arithmetic whenever equality is actually possible... but if I want this thing to accept more general inputs, I'm not going to be able to predict in advance when that could happen and route around it. No, if you want to verify equality, you need to be able to do symbolic computations, and that means a CAS. Well, either that or rolling my own linear-combination-of-logs type and then converting all comparisons to integer arithmetic (since I'm too lazy to learn what the fast algorithms might be). Seriously though, this thing is slow enough already.
So why not just use Sage? Well, there's a good chance I will, but... Sage is based on Python. Now I wrote this program in Haskell. No, rewriting it in another language doesn't in general bother me, but there's a reason I picked Haskell. You know what I like about Haskell? It's really easy to define nice, simple, algebraic datatypes. You know, like if you wanted to define linked lists -- they're built in so you don't need to, of course, but if you wanted to, it would just be something like
data List A = Nil | Cons A (List A)
...and boom, you've got linked lists, and you can start defining functions on them.
Python... well, it's been a long time since I looked at Python, but as I recall, it goes the object-oriented route when it comes to defining new datatypes. And, well, ew. I want immutable datatypes I can define simply and operate on algebraically. Does it even support union types? I doubt it. I mean, you can work without union types, but I'm thinking in terms of Haskell which makes them simple and convenient, and to me they just seem the right way to do things, rather than having members which might be null or whatever the equivalent is. Not to mention Python is dynamically typed, so you can't even tell whether you've written something meaningful until you run it.
Now I don't need much, I just need the ability to compare numbers with logarithms in them (and take their floors and ceilings), and get the comparison correct, guaranteed, in finite time. You shouldn't, strictly speaking, need a whole CAS for that; but it's the sort of thing that you don't tend to find outside of one. I don't think I see a Haskell package that can do it (though I suppose I could have missed it). I don't want to take the time learn how to do it myself, and I don't want to convert everything to integer arithmetic, because I'm afraid that would be slow -- well, unless that that *is* how a CAS would do it, in which case I assume it really is the best way.
In short, I like Haskell because it's so algebraic, it's a lot like just writing math, and I would like a CAS that also has that property -- not just when you're using its built-in data types, but when working with your own weird tree type which you've implemented as a union type and you want it to do compile-time type checking so you can be sure you've written something meaningful.
...I guess I mostly just want a CAS based on Haskell, when you get down to it. I guess ML would be fine too. :P Anyway, I don't suppose there are any open-source CAS'es out there that do what I want? Anyone know one that would be close, at any rate? Or am I just going to have to end up either using Sage or rolling my own slow comparisons?
-Harry
[0]I'll write about just what it does later. I'm sure the constant involved has tipped you off that it's related to integer complexity.
