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 Since above the definition says 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 replyyixin.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(%," Now, I Re: nothing to do with the actual names of operations --hemmecke, Sat, 26 Jul 2008 09:09:01 -0700 replystrongly 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. 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: 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 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 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. |

Is this the really problem?--yixin.cao, Sat, 26 Jul 2008 00:20:36 -0700 reply