Re: [Axiom-developer] Why proving Axiom correct is important

[daly]

Martin,

>If you are using COQ then why not just map the COQ library entries into 
>the Axiom categories?
>So if we take part of the base library here:
>https://coq.inria.fr/library/Coq.Arith.Mult.html#

>So the appropriate Axiom category could have an entry like:

>Zero property
>Lemma mult_0_r : forall n, n * 0 = 0.
>Lemma mult_0_l : forall n, 0 * n = 0.

I will look into this. Thanks for the pointer.




>Of course the COQ libraries have a different structure than the Axiom 
>libraries so there is no exact mapping between them but it would seem to 
>be a good idea to have as much compatibility as possible rather than 
>invent something from scratch?

There are no plans to invent anything from scratch. This is research,
which implies understanding and using what exists before pushing a
boundary. The bibliography volume has references on the subject but
these need to be organized, maybe into a survey paper.




>Looking at these they are not 'axioms' in that they have redundancy.

>For example there is also the following
>Commutativity
>Lemma mult_comm : forall n m, n * m = m * n.

>So mult_0_l could have been derived from mult_0_r.

>Do you propose to have a minimal set of axioms or to have a larger set 
>of lemmas?

There is no need for a minimal set. Special cases like 0 arise all
the time so it is just as easy to check for a few special cases.
Knowing that n=0 can cause a lot of simplification early in the process
which can only be a good thing.




>The form you have used in 10.2 is like this (in the human readable LP 
>part - not part of the category itself):
>Axioms:
>associative("*":(%,%)->%)    (x*y)*z = x*(y*z)
>Conditional attributes:
>commutative("*":(%,%)->%)    x*y = y*x

>Are you proposing to put this into the category itself, not just as a 
>comment? Do you prefer this syntax over the COQ syntax?

The effort at this point is collecting the information to decorate the
algebra and lisp code. There are no particular syntax requirements at
the moment because all of my reference material is from books.

You raised the interesting question of COQ vs Isabelle vs books.
It might make sense to introduce an "Axioms" category to collect
operations that make sense. In fact, there is no reason why, with
careful thought, there might be operations on the same internal
structures which present the COQ or Isabell or book form output

  )abbrev category AXIOMS Axioms
   ...
  COQ: () -> List(COQ-axioms)
  Isabell: () -> List(Isabelle rules)
  Book: () -> List(traditional book axioms)

This has the advantage that a domain can inherit the axioms which
would make it easy to see when things disagree or are incomplete.




>Isabelle uses a different approach again (in the flavor of Isabelle I 
>have seen so far) in that it uses 'rules' instead of 'axioms'

>So instead of:
>n * 0 = 0

>We have separate rules for each direction:
>n * 0 ==> 0
>0 ==> n * 0

>So the first direction can be declared as a simplification rule and can 
>be applied without any danger of an infinite loop.

>The advantage that I could see, for this in Axiom, is that the 
>simplification that is applied to equations in the output formatter 
>could be made explicit, configurable and provable.

>Do you have a view on axioms vs. lemmas vs rules?

There is no way to decide this at the moment. Rules seems to be more
"actionable" for writing code but lemmas seem to be more "composable".
Axiom tends toward the actionable so Isabelle's approach might make
more sense. COQ seems closer to Axiom in design.




>Are you proposing to put this into SPAD itself rather than comments or LP?

This is the design phase of the problem, collecting information.
At the moment it is just dead text being added to the files. However
the idea is to make it useful for two levels. At one level the proof
mechanism should be able to use the assumptions in a proof. At another
level Axiom should make the assumptions available to the algorithms
and the end user. So, to answer your question, this will be SPAD level
code rather than just comments.

SPAD is really just a domain-specific language layered on top of Lisp.
The lisp code is also being decorated with type information. There 
needs to be some careful thought to ensure that the two sources of
information are synergistic.

So there needs to be some thought given to encoding the assumptions
to fulfill these goals. Suggestions are welcome.

Tim