Re: Proving Axiom Correct, "state of the art" report
On 31/03/17 05:34, Tim Daly wrote:
> Consider the Axiom Domain NonNegativeInteger. NNI roughly
> corresponds to the Type theory "Nat" construction. They differ
> in that Axiom uses Lisp Integers whereas Type theory uses
> Peano arithmetic (a zero and a successor function) but for
> our purposes this does not matter at the moment.
Perhaps there are issues around this that will matter? Given that there
are two formulations of each algebra, one like this:
zero: () -> $
succ: ($) -> $
and one like this:
+ ($,$) -> $
If one form is needed for inductive proofs and the other form for
applied mathematics. Could Axiom hold both forms in a single
category/domain and switch between them as needed?