Progress in happening on the new Sane Axiom compiler.
Recently I've been musing about methods to insert axioms
into categories so they could be inherited like signatures.
At the moment I've been thinking about adding axioms in
the same way that signatures are written, adding them to
the appropriate categories.
But this is an interesting design question.
Axiom already has a mechanism for inheriting signatures
from categories. That is, we can bet a plus signature from,
say, the Integer category.
Suppose we follow the same pattern. Currently Axiom
inherits certain so-called "attributes", such as ApproximateAttribute,
which implies that the results are only approximate.
We could adapt the same mechnaism to inherit the Transitive
property by defining it in its own category. In fact, if we
follow Carette and Farmer's "tiny theories" architecture,
where each property has its own inheritable category,
we can "mix and match" the axioms at will.
An "axiom" category would also export a function. This function
would essentially be a "tactic" used in a proof. It would modify
the proof step by applying the function to the step.
Theorems would have the same structure.
This allows theorems to be constructed at run time (since
Axiom supports "First Class Dynamic Types".
In addition, this design can be "pushed down" into the Spad
language so that Spad statements (e.g. assignment) had
proof-related properties. A range such as [1..10] would
provide explicit bounds in a proof "by language definition".
Defining the logical properties of language statements in
this way would make it easier to construct proofs since the
invariants would be partially constructed already.
This design merges the computer algebra inheritance
structure with the proof of algorithms structure, all under
the same mechanism.
Tim