> It seems to me that a better direction for FriCAS would be to insist
> that this sort of logic remain part of the *type system* of the
> language rather than as values in some new "conditional expression"
> domain.
I tend to support this. However, I don't think that FriCAS would be the
first system that would do that. So before embarking on such a project,
it would be interesting to learn what has already been done in that
direction (not only in panAxiom).
[snip]
> In general functions defined in the FriCAS library should always be
> total over their domains. E.g.
>
> g:Integer->Integer
>
> should have a well-defined value for all values of Integer and not
> generate any run-time exception.
I somehow also like this.
> This philosophy would mean that operations like
>
> /:(Integer,Integer) -> Fraction(Integer)
>
> in Fraction(Integer) are not properly defined in the present code. It
> seems that there is a need for a subdomain of Integer that might be
> called for example NonZeroInteger, similar to PositiveInteger and
> NonNegativeInteger.
>
> /:(Integer,NonZeroInteger) -> Fraction(Integer)
>
> Probably it also makes sense to have NonZero(S:IntegralDomain) as a
> domain constructor in it's own right.
>
> /:(S,NonZero(S)) -> Fraction(S)
> /:(%,NonZero(%)) -> %
Ummmm. Although this idea is good, it will rather soon get messy.
For example, for some reason, I have need for a domain NonOne, NonTwo,
etc. That probably would lead to a Domain constructor
Non(m: Integer): (n: Integer) -> SetCategory
that is definied as a Subdomain of Integer. But then I'd like to have a
domain where two numbers are nonzero. Of course that here is all
artificial, but you see, where it leads to.
> Ideally subdomains should interact with Union so that for example we
> would have the following type equivalence:
>
> PositiveInteger = Union(Zero(Integer),NonNegativeInteger)
corrected:
NonNegativeInteger = Union(Zero(Integer),PositiveInteger)
> However the current implementation of Union in FriCAS is rather
> "brain-dead" in several ways.
Yep. The compiler should understand that this is equal, but... equal
(isomorphic) as what? As sets, or as additive monoids or ...?
In mathematics we take the freedom to add and remove structure as we
like, but here we deal with stupid computers that must be told exactly
what they should do. At least it must be possible to infer the intended
meaning from the context. What SPAD/Aldor needs is a proper language
that makes certain logical specifications accessible to the compiler.
Encoding them in ad-hoc domains as you did with NonZero, is only a first
step but does not bring us to a situation where the compiler is coupled
with a proof-checker that (from the specification) of a function can
reason about the program and possibly optimize.
For example, if somewhere in a program there is
c: Integer := abs(x); -- x is supposed to be any integer
d: Integer := c+1;
q: Fraction Integer := inverse(d::Fraction(Integer));
and the inverse function is defined like
inverse(x:%):% ==
zero? x => error "division by zero";
... here the proper reciprocal value ...
then the compiler should be able to avoid to generate the zero test if
it inlines the 'inverse' in the 'q:=inverse..." line.
But that are future dreams...
Ralf
--~--~---------~--~----~------------~-------~--~----~
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
-~----------~----~----~----~------~----~------~--~---
