Four Approaches to Automated Reasoning with Differential Algebraic Structures - Artificial Intelligence and Symbolic Computation - page 234

functions in order to provide them with an enveloping algebraic structure. Our
choice was to introduce completions, identifying the elements outside the do-
main of the partial function with a distinguished element, the identity of the
image structures. Similarly, the extensional functions already available in Is-
abelle could have been used, just with some modifications in the composition
of functions. The result is that a generic algebraic structure can not be directly
defined from the homomorphisms since there are multiple functions representing
each of them. In particular, it was shown that inside this framework implemen-
tations could be given for all the properties in Lemma 2, and that from the
formal point of view, there was a clear abstraction function between the ob-
jects implemented in Isabelle and the mathematical objects required. Finally, in
Section 6, the possibilities of a recent Isabelle feature (instantiation of locales)
were studied; this new tool fits with several problems and so far would allow to
implement all the proofs of the lemmas in Section 2. We have implemented a
proof of all the properties in Lemma 2. From this study, we conclude that the
approach based on the instantiation of locales is the most promising for further
developments in homological algebra.
Some problems remain open, and more work has yet to be done:
1. To complete the proofs of all the lemmas in Section 2 and then give a com-
plete implementation of the proof of the BPL. The proof obtained should
satisfy all the requirements needed to extract a program from it. At this
point, we could explore the possibilities of extracting code in Isabelle (see,
for instance, [2]). In addition to this, a comparison will be needed with other
provers where code extraction has been used in non trivial cases (see, for
instance, the work on Buchberger's algorithm in Coq [17]).
2. As it has been explained in Section 4, partial functions can be implemented
by using equivalence classes. Actually, the solutions proposed here (using
completion functions or the extensional functions implemented in Isabelle)
are just different ways of giving elements to represent these (non-implemen-
ted) equivalence classes. The implementation would force to redefine all the
concepts regarding homomorphisms (composition, identities,...) but would
produce a definitive way to deal with partial functions in the Isabelle/HOL
system. Following the instructions given in [13], the definition should be
quite feasible.
3. A ringoid (see [10]) is an algebraic structure containing homomorphisms and
endomorphisms over different algebraic structures. To give an implementa-
tion of it could be useful for several problems in group theory. An attempt
to introduce category theory in Isabelle has been already made (see [6]), and
some similarities can be found between the implementation of morphisms
given there and the representation of homomorphisms that we proposed in
Section 5, needed to work in a more effective way with them. Specification
of ringoids is not a complicated task in Isabelle. Nevertheless, the benefits
and drawbacks of this new approach with respect to our third and fourth
approaches should be carefully studied.