Can anyone explain me the following behavior of Sage: What is the idea behind not evaluating symbolic equations which are (obviously) true? For example:
sage: m = var('m')
sage: m == m
m == m
Evaluation works with
sage: bool(m == m)
True
I can think of a few reasons:
(1) Symbolic equations and boolean values are different kinds of thing, and magical coercions like that should be avoided as a general principle. For example, if it autocoerces, it would be awkward to print out a symbolic expression that Sage decides is true. You also couldn't start from a known true equation and work toward something else.
(2) If you have a list of symbolic equations and you substitute values into them, with this autocoercion you could wind up with a list of symbolic equations and some boolean values scattered in. You can't continue to substitute into boolean values, so now you have to write every line of symbolic manipulation code with branches just in case your expression is suddenly a Python bool.
(3) How are you going to decide when to convert to boolean or not? You can't let it return False, because Sage will return False even if something is true but it can't prove it. So you could only ever coerce when Sage decides it's true, which means it'd be hard to explain the conditions under which the coercion took place, among other reasons because
(4) This means that Sage will have to either try to convert every symbolic expression to a boolean, which can sometimes be really slow, or you'll have to have a set of conditions to decide when to give up on trying to prove something, and those will be pretty arbitrary by necessity.
ISTM there would be lots of disadvantages to this autocoercion and I can't think of a significant advantage it offers. All of my objections are consequences of (1), really: an expression is a different kind of thing than a boolean, and both are useful.
Asked: 2011-11-03 05:44:22 +0100
Seen: 646 times
Last updated: Nov 03 '11
Copyright Sage, 2010. Some rights reserved under creative commons license. Content on this site is licensed under a Creative Commons Attribution Share Alike 3.0 license.
