Mathematics Software Projects

There are many software projects which allow us to model mathematics such as:

• Computer Algebra Systems (CAS)
• Algebraic Specification Language (ASL) systems
• Proof Assistants

These types of programs have different purposes but they also have many similarities, I have discussed an example of each of these types of program below:

Each of these programs uses its own computer language to code information about mathematical structures. I think this makes sense since no program can represent all of mathematics, it is effectively infinite, so we cant include all mathematical sructures with the program. All we can do is to provide some common structures and then let users add their own structures using a language designed for this.

Lets look at how these programs represent mathematical structures using their own languages.

FriCAS (an example of a CAS)

FriCAS is an example of a computer algebra system (CAS) . FriCAS is a fork of the Axiom project, more about FriCAS here. FriCAS allows mathematical structures to be specified in a language called SPAD like this:

 ```)abbrev category ABELMON AbelianMonoid ++ Author: ++ Date Created: ++ Date Last Updated: ++ Basic Functions: ++ Related Constructors: ++ Also See: ++ AMS Classifications: ++ Keywords: ++ References: ++ Description: ++ The class of multiplicative monoids, i.e. semigroups with an ++ additive identity element. ++ ++ Axioms: ++ \spad{leftIdentity("+":(%,%)->%,0)}\tab{30}\spad{ 0+x=x } ++ \spad{rightIdentity("+":(%,%)->%,0)}\tab{30}\spad{ x+0=x } -- following domain must be compiled with subsumption disabled -- define SourceLevelSubset to be EQUAL AbelianMonoid() : Category == AbelianSemiGroup with --operations 0 : constant -> % ++ 0 is the additive identity element. sample : constant -> % ++ sample yields a value of type % zero? : % -> Boolean ++ zero?(x) tests if x is equal to 0. "*": (NonNegativeInteger,%) -> % ++ n * x is left-multiplication by a non negative integer add import RepeatedDoubling(%) zero? x == x = 0 n : PositiveInteger * x : % == (n::NonNegativeInteger) * x sample() == 0 if not (% has Ring) then n : NonNegativeInteger * x : % == zero? n => 0 double(qcoerce(n)@PositiveInteger, x) @```

The above code is specifying a 'category' this is effectively a set of function signatures like an 'interface' in other languages. We can then implement instances of that, called 'domains', which effectively implement algorithms to construct instances. In these respects FriCAS is very similar to mainstream computer languages, however FriCAS has many powerful capabilities that mainstream languages don't (discussed on these pages). The point I would like to make here is that the axioms for this structure are given in comments only and can't be used to influence instances of this structure or even to check code.

CASL (an example of an Algebraic Specification Language)

CASL is an algebraic specification language, its purpose is completely different to FriCAS, it is used as a means to specify more general computer programs. There is some information about CASL in its reference manual and its libraries in section 'v'. However, like FriCAS it does have its own language (and library of code) that can be used to specify mathematical structures.

 ```spec Monoid = sort Elem ops e: Elem; __ * __: Elem * Elem -> Elem, assoc, unit e end spec CommutativeMonoid = Monoid then op __ * __: Elem * Elem -> Elem, comm end spec Group = Monoid then forall x: Elem . exists x': Elem . x' * x = e %(inv_Group)% end spec AbelianGroup = Group and CommutativeMonoid end spec Ring = AbelianGroup with sort Elem, ops __ * __ |-> __ + __, e |-> 0 and Monoid with ops e, __*__ then forall x,y,z:Elem . (x + y) * z = (x * z) + (y * z) %(distr1_Ring)% . z * ( x + y ) = (z * x) + (z * y) %(distr2_Ring)% end view AbelianGroup_in_Ring_add: AbelianGroup to Ring = ops e |-> 0, __ * __ |-> __ + __ end```

The interesting thing for me, about this language, is that it encodes both the function signatures and the axioms. Common axioms are represented by 'assoc', 'unit e' and 'comm' but any other axiom can be specified by using equations and quantifiers.

Isabelle (an example of a Proof Assistant)

Again, Isabelle has a completely different purpose and again it has its own language (and library of code). Isabelle is a proof assistant (I have put more about Isabelle on this page). Isabelle language is two level allowing different types of logic to be used (the main one, used here, is higher order logic (HOL)), the inner language is enclosed in quotes:

 ```locale semigroup = fixes f :: "'a => 'a => 'a" (infixl "*" 70) assumes assoc [ac_simps]: "a * b * c = a * (b * c)" locale abel_semigroup = semigroup + assumes commute [ac_simps]: "a * b = b * a" begin lemma left_commute [ac_simps]: "b * (a * c) = a * (b * c)" proof - have "(b * a) * c = (a * b) * c" by (simp only: commute) then show ?thesis by (simp only: assoc) qed end locale monoid = semigroup + fixes z :: 'a ("1") assumes left_neutral [simp]: "1 * a = a" assumes right_neutral [simp]: "a * 1 = a" locale comm_monoid = abel_semigroup + fixes z :: 'a ("1") assumes comm_neutral: "a * 1 = a" sublocale comm_monoid < monoid proof qed (simp_all add: commute comm_neutral)```

Again this language has function signatures (curryed like this "'a => 'a => 'a" Isabell is based on ML and sometimes requires ML code to be embedded into the Isabelle language).

Although Isabelle allows axioms to be specified, the specification of axioms using equations is dicouraged. In Isabelle an equals character '=' represents 'iff' (If and only if). Instead Isabelle uses a 'definitional approach' but not quite as arbitary computer code (algorithmns) such as is used in FriCAS code instead Isabelle encourages a more structured approac to building up definitions. These definitions then relate back to first principles.

Isabelle has a few built in datatypes and allows us to build up more complicated datatypes (including recursive definitions). The difference is Isabelle adds proofs to this, so recursive datatypes have the capability for inductive proofs.

The concepts of HOL come from an earlier language 'LCF' its key ideas are:

• Have a special abstract type 'thm' of theorms.
• Make the constructors of the abstract type the inference rules of the logical system.
• Implement the system in a strongly typed high level language.

The ML family of languages are all decended from LCF.

The reason that equational definition of axioms is discouraged is that an arbitrary axiom, such as: f(x) + 1 = f(x), could lead to contradictions. For instance, if it were combined with a cancellation law we could derive 1=0.

COQ

Another interesting theorem prover is COQ which is based on constructive logic rather than HOL. COQ supports dependant types.

Other Computer Algebra Programs

http://en.wikipedia.org/wiki/Comparison_of_computer_algebra_systems
Here are my own comments on some of them:

pro's

Covers a wide range of algebras, includes equation solvers.

con's

Steep learning curve, need to learn SPAD language, very poor error messages, no IDE environment, no direct access to class library.

Language

SPAD/Aldor - written in mixture of lisp and C.

con's

Non-standard open source licence.
Does not cover such a wide range of algebras as Axiom.

UACalc

http://www.uacalc.org/

Universal Algebra Calculator - a more specialised program just for universal algebra.

Java.

pro's

This is an internal DSL (Domain Specific Language) for Scala and so users have full access to Java environment.

con's

Only supports numeric programming.

Scala.

kiama

Includes a library for parsing lambda calculus, but not a general mathematics language program.

Scala

Java Algebra System

http://krum.rz.uni-mannheim.de/jas/

Language

Java and Java Python

Java.

Gap

discrete algebra
no longer supported

Macaulay2

http://www.math.uiuc.edu/Macaulay2/

Own Language

Maxima

http://maxima.sourceforge.net/

Lisp

Octave

http://www.gnu.org/software/octave/

numerical