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:

• FriCAS (an example of a CAS)
• CASL (an example of an Algebraic Specification Language)
• Isabelle (an example of a Proof Assistant)

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.

Axioms in Axiom

I have put further thoughs about representing axioms in a CAS like Axiom on this page.

Other Computer Algebra Programs

There is a wider list on this page:
http://en.wikipedia.org/wiki/Comparison_of_computer_algebra_systems
Here are my own comments on some of them:

EuclideanSpace

home