axiom-developer
[Top][All Lists]
Advanced

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

## Re: [Axiom-developer] [Proving Axiom Correct] Bootstrapping a library

 From: Tim Daly Subject: Re: [Axiom-developer] [Proving Axiom Correct] Bootstrapping a library Date: Tue, 14 Feb 2017 23:24:18 -0500

Renaud,

I've been looking at FoCal and, in particular, the Zenon program
http://zenon.inria.fr/zenlpar07.pdf

Zenon appears to be able to output OCAML code from proofs.
In your opinion is it reasonable to consider modifying the back end
to output Spad code?

Tim

On Fri, Feb 10, 2017 at 8:39 AM, Tim Daly wrote:
Renaud,

I'm just getting around to the FoCal information. Obviously you've done a lot of
work on this subject already. I have the papers and the reference manual near
the top of the reading stack. I'm certain to have questions.

Yes, BasicType requires properties for = "" as symmetry which would have
to be proven at the Domain level for each implementation. Of course, = is not
actually implemented directly in NNI but somewhere up the inheritance chain.
For example, the domain ANY has

x = y ==
(x.dm = y.dm) and EQUAL(x.ob, y.ob)\$Lisp

where dm is a field in the Record implementation of ANY

Rep := Record(dm: SExpression, ob: None)

which depends on the Lisp definition of EQUAL and SExpression
is one of String, Symbol, Integer, DoubleFloat, OutputForm

Whereas the domain IndexedList implements

x = y ==
Qeq(x,y) => true
while not Qnull x and not Qnull y repeat
Qfirst x ^=\$S Qfirst y => return fase
x := Qrest x
y := Qrest y
Qnull x and Qnull y

where
Qeq   ==> EQ\$Lisp
Qnull ==> NULL\$Lisp
Qfirst ==> QCAR\$Lisp
Qrest ==> QCDR\$Lisp
and
S : Type
is a dependent argument type. Sigh.

The proofs of = in each domain will involve an appeal to the Lisp
definition of a small number of functions. I'm using ACL2 for Lisp.

This is where the ACL2 and Coq proofs meet.

There is no such thing as a simple job.

Tim

On Fri, Feb 10, 2017 at 5:13 AM, Renaud Rioboo wrote:
Dear Axiom gurus,

Axiom's NNI inherits from a dozen Category objects, one of which
is BasicType which contains two signatures:

?=?: (%,%) -> Boolean       ?~=?: (%,%) -> Boolean

In the ideal case we would decorate BasicType with the existing
definitions of = and ~= so we could create a new library structure
for the logic system. So BasicType would contain

theorem = (a, b : Type) : Boolean := .....
theorem ~= (a, b : Type) : Boolean := ....

Since BasicType is not an implementation you need to write a specification for equal and different. These specifictions should be inherited and proved at the domain level. You can see the standard library of FoCaLiZe for details.

In practice you need a language for writing logical statements and a language to prove these statements. Again see the FoCaLiZe library (for instance lattices) to see how a statement can be used in a proof.

Unfortunately it appears the Coq and Lean will not take kindly to
removing the existing libraries and replacing them with a new version
that only contains a limited number of theorems. I'm not yet sure about
FoCaL but I suspect it has the same bootstrap problem.

Inheritance is managed by the FoCaLiZe compiler together with dependencies which enables to have statements and proofs in a coherent way.

--
Renaud Rioboo

reply via email to

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