Information Technology Reference
In-Depth Information
framework where the level of abstraction is as suitable as in the set theoretic ap-
proach and the degree of mechanization is as high as in the symbolic approach.
The idea is to develop a structure where the domain of the homomorphisms
and also the homomorphisms can be found at the same time, with homomor-
phisms represented by elements of functional type (or something similar), which
would allow working with them at a concrete level, but with the same homomor-
phisms being part of an algebraic structure. Since various algebraic structures
are involved in the problem (at least (
D
,d
D
∗
)and(ker
p, d
D
∗
)), there is not a
simple algebraic structure containing all the homomorphisms appearing in the
problem. Clearly endomorphisms of (
D
∗
,d
D
∗
) form a ring, and also the ones in
(ker
p, d
D∗
), as well as the homomorphisms from (
D
∗
,d
D∗
)into(ker
p, d
D∗
)form
an abelian group; the automation of proofs in such a complicated environment
would be hard; some ideas will be proposed in Section 7.
Another possible solution is explained in this section. It involves consider-
ing just one simple algebraic structure where all the homomorphisms can be
embedded, and then develop tools allowing to convert a homomorphism from
this structure into one of the underlying ones. Taking into account that ker
p
is a substructure of
D
∗
, we will consider as our only structure the ring of en-
domorphisms
R
=hom(
D
∗
). Later we will introduce the tools
allowing to convert homomorphisms from
R
into homomorphisms, for instance,
of hom(ker
p, d
D
∗
)(ker
p, d
D
∗
), but just to illustrate the benefits of this approach
we give a brief example here:
,d
D
∗
)(
D
,d
D
∗
∗
∗
Example 1.
Proving the fact “assumes
d
∈
hom(
D
,d
D
∗
)(
D
,d
D
∗
)and
h
∈
∗
∗
hom(
D
,d
D
∗
)”, due to
partiality matters, requires several reasoning steps. When providing homomor-
phisms with an algebraic structure this is a trivial proof, since rings are closed
under their operations.
,d
D
∗
)(
D
,d
D
∗
)shows
p
=
dh
+
hd
∈
hom(
D
,d
D
∗
)(
D
∗
∗
∗
∗
In order to embed homomorphisms into a ring, it is necessary to choose carefully
the elements and also the operators. Firstly, there can be only one represen-
tant for each homomorphism, and here partiality appears again, since otherwise
both
λx.
(one
G
)and
λx.
(if
x
G
then one
G
else
arbitrary
) could be iden-
tities in this ring. Secondly, operators must be closed over the structure, and
thus they rely strongly on the chosen representation for homomorphisms. With-
out going in further depth, we decided to consider the carrier of the ring R
formed by the completions
λx.
(if
x
∈
∈
G
then
fx
else one
G
), because then the
generic composition operator
can be used in Isabelle (whereas this was not
possible with the
extensional functions
based on “arbitrary” in Isabelle). At a
second stage, we had to implement the tools allowing to convert an element
of hom(
D
◦
,d
D
∗
) into one of, for instance, hom(ker
p, d
D
∗
)(ker
p, d
D
∗
)
(under precise conditions). This would allow to implement proofs for facts such
as
,d
D
∗
)(
D
∗
∗
(property (3) in Def. 2, needed for
Lemma 2) in a human readable style such as
4
:
id
−
p, D,
ker
p
◦
h, D, D
=
0
,D,
ker
p
4
The
···
are just an abbreviation meaning “the previous expression” in sequential
calculations.
Search WWH ::
Custom Search