[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Proving Axiom Correct, "state of the art" report

From: Martin Baker
Subject: Re: [Axiom-developer] Proving Axiom Correct, "state of the art" report
Date: Fri, 31 Mar 2017 11:51:20 +0100
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0

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?


reply via email to

[Prev in Thread] Current Thread [Next in Thread]