Axioms in Axiom

Warning: There is some unfortunate notational overloading here. I'll try to use a capitalised 'Axiom' for the program (any flavour) and lower case 'axiom' for the mathematical concept. I'll try to make the word 'category' clear by the context.

Motivation

There are various ways to divide up mathematics. The Axiom program (here I mean pan-Axiom) generally aligns with these, but there is a slight mismatch.

An Axiom category has little definition of its axioms. Of course a domain must respect its axioms but they are not yet explicitly and automatically policed or available to SPAD or external code.

theories

I guess we can roughly characterise what is required in a category as

It seems to me that It would be very useful to have axioms defined within categories, for many reasons, including such things as:

Gabriel Dos Reis and Yue Li have done a lot of work on specifying axioms in a category and it is starting to appear in OpenAxiom. Three years ago Yue Li used an early version of this for:

His code is here and there is some information here.

I would like to help and encourage, in my own small way, putting axiom information in OpenAxiom categories and it seems to me that there is a need to fill the documentation/tutorial holes. I would also like to make information about this available to the Axiom and FriCAS projects in the hope that they might join in.

'assume' Syntax

OpenAxiom and the sandbox code written by Yue Li has gone through some changes and it is not yet completely in its final final form. So its probably best if I try and write down where it is headed but, just to explain existing code, these are roughly the stages:

Stage 1 - axioms in inline comments in existing categories.

snippet from here

++ 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
Stage 2 - Operator categories added so that axioms can be defined on a per operator basis

snippet from here

)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)
Stage 3 - 'assume' syntax (still on a per operator basis) .

Snippets from here

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
      

So extra syntax has been added in to encode the axioms, it would help to have a more precise definition of this extra syntax, here is my first try to reverse engineer the openAxiom syntax (in a semi-formal syntax - not quite the full EBNF to try to make it more readable):

syntax

where:

Using axioms from within SPAD

SPAD does already have a mechanism for specifying rewrite rules (described on the page here. Could this be extended to allow, for instance, identities to be specified as part of each category and domain and to be inherited in the same way that the function signatures are.

It would be useful for:

Category Structure

I think there is a need for a way that humans can absorb the complex interrelationship of these structures. Axiom already has diagrams like this It would be good (and I hope useful) to try to extend this to incorporate the axiom information.

In order to explore the possibilities I am starting by using a simple graphical editor (Inkscape) which makes it easier to try out various layouts. The downside, compared to automated methods, is that it it time consuming to maintain and errors can, probably already have, get in.

The first problem is to find the right level of detail. For me, just including the category and domain names does not give enough information to human users about what domains they should use. However too much information makes the diagram cluttered and unusable. I think it will take some experimenting to get the balance right.

Here is a very small sub-diagram (based on catdef.spad.pamphlet) to experiment with layouts and level-of-detail issues:

Here are the operator categories:

operations

Here are the categories that the operators will be used in.

ops part 2
ops5
ops4
ops6
ops3

Key

The above diagram is PNG for maximum web browser compatibility but the master is in SVG format here.

I don't know what to do about categories (such as AbelianGroup) that have not been converted yet? Including all function signatures would make the diagram far too big and cluttered but I would like to have function signatures for functions related to axioms. I am concerned that having some function signatures, and not others, could be a source of confusion.

Questions

Here are some unanswered questions that I put on the OpenAxiom forum:

As I understand it, in the existing 'catdef.spad.pamphlet': Categories that inherit from SemiGroup use '*' as the main operation *: (%,%) -> %

Categories that inherit from AbelianSemiGroup use '+' as the main operation +: (%,%) -> %

So we can get ring and field-like categories by inheriting from both?

So the commutative axiom is bound up with function names and inheritance details when it might be more flexible if they were independent concepts.

The code in the Yue Li sandbox works differently from this in that it uses a generalised mapping op: Mapping(T, T, T) which can be mixed and matched in a more general way.

I get the impression that the new 'assume' syntax is intended to allow this more generalised approach to be applied to the categories in 'catdef.spad.pamphlet'. I get the impression that each of these mappings would have a category and a domain like this:

So my questions are:

I Have drawn a diagram (by hand) of all the existing categories in catdef.spad.pamphlet above .

This is just a start, it really needs to be optimised to clarify these issues. Perhaps if I understood the answers to the above questions better I might be able to change it to reflect the proposed new structure?

Formal Methods

Once axioms are more generally included in Axiom then, I think this adds greater potential for interworking with formal methods tools. I therefore think it makes sense to include that topic here. There are many types of such tools available, such as:

quote from wiki page:

"In the property-oriented approach to specification (taken e.g. by CASL), specifications of programs consist mainly of logical axioms, usually in a logical system in which equality has a prominent role, describing the properties that the functions are required to satisfy - often just by their interrelationship. This is in contrast to so-called model-oriented specification in frameworks like VDM and Z, which consist of a simple realization of the required behaviour."

So:

(or by Curry–Howard: proofs)

I have not yet seen a program that is good at both.

Gabriel Dos Reis is working on integration between OpenAxiom and Isabelle. "The first batch of work led to initial code generators targeting PolyML (one of the primary ML implementation used for Isabelle). Yue was also involved in that effort. David Mattews (the main guy behind PolyML) has been very helpful. More remains to be done."

See also "Calculemus project"

Tool Logic Support Configuration Input Comments
ACL2 first order prover state machine defined in LISP

the leader in that field

does term rewriting and proofs.

Isabelle higher order prover axioms  
HOl, Coq higher order prover   based on lambda calculus encoding

I am planning to experiment with CASL and Isabelle. On this page: I looked the relation between FriCAS and 'CASL' (an example of an Algebraic Specification Language) and 'Isabelle' (an example of a Proof Assistant). In particular I looked at how all of these programs code a randomly chosen example - AbelianMonoid. If all these programs were modified slightly to work from a common AbelianMonoid definition then we would get a much richer meta representation.


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Axiom Volume 1: Tutorial. Documentation is freely availible from: http://www.axiom-developer.org/axiom-website/documentation.html

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.