Re: Axiom musings...

Tim,

Would this also be compatible with 'propositions as types' as in Idris 
and various proof assistants? That is, could you have both Curry–Howard 
and Carette-Farmer?

I ask this because types (and constructors for types) could also be 
inherited by categories in the way you describe. So an equation (axiom 
or identity) like a=a+0 has a constructor, Refl, if true which can be 
inherited.

Or do you see computer algebra/deduction/proof programs forking into 
constructive or axiomatic approaches?

Martin

On 16/12/2019 00:52, Tim Daly wrote:
> 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