Re: [Axiom-developer] Call for help

[daly]

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.
That way COQ would have access to the Axiom signature database
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