Note: In FriCAS the Can the attribute )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, 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
Since above the definition says Is this the really problem? --yixin.cao, Sat, 26 Jul 2008 00:20:36 -0700 reply 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. Re: nothing to do with the actual names of operations --Bill Page, Sat, 26 Jul 2008 06:24:22 -0700 reply 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! Re: nothing to do with the actual names of operations --hemmecke, Sat, 26 Jul 2008 09:09:01 -0700 reply 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 This looks a little to me like the way the interpreter treats variables. If I say: fricas x
Type: Variable(x)
without declaring But if I really want to I can associate it with some other symbol. E.g. fricas x:Variable(_*):="*"::Symbol
Type: Variable(*)
So let us suppose that the semantics of SPAD is such that
it attempts to evaluate the names of functions and finding
that 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 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. |