On 8/28/08, Raymond Toy <raymond.toy at ericsson.com> wrote:
> How would such a tagged inf be printed? Will it be printed inf<junk>?
> Or just inf?
All tagged infs should be displayed the same, at least for ordinary
pretty-printed output.
The output of grind is ostensibly a representation which can be
read as input. If so, maybe the tags should be displayed in
grind output. Or maybe grind should print all tagged infs as just
"inf" but the parser should generate a tag for every such input.
Something to think about.
> With or without tagging, I'm not sure I like the example of x-x
> returning 0, but inf-inf being undefined. I find that rather confusing.
To be clearl, the result should be something like
x - x => 0 assuming finitep(x)
where I've introduced two vaporware concepts, "assuming" where
the rhs is a list of conditions which apply to the lhs, and finitep(x)
which asserts x is not infinite. To round it out, we could have
declare(x, finite) and declare(x, potentially_infinite) or some such
nuttiness. We could have a default assumption that variables are
finite unless declared otherwise; I guess then x - x => 0 for all
variables not declared potentially infinite, and some guarded
expression otherwise.
Maybe instead of finitep(x) and declare(x, finite) we should phrase
everything in terms of sets, e.g. is(x in R) and declare(x in R),
declare(x in union(R, {inf, minf})). Some days I'm really psyched
about declarations like that.
FWIW
Robert Dodier