On 01/14/2012 04:19 PM, Gabriel Dos Reis wrote:
There are situations where one has to amend the proposal. For example,
consider the following:
)abbrev domain MYDOM MyDomain
MyDomain(T: SetCategory): Public == Private where
Public == SetCategory with
myDomain: T -> %
Private == T add
myDomain t == per t
Here, none of the operations exported by SetCategory is directly
implemented by MyDomain. Should the compiler abort compilation right away?
My answer is no.
Of course that should be accepted without any warning or error.
The compiler can assume that T implements all exports of SetCategory.
Together with the explicit definition of myDomain, that should be enough
to prove (at compile-time) that MyDomain has an implementation for all
its exports.
The reason is that those operations may be provided
by the actual argument T. And indeed, that is what is expected in that
definition -- operations not directly implemented in the constructor
MyDomain are to be looked up in the base domain and possible defaults.
Can the compiler find those apparently missing operations while
compiling MyDomain? No, there is no domain constructor it can look
into. It has to *assume* that the missing operations will come from T.
Yes, to *assume* is OK in the above case. All I was asking for was an
algorithm that leads to a compile time check for all the implemented
functions. Since with complicated conditions that is probably
undecidable, the algorithm should at least catch the easy cases.
For constructor arguments that are not type, I believe one has to wait for
the actual value; one does not need "odd? random()" for that.
Consider the case of category ComplexCategory for example. At the moment,
all flavours of AXIOMs cheat with
if R has Field then -- this is a lie; we must know that
Field -- x**2+1 is irreducible in R
whether 'x^2 + 1' is irreducible in R is not a simple condition known to
the compiler (at least not as simple as has tests) since the exponention
and addition operations can be arbitrary user code.
IMHO this test is wrong. It should be minusOneIsNotASquare(R). In the
"add" part, one will probably have something like
if minusOneIsNotASquare(R) then
-- implementation of field operations
The compiler does not have to evaluate minusOneIsNotASquare(R), it just
must check that for both cases, i.e. if minusOneIsNotASquare(R) returns
true/false all the respective operations are implemented.
Of course, one has to assume that this function is without side effects
and deterministic.
The only problem I see, is where the test (function) in the category
part is not identical with the test (function) in the implementation
part, because then one would have to evaluate the function or there
would be some language extension that allows some theorem proving that
could be used by the compiler without evaluating the test function.
For has-tests cases, the complexity can be bad in practice.
If already has-tests can be rather complex there is probably not much
hope for the more complicated cases. Do you happen to know which
constructor it is. I faintly remember that AGG takes quite a lot of
time. Maybe one should look at the source code and simplify that a bit?
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.
