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 = such 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 <[email protected]>
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
>
_______________________________________________
Axiom-developer mailing list
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
