> All of this is as is should be for me to write something like:
>
> Ring(a:Symbol,z:Symbol,m:Symbol,o:Symbol) == Join(Associative(a),
> Commutative(a), Identity(a,z), Associative(m), Commutative(m),
> Identity(m,o), ... etc.
>
> Ring("+","0","*","1")
>
> which I expect to export
>
> +:(%,%)->%
> 0:%
> *:(%,%)->%
> 1:%
>
> and to satisfy all of the expected properties.
That doesn't look too bad. But I have some issues.
1) You connect here Symbol with an identifier in the language. So your
"Symbol" domain should be rather something builtin to the language than
just an ordinary library domain.
2) Your approach is a first approximation, but imagine you give some
properties inside Join. It might happen that another property follows
logically from that knowledge base, but you have not explicitly included
it. So it would be nice to state a logical formula for "Commutative(m)"
etc. instead of just giving the property a reasonable name and hide its
meaning in the documentation, in accessible to the compiler.
>>>> Otherwise, one gets into the same trap as the M&M who as able
>>>> to evaluate M * N - N * M to *integer* 0, no matter what M and N
>>>> might be.
>>> I don't see that happening here. Could you explain?
>> Oh, I suspected you would do the same think for commutative
>> operator, Assuming "*" is commutative, how to you simplify
>> the expression M*N - N*M?
> Ok. As you know, unless the expression "M*N - N*M" and it's
> sub-expressions are objects in some domain (such as Expression
> Integer) then the concept of "simplification" is not well defined in
> Axiom. Given such a domain D, we may write:
>
> if D has Commutative("*") then ...
> for example:
> perform some canonical transformation of subexpressions of
> the form x*y based on lexical ordering of x and y.
If you have a domain D that represents its objects without ever storing
"*" (Integer, for example) then what is meant by simplification? Of
course, D can take advantage if it knows that * is commutative, but that
is something else than expression simplification.
>>>> In Implicit System F, or in a forall-quantified style I would write
>>>>
>>>> forall(T: Type) .
>>>> Associative(Modemap(T,T,T): op): Category == with nil
>>>>
>>>> so that when I say Associative(_+$Integer), T gets deduced to
>>>> Integer.
Also here we can end up with an ambiguous situation.
MyInt: with {
+: (%, %) -> %;
+: (String, String) -> String;
} == add {
-- implement something here
}
Now if you say
Associative(+$MyInt)
then that should be rejected by a compiler, since it is ambiguous.
Well, of course, that is a constructed case, but why shouldn't I be
allowed to write MyInt and state associativity of the first + and maybe
some other property for the second? Unfortunately, I am unable to
specify the input for Associative with the current choices (i.e. using $
and/or @).
Ralf
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
