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