Information Technology Reference
In-Depth Information
prover Isabelle [12] has been chosen, mainly, because it is the system the authors
are most familiar with.
A first algorithm for which we intend to implement a proof is the Basic Per-
turbation Lemma (hereinafter, BPL), since its proof has an algorithm associated
used in Kenzo as one of the central parts of the program. In Section 2, the state-
ment of the BPL, as well as a collection of lemmas leading to its proof, will be
given. In Section 3, a na ıve attempt to implement the proofs of these lemmas is
introduced. Section 4 describes an approach using the existing tools in Isabelle.
In Section 5, we try to avoid the problems arising from partiality and provide a
generic algebraic structure embedding most of the objects appearing in the prob-
lem. In Section 6, an approach based on a new Isabelle feature, instantiation of
locales, will be commented on. The paper ends with a conclusions section.
2
Some Homological Algebra
In the following definitions, some notions of homological algebra are briefly in-
troduced (for further details, see [10], for instance).
Definition 1. A graded group C
is a family of abelian groups indexed by the
integers, C
=
{
C n } n∈ Z ,witheach C n an abelian group. A graded group homo-
morphism f : A
B
of degree k (
Z
) between two graded groups A
and
B
is a family of group homomorphisms, f =
{
f n } n∈ Z ,with f n : A n
B n + k
a
group homomorphism
n
Z
.A chain complex is a pair ( C
,d C
) ,where C
is
a graded group, and d C
(the differential map) is a graded group homomorphism
d C
: C
C
of degree -1 such that d C
d C
=0 hom D D
.A chain complex ho-
momorphism between two chain complexes ( A
,d A
) and ( B
,d B
) is a graded
group homomorphism f : A
(degree 0) such that fd A = d B f .
Let us note that the same family of homomorphisms f =
B
f n } n∈ Z can be con-
sidered as a graded group homomorphism or a chain complex homomorphism. If
no confusion arises, C
{
will represent both a graded group and a chain complex;
in the case of a chain complex homomorphism, the differential associated to C
will be denoted by d C
.
Definition 2. A reduction D
between two chain complexes is a triple
( f, g, h ) where: (a) the components f and g are chain complex homomorphisms
f : D
C
C
and g : C
D
; (b) the component h is a homotopy operator on
D
, that is, a graded group homomorphism h : D
D
of degree 1; (c) the
following relations are satisfied: (1) fg =id C
;(2) gf + d D
h + hd D
=id D
;
(3) fh =0 hom D C
;(4) hg =0 hom C D
;(5) hh =0 hom D D
.
Reductions are relevant since the homology of chain complexes is preserved by
them and they allow to pass from a chain complex where the homology is un-
known to a new one where homology is computable.
Definition 3. Let D
be a chain complex; a perturbation of the differential d D
is a homomorphism of graded groups δ D
: D
D
(degree -1) such that d D
+
Search WWH ::




Custom Search