[Top][All Lists]

[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


I've been looking at FoCal and, in particular, the Zenon program

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?


On Fri, Feb 10, 2017 at 8:39 AM, Tim Daly <address@hidden> wrote:

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 ==
    ( = 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

  Qeq   ==> EQ$Lisp
  Qnull ==> NULL$Lisp
  Qfirst ==> QCAR$Lisp
  Qrest ==> QCDR$Lisp
  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.


On Fri, Feb 10, 2017 at 5:13 AM, Renaud Rioboo <address@hidden> 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]