Note: In FriCAS the commutative("*") attribute is replaced by CommutativeStar catogory. The disscussion below is kept as it raises some issues that are still relevant.

Can the attribute commutative("*") be replaced with a category definition like

)abbrev category COM Commutative Commutative(n:String):Category == with ()

)abbrev domain COMD CommutativeDomain? CommutativeDomain?(): Commutative("*") with coerce:%->OutputForm? == add coerce(x)== x pretend OutputForm?

CommutativeDomain? has Commutative("*") CommutativeDomain? has Commutative("+")

That is amazing. As demonstrated above, CommutativeDomain is just declared to be Commutative("*") even though there is no exported operation *.

In fact, what is demonstrated here has nothing to do with the actual names of operations exported by a domain, but just with the declaration that CommutativeDomain is of category Commutative("*").

Since above the definition says Commutative(n:Symbol) there should be double quotes around the *.

Even such a category is possible, so we can define domain D:Join(Commutative(*),Commutative(+),Commutative(max),....). But when I need to write a algorithm package to do some computations on that domain, in which I have several new functions(supposed all (D,D)->D), say, f1, f2, f3, how do I say f1 and f3 are commutative, while f2 is not?

One choice is adding properties inference with static analysis into the compiler(is there a possibility this inference algorithm be designed perfect?). Another is to define the property commutativity directly on the function *, instead of the domain. Or both.

It is equally true that attributes like commutative("*") have nothing to do with the actual names of operations. So I think that this use of categories is functionally equivalent to the use of attributes.

yixin.cao, I do not see anything wrong with writing, for example:

  Dpackage(): Join(Commutative("f1"),Commutative("f3", ...) with
    f1:(D,D)->D
    f2:(D,D)->D
    f3:(D,D)->D

To me this a reasonable encoding of the idea that "f1 and f3 are commutative, while f2 is not". But of course it is only referring to the symbols/strings "f1" etc. and not the actual functions.

I think it is possible to try something a little more ambitious that at least appears to relate to the names of functions.

)abbrev category COM2 Commutative2 Commutative2(T:Type,s:Symbol):Category == with s:(T,T) -> T

)abbrev domain COMD2 CommutativeDomain2? CommutativeDomain2?(): Commutative2(%,"") with coerce:%->OutputForm? == add coerce(x)== x pretend OutputForm? x x == x

Now, I do consider the fact that this works rather amazing!

I strongly dislike:

  Commutative2(T:Type,s:Symbol):Category == with
    s:(T,T) -> T

until somebody tells me that an identifier in the language is connected to Symbol (which is a library domain). That this works is magic and requires that Symbol is built into the compiler.

Disliking some feature of SPAD because it is not part of some specification of the language and requires that something defined in the library is also built into the compiler would classify many other features of SPAD as magic. Unless we decide to remove this feature, I think we need to imagine some semantics that would make sense of it.

This looks a little to me like the way the interpreter treats variables. If I say:

x

(1)

without declaring x, the interpreter evaluates x as a value of the domain Variable(x).

But if I really want to I can associate it with some other symbol. E.g.

x:Variable(_*):="*"::Symbol

(2)

So let us suppose that the semantics of SPAD is such that it attempts to evaluate the names of functions and finding that s above is a parameter it uses it's value * as the name of the function. Does that make sense?

I agree that the interpreter is allowed to do magic things. But we are speaking of SPAD here. So if the SPAD compiler is allowed to match (or convert) something of type Symbol with the name of a function. Then Symbol must be known to the compiler.

But suppose I don't use the current algebra library of panAxiom and create a library that does not implement Symbol or that calls its symbol-like domain MySymbol. What will the compiler do in that case? I said that I strongly dislike above, because I would like to have a language that does not have things builtin which are unnecessary.

I would rather like to be able to specify axioms via a predicate logic language than doing this workaround of specifying axioms by giving a category. The real logical condition currently just appears in comments and thus is inaccessible to the compiler.