axiom-developer
[Top][All Lists]

Re: [Axiom-developer] Call for help

 From: daly Subject: Re: [Axiom-developer] Call for help Date: Sun, 26 Jul 2015 14:27:22 -0500

```Martin,

I like the idea of "specific mathematical axiom markup" as a first
cut.  I will try this idea.

This is (reasonably) easy to do as there are already some markers
in place. These are the "attributes" such as LeftUnitary.
Unfortunately most of them are somewhat more advanced, such as
FiniteAggregate, which requires the use of dependent types.
That's still a steep hill to climb.

Axiom has signatures already. The real hack would be to unify
the signatures used by COQ with the signatures used by Axiom.
and Axiom would be able to use COQ to prove Spad code. This
would be the very essence of elegance.

Right now in Axiom you can say
)d op pop!
and it will show you signatures and examples from domains.
Perhaps we can develop a "rewriter" that will translate the
Axiom signature to a COQ signature.

==========================================================
)d op pop!

There are 4 exposed functions called pop! :
[1] ArrayStack(D1) -> D1 from ArrayStack(D1) if D1 has SETCAT
[2] Dequeue(D1) -> D1 from Dequeue(D1) if D1 has SETCAT
[3] D -> D1 from D if D has SKAGG(D1) and D1 has TYPE
[4] Stack(D1) -> D1 from Stack(D1) if D1 has SETCAT

Examples of pop! from ArrayStack

a:ArrayStack INT:= arrayStack [1,2,3,4,5]
pop! a
a

Examples of pop! from Dequeue

a:Dequeue INT:= dequeue [1,2,3,4,5]
pop! a
a

Examples of pop! from StackAggregate

a:Stack INT:= stack [1,2,3,4,5]
pop! a
a

Examples of pop! from Stack

a:Stack INT:= stack [1,2,3,4,5]
pop! a
a
=============================================================

There really ought to be a way to show the mathematical axioms,
possibly as part of the output of the )show command.

Tim

```