On Tue, Jul 6, 2010 at 1:58 PM, Ralf Hemmecke wrote:
>
> My dream would actually be something like
>
> /: (%, NonZero %) -> %
>
> Which would mean that the zero test would be at the time when one has to
> coerce an element from % to NonZero(%). An implementation of / would be
> certain that it never gets 0 as its second argument.
>
> I don't yet know whether that makes much sense. I would rather like that
> there were a way to specify logical formulae that I can connect to the
> type system.
>
+1 I think this is absolutely correct. In fact this was the original
intention of introducing subdomains into the language -
notwithstanding that the current implementation has many problems. I
suppose that what Waldek is saying is that fully implementing this in
a type system like Axiom's is a difficult and in some cases formally
unsolvable problem.
I think this is related to another recent thread on equality in Ring.
The issue there seemed to be that it is unrealistic to expect that
equality can always be evaluated to a Boolean value - true or false.
In some cases we might be formally required to answer "don't know".
Logicians have spent a lot of time worrying about how to model such
situations giving for example specific axioms that allow one to deal
with various non-Aristotelean cases such as "it is provable that", "it
is known that", "it is possible that", "it is necessary that", etc.
I think it might be interesting to observe how this is implemented in
the "assume" facility in Maple. There the operator 'is(...)' evaluates
to true only if it is necessarily that case that (...) holds "in all
possible worlds":
"The is routine determines whether x1 satisfies the property prop1. It
returns true, false, or FAIL. The is routine returns true if all
possible values of x1 satisfy the property prop1. The is routine
returns false if any possible value of x1 does not satisfy the
property prop1. The is function returns FAIL if it cannot determine
whether the property is always satisfied. This is a result of
insufficient information or an inability to compute the logical
derivation."
There is also a dual operator named 'coulditbe(...)':
"The coulditbe routine determines whether there is a value of x1 such
that prop1 is satisfied. It returns true, false, or FAIL. The
coulditbe routine returns true if there is a possible value of x1 that
satisfies prop1. The coulditbe routine returns false if all possible
values of x1 do not satisfy the property prop1. The coulditbe routine
returns FAIL if it cannot determine whether the property is true or
false. This is a result of insufficient information or an ability to
compute the logical derivation.
The environment variable _EnvTry can be used to specify the intensity
of the testing by the is and coulditbe routines. Currently _EnvTry can
be set to normal (the default) or hard. If _EnvTry is set to hard, is
and coulditbe calls can take exponential time."
If nothing else is known about 'a' and 'b' then we get the following result:
> is(a = b);
false
> is(a = a);
true
> coulditbe(a = b);
true
>
Perhaps how something like this should interact with a fully typed
language is still somewhat of a research topic?
Regards,
Bill Page.
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
