

last edited 6 years ago by test1 
1 2 3 4 5 6 7 8 9 10 11  
Editor: test1
Time: 2013/07/31 16:04:00 GMT+0 

Note: 
added: 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. changed: \begin{spad} )abbrev category COM Commutative Commutative(n:String):Category == with () \end{spad}  \begin{spad} )abbrev domain COMD CommutativeDomain CommutativeDomain(): Commutative("*") with  coerce:%>OutputForm  == add  coerce(x)== x pretend OutputForm \end{spad}  \begin{axiom} CommutativeDomain has Commutative("*") CommutativeDomain has Commutative("+") \end{axiom} )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("+") changed: \begin{spad} )abbrev category COM2 Commutative2 Commutative2(T:Type,s:Symbol):Category == with  s:(T,T) > T \end{spad}  \begin{axiom} )show COM2(Integer,"*") )show COM2(Float,"+") \end{axiom}  \begin{spad} )abbrev domain COMD2 CommutativeDomain2 CommutativeDomain2(): Commutative2(%,"*") with  coerce:%>OutputForm  == add  coerce(x)== x pretend OutputForm  x * x == x \end{spad}  \begin{axiom} )sh CommutativeDomain2 CommutativeDomain2 has Commutative2(CommutativeDomain2,"*") CommutativeDomain2 has Commutative2(CommutativeDomain2,"+") \end{axiom} )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
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 *.
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.
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!
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.
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?
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 symbollike 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.