Francois,
Thank you for reading and considering this list. To some people this
exercise may seem a little pointless - being concerned with mostly
"abstract nonesense" as opposed to "real" programming problems. But I
think the situation is rather similar here to category theory in
mathematics: It seems that if we could just get these fundamentals
correct (e.g. the axioms of category theory), then we can be confident
that a very large part of mathematics can then be consistently and
accurately expressed in this language.
On Thu, May 29, 2008 at 7:59 AM, Francois Maltey wrote:
> Bill Page wrote :
>> 1) Categories and domains are types.
>> 2) Domains satisfy categories only by assertion,
>> 3) It is possible to construct domains that contain types
>> 4) 'Void' is a domain that satisfies no categories except 'Type'
>> 5) Objects /1 are members of 'Domains'
>> 6) In the interpreter the type (domain) of variables can be declared
>> 7) Categories can be passed as arguments
>> 8) But at the present time the type of a variable cannot be a category
>> 9) Is 'Category' the domain of all categories
>> 10) or is 'Category' a category?
>>
> For 6) and 1) I never see x:CategoryXX := ...
> So it seems that variable has ONE value in ONE domain
>
Yes, variables in the interpreter are "domain-valued".
Categories are not a source of "values" as such. Rather we say that
some domain "satisfies" some category, e.g.
Integer has IntegerNumberSystem
True
Float has IntegerNumberSystem
False
But we also have
Integer has Ring
True
Integer has AbelianGroup
True
etc.
This not the same as saying that: "Integer *is* an
IntegerNumberSystem" in the same sense as when we say: "-1 is an
Integer". Categories are logical statements - sometimes called
"contracts", or interfaces or perhaps, abstract algebras. Maybe a bit
like PROPS as discussed here:
http://golem.ph.utexas.edu/category/2008/05/theorems_into_coffee_iii.html
On the other hand Integer is a Domain, in the same sense as -1 is an
Integer,so we can write:
x:Domain := Integer
and even
x:Domain := Domain
i.e. Domain is a Domain.
In the compiler however when we write:
)abbrev domain COMPLEX Complex
Complex(R:CommutativeRing): ComplexCategory(R) with
if R has OpenMath then OpenMath
== add
Rep := Record(real:R, imag:R)
...
R does play a role like a variable. The intention is that one can write
x:Complex X
only if
X has CommutativeRing
The set of domains that satisfy some categoy
{x for x in Domain | x has SomeCategory}
is a kind of subset (subdomain?) of Domain.
I think the interpreter could treat categories this way.
> x :=Integer claims that Integer is a member of a domain : Domains.
> x : Domains := Integer
>
Yes.
> x :Category:= ThisCategory means that Category is also a domain.
>
I proposed above that in this context a category should denote a
subdomain of Domain, i.e. those domains that satisfy the category.
> I feel that no axiom can hold any category. A category adds functions to
> an "object".
>
In the compiler categories are used to specify exports. Because the
concept of "satisfaction" is defined (in part) in terms of the
operations exported by a domain, I think this difference in usage
remains consistent.
> And I'm waiting about functions : what are the type/domain of functions
>
The domain of a function is called 'Mapping'.
> f (x) == 2*x
This is not a function - it is a "mode". In a given context it can be
compiled into a function. The underlying domains of the mapping will
be inferred.
> g(x:Integer) : Integer==3*x
>
The domain of g is
Integer -> Integer
which is also written
Mapping(Integer,Integer)
> h := x +-> 4*x --- an anonymous function
> k: Integer -> Integer := x +->5*x -- not yet possible...
>
This works for me:
(1) -> k: Integer -> Integer := x +->5*x
; (DEFUN |*1;anonymousFunction;1;frame1392;internal| ...) is being compiled.
;; The variable |*1;anonymousFunction;1;frame1392;internal;MV| is undefined.
;; The compiler will assume this variable is a global.
(1) theMap(*1;anonymousFunction;1;frame1392;internal)
Type: (Integer -> Integer)
(2) -> k(3)
(2) 15
Type: PositiveInteger
> Last related question :
>
> Imagine I want to have rewrite functions over every trigonometric
> expressions, not only Expression Integer, nor Expression
> DomainXXX, but over all sort of expressions.
>
Becareful! 'Expression Integer' means rational functions (a ratio of
polynomials) with Integer coefficients, defined recursively over a
large set of additional kernels. Do not confuse this with the general
concept of a general "expression".
> The place of this rewrite/expand/combine function is in
> TrigonometricFunctionCategory (see trigcat.spad file).
>
I disagree. This category only specifies the trigometric functions,
not manipulations of trigonometric expressions.
)abbrev category TRIGCAT TrigonometricFunctionCategory
++ Description: Category for the trigonometric functions;
TrigonometricFunctionCategory(): Category == with
cos: $ -> $ ++ cos(x) returns the cosine of x.
cot: $ -> $ ++ cot(x) returns the cotangent of x.
csc: $ -> $ ++ csc(x) returns the cosecant of x.
sec: $ -> $ ++ sec(x) returns the secant of x.
sin: $ -> $ ++ sin(x) returns the sine of x.
tan: $ -> $ ++ tan(x) returns the tangent of x.
add
if $ has Ring then
csc x ==
(a := recip(sin x)) case "failed" => error "csc: no reciprocal"
a::$
sec x ==
(a := recip(cos x)) case "failed" => error "sec: no reciprocal"
a::$
tan x == sin x * sec x
cot x == cos x * csc x
> In this case I must be able to pick up the x in sin x, and play with
> this x even if I don't know the domain of x...
This is what the definitions of 'csc', 'sec', 'tan' and 'cot' do
above. They only require that the domain of x has Ring. But I do not
think that is what you have in mind.
>
> How is it possible ?
> I have 2 examples in mind.
> How can I expand (sin (3*x)) ?
>
> and how can I expand (exp (a+%i*b)) in exp a * (cos b + %i * sin b).
Manipulating expressions is a completely different problem then the
definition of various trigonometric functions. Probably the right
place for this would be in a package like TRIGMNIP
(TrigonometricManipulations).
> In this last case I must be able to recognize the domain :
> Expression Complex Integer or Expression XXXX Complex YYYYYYY, as
> Expression Fraction Complex Integer and Expression Complex Fraction
> Integer or others.
>
Even if you do not allow Complex coefficients in the rational
functions, that does not imply that the expressions are real-valued.
For example, I can write:
(1) -> sin(sqrt(-1)*x+1)
+---+
(1) sin(x\|- 1 + 1)
Type: Expression Integer
Currently there is no symbolic domain in panAxiom where symbols like
'x' are restricted to values from a given domain. If I write:
n:Integer
then I cannot write
sin(2*%pi*n)
The best I can do is:
(1) -> n:Union(Variable n,Integer)
Type: Void
(2) -> sin(2*%pi*n)
(2) sin(2n %pi)
Type: Expression Integer
But then in (2) n is treated like any other Symbol.
See:
http://axiom-wiki.newsynthesis.org/SandBoxSymbolic
for some more musings about this issue.
Regards,
Bill Page.
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
