[Top][All Lists]

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

Re: [Axiom-developer] Computational Mathematics, proofs, and correctness

From: Martin Baker
Subject: Re: [Axiom-developer] Computational Mathematics, proofs, and correctness
Date: Mon, 26 May 2014 15:28:12 +0100
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.5.0


Yes, I think it would be really good if Axiom could live up to its name and include axioms.

It seems to me that categories in Axiom are mostly about function signatures (I know I'm vastly oversimplifying here) but they would be more like the mathematical concepts they represent if they included axioms?

Are you talking about two different types of capability here:
* Proof Assistants like 'Coq' or 'Isabelle'.
* Algebraic Specification Languages like 'CASL'.
Does ACL2 fit into this distinction?

So I'm thinking that proof assistance are based on rules and driven by human input and algebraic Specification Languages are based on axioms and provide some level of automatic checking, although I guess there is some overlap?

I get the impression that Axiomatic systems are problematic in that a single error allows you to prove anything (true=false) and, as you have pointed out to me, rule based systems are difficult to debug.

Even so, I think that the addition of axioms into categories would be a big benefit, even it it was only initially used for human readers and some automated checking.

The choice of what rules to call axioms may be arbitrary but there are all sorts of choices that have to be made when supporting an algebra, like notation and which algorithm to use, which don't follow automatically from the mathematics.

What would it mean to prove Axiom correct?

I get the impression that, at some level a computer program is only an approximation to mathematics (float approximates to reals and so on). Issues with proving code(algorithms) - 'halting problem'. Despite these limits to a complete proof of the whole program, there is a lot that can be done at a higher level if axioms were included in the program.

So I think this sort of capability would be really good, I'm just too impatient to wait 30 years.


reply via email to

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