On Tue, Aug 5, 2008 at 10:45 PM, Gabriel Dos Reis wrote:
> On Tue, Aug 5, 2008 at 9:10 PM, Bill Page wrote:
>> ...
>> In fact, if I write:
>>
>> MyDomain(): Associative("*")
>>
>> The compiler does generate code with
>>
>> *:(%,%) -> %
>>
>> The associative property is associated with the category 'Associative("*")'
>> but
>>
>> *:(%,%) -> %
>>
>> is exactly what is exported by this category so it is precisely that
>> map to which this property applies.
>
> But then the associative property is associated (no pun intended)
> with the symbol "*": Now you have a category domains with
> associative "*". I cannot name the operation and describe its
> property. I can only name the operator name.
>
In Axiom categories describe properties. 'Associative("*")' is one
category and 'Associative("+")' is another. I am passing "*" and "+"
as parameters, not associating them with some property. I can write:
MyDomain2(): Join(Associative("*"),Associative("+"))
now in the interpreter both
MyDomain has Associative("*")
and
MyDomain has Associative("+")
return true. MyDomain exports both
*:(%,%)-> %
and
+:(%,%)->%
but
MyDomain has Associative("-")
is false. 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.
>> ...
>>> 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.
> ...
>>
>> All category declarations are "logical axioms" in this sense.
>
> well, some of them are purely logical, some are non logical. A category
> that meaningfully exports an operation is not purely logical -- it has
> a computational content.
>
Ok. But by convention the operations that it exports are just those
required to express the associated logical concept.
>
>>>
>>> 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. You can see how this relates to the issue Stephen and
>>> I discussed at the workshop in Hagenber.
>>>
>>
>> Yes, I thought it was an interesting discussion but this machinery
>> strikes me as being to "heavy" for what seems to me to be a relatively
>> simple problem. I am afraid that such changes lead away from the
>> original intend of Spad/Aldor as fundamentally an *algebraic*
>> language. But my ideas about this are only partially formed, so I do
>> want to keep an open mind.
>
> That is interesting.
> I would be highly interested in knowing what you think is not algebraic
> about a universally quantified type.
>
Well, to start with the construction 'Associative(_+$Integer)' is
rather strange. A category is a predicate which identifies a specific
subset of domains (subdomain of Domain), namely those which explicitly
include 'Associative(something)' in a 'Join' or 'with' clause. The
expression '_+$Integer' on the other hand is evaluated as a specific
function exported by the domain 'Integer'. How are we to use this to
imply that the operation exported by Integer is associative? Maybe you
would write:
Integer():Join(Associative(_+$%),...)
If so, then I do not see why you would prefer this over the semantics
of simply passing a symbol.
But this notwithstanding, let me at least try to answer your question
about why I think universal quantification might lead to something
"not algebraic". This is still only "half baked", but I did not mean
to say that there was something necessarily non-algebraic about
universally quantified types. But to be "algebraic" in the (admittedly
still unclear) sense in which I meant it, I think that universal
quantification must enter the language only in a "constructive"
manner. This means (for example) that if I write:
MyDomain(a:MyCatA(x:X)): MyCatB(y:Y)
where the name 'y' does not appear in any expression in the argument
list of MyDomain and 'x' does not appear in any expression of the
category to which MyDomain belongs, then it is correct to interpret
'y' as universally quantified and 'x' as existentially qualified only
in the following sense:
MyDomain(a:Meet(MyCatA(x) for x in X) ): Join(MyCatB(y) for y in Y)
In other words this domain must satisfy all such categories
'MyCatB(y:Y)' for all y in Y. Similarly the parameter 'a' of MyDomain
is a domain that satisfies at least one of the categories
'MyCatA(x:X)' for some x in X. This can be extended to more complex
dependencies in a mostly obvious manner. The significance of these
rules is that we know exactly how to write 'MyDomain', i.e. which
operations to expect from domain 'a' and when operations we must
export.
It is not clear to me if what you are proposing would always fit these
restrictions.
'Meet' is the built-in category constructor dual to 'Join' that was
also briefly discussed at the workshop.In Axiom (but not Aldor!)
'Type' is just the top of the category lattice where all categories
"meet" and which exports no operations.
> ...
>>
>> I took that fact that this approach of passing symbols that are
>> evaluated as names of exported functions "almost works" as evidence
>> that some changes were made to Spad that were intended to make this
>> possible. (Why else evaluate the function names?).
>
> I suspect the right question is why category expressions are evaluated at
> compile time. The answer is to get the list of exported operations.
>
The answer to that question is obvious. But why does it evaluate the
function names? I.e. Given
MyCat(f:Symbol):Category == with
f:X->Y
Why is 'f' in 'f:X->Y' replaced with "*" when I write:
MyCat("*")
Wouldn't it be enough to treat 'f' in this context as a constant
unrelated to the parameter 'f'? Or do you think that this is just an
accident of the design of the compiler?
>> It seems to me that
>> the bug that prevents its full use in the "monoid problem" is not a
>> fundamental design problem but rather something much more technical. I
>> would greatly appreciate any suggestions you have about how to
>> approach debugging this problem.
>
> My immediate question is how do you use it in practice? A monoid
> operation comes with a neutral element. How do you use it?
)abbrev category ID Identity
++ m(u,a)=a and m(a,u)=a
Identity(u:Symbol,m:Symbol):Category == Commutative(m) with
u: () -> % ++ unit
-------
In other words Identity implies the operation is commutative and has a
unit. E.g.
Identity("*","1")
and
Identity("+","0")
> Something I found very effective at testing proposals I've seen so far
> is to construct all the usual algebraic structures up to Lie algebras
> and use them in usual algorithms. That is a good test. Can you
> test that?
>
Someday soon. :-)
Regards,
Bill Page.
-------------------------------------------------------------------------
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
