[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: Fri, 10 Feb 2017 08:39:59 -0500


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]