Re: [Axiom-mail] A question about Axiom capabilities

[Gabriel Dos Reis]

On Fri, Apr 5, 2013 at 11:05 AM, Martin Baker <address@hidden> wrote:
> On 05/04/13 12:11, Gabriel Dos Reis wrote:
>> Your probably know that OpenAxiom started putting the axioms in AXIOM.
>> See for example:
>>
>>
>> http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
>>
>> In fact, a couple of years ago, a student of mine did experiments on
>> exploiting these axioms to help code generation and automatic
>> parallelization.  The results were very encouraging (see the
>> yli-sandbox for example.)
>>
>> OpenAxiom is very much committed to get the axioms integrated to the
>> entire type checking and elaboration process.
>
> Gaby,
>
> Thanks, I find this stuff interesting, Its not that I expect it to appear in
> any flavour of Axiom soon (feel free to correct my assumptions), its just
> that I like to know how things work, what can and what can't be done.
>
> AFSICS axioms are currently embedded in the inline documentation for the
> category like this:
>
> snippet from:
> http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
> ++ Axioms:
> ++   \spad{associative("+":(%,%)->%)}\tab{30}\spad{ (x+y)+z = x+(y+z) }
> ++   \spad{commutative("+":(%,%)->%)}\tab{30}\spad{ x+y = y+x }
> AbelianSemiGroup(): Category == SetCategory with

We did not get time to convert all the comments into code as is done
for some the new categories and domains in the trunk repository.
For example, from

http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet

you see:

SemiGroupOperatorCategory(T: BasicType): Category ==
  BinaryOperatorCategory T with
    assume associativity ==
      forall(f: %, x: T, y:T, z: T) . f(f(x,y),z) = f(x,f(y,z))

and

MonoidOperatorCategory(T: BasicType): Category ==
  SemiGroupOperatorCategory T with
    neutralValue: % -> T
      ++ \spad{neutralValue f} returns the neutral value of the
      ++ monoid operation \spad{f}.
    assume neutrality ==
      forall(f: %, x: T) .
         f(x, neutralValue f) = x
         f(neutralValue f, x) = x

The general idea is that most of the axioms and properties are
with the operations, not the carrier sets of structures (as currently
done for old domains.)  That entails some redesign of the
category and domain hierarchies.  We didn't get around to finish
the conversion; plus Yue  is no longer working in this area.

> I had a rummage about in the sandbox you mentioned (written by Yueli about 3
> years ago) and I did not come across any overall tutorial file (what I would
> think of as top level documentation) I may have missed it. Did Yueli write
> any thesis or anything like that?

unfortunately, no.  What I have are internal reports we didn't to put
in shape that is publishable, even as technical reports.

> At first glance it does look encouraging as the code to analyse the code
> does seems to be written in SPAD, which hopefully shows that it can be done.

Yes, most of the code was written in Spad; some hooks into the parser was
needed, but the elaboration, and the whole static analysis is written in Spad.

(By the way, I used OpenAxiom in 2006 and 2008 for static analysis and
compiler courses so, there was precedent for writing the "compiler stuff" in
Spad.  Some improvements were needed to make the whole experience palatable
though -- for example, that is why we have a Syntax domain, some form of
pattern matching, user-defined case operator, existential type, etc.)

> When I look at the code (such as snippet below) it looks like the axioms are
> coded differently, that is on a per operator basis?

Yes, I explained above many properties are with the operators, not the
carrier set -- Integer can be the carrier set for many monoidal structures.

>
> snippet from:
> http://sourceforge.net/apps/trac/open-axiom/browser/yli-sandbox/contrib/redec/operatorcats.spad?rev=2776
> )abbrev category ASSOCOP AssociativeOperator
>   ++ Axiom: associativity: rule op(a, op(b, c)) == op(op(a,b), c)
>   AssociativeOperator(T: SetCategory, op: Mapping(T, T, T)):Category
>     == MagmaOperator(T, op)
>
> Any further clues for understanding the code appreciated, thanks,

The main trunk has the axioms integrated in codes.  One of the reasons why
Yue used the old commentary style to write some of the axioms is that he
needed to analyse the entire algebra set (which he did), but he did
not have the time
to redesign the entire algebra hierarchy.  After the positive
preliminary reports,
we headed for getting some results out (see the ISSAC 2011 paper); and
after that
he changed fields of studies.

-- Gaby