Information Technology Reference

In-Depth Information

800 lines of Isabelle code were needed to both specify the required structures

and implement the proofs, and a readable proof was obtained.

We would like to point out the following about this approach:

1. A higher degree of accuracy (in comparison to the previous approach) has

been obtained; now the relationship between the objects implemented in the

proof assistant and the mathematical concepts present in the proof is much

clearer.

2. The representation of algebraic structures in Isabelle and Kenzo is performed

in the same way, using records where each field represents an operator. On

the other hand, homomorphisms have a simpler representation in Isabelle

since they are just elements of a functional type whereas in Kenzo they are

also records, allowing that way to keep explicit information over their domain

and codomain.

3. Converting homomorphisms into total functions by the use of “arbitrary”

makes things a bit more complex. From the formal point of view, it is dif-

ficult to identify a homomorphism containing an arbitrary element, i.e., a

conditional statement “if
x

G
then
fx
else arbitrary”, with any mathemat-

ical object; there is a gap in the abstraction process that cannot be directly

filled. A solution to clarify this process by identifying the elements outside

the domain with a special element of the homomorphism's codomain will be

proposed in Section 5; with this idea are avoided the non defined values of

the total function representing a concrete homomorphism. This solution has

been proposed before and its disadvantages are well known, but making a

careful use of it can make mechanization easier.

4. Homomorphisms are represented by conditional statements, and working

with
n
homomorphisms at the same time one has to consider 2
n
cases. There

are two solutions to this problem. The first one consists in enhancing the

homomorphisms with an algebraic structure allowing to reason with them

like elements of this structure in an equational way (for instance, an abelian

group or a ring). With this implementation, proofs can sometimes avoid to

get into the concrete details of the representation of homomorphisms in the

theorem prover. To some extent this can be understood as the development

of a new level of abstraction; some steps (or computations) are developed at

the level of the elements of the homomorphisms domains whereas some are

developed at the level of the structure where homomorphisms are embedded.

This forces to implement proof steps more carefully and also to make a

correct choice of the homomorphisms that can be provided with an algebraic

structure, and will be discussed in Section 5. A second possible solution not

implemented yet using equivalence classes will be mentioned as future work

in Section 7.

∈

5

A Homomorphism Approach

If we capitalize the advantages of both the symbolic approach and the set the-

oretic approach and we combine them carefully, it is possible to obtain a new

Search WWH ::

Custom Search