Mathematics to compute 

Get Complete Project Material File(s) Now! »

Bishopian toolkit

In term of our type theory, a set A would be defined as:
El A : Type
=A : El A El A Ω
_ : Equivalence ( =A )
More often than not we shall use A instead of El A and omit the index of the equality when it is clear from context.
Let us dwell on this definition for a moment. Given a relation R on a set A, it is fairly straightforward how to build the quotient A R: it amounts to replacing =A with R. This is an important feature programming-wise: there is no need to change the representation of the data to change which data are equal. For instance, if one is interested in considering lists up to reordering of their elements (a.k.a. multisets), they can be just a lists. Considered up to reordering of their elements. This is essentially, by the way, what is done when Haskell’s list monad is used as a non-determinism monad.
In ZF, on the other hand, as equality cannot change, it is always the representation of data which much change to conform to it. In the case of quotienting, equivalence classes might look like a particularly odd encoding to a programmer.
On a side note, programmers are often particularly wary of what cannot be embedded in their programming languages. In particular, they usually try to avoid relying on equalities which are not decidable. Many even loathe equalities which are not the structural equality. These are limitations which will not apply to us. Though having a decidable – or structural – equality of course has benefits in many situations. This new found liberty might be a strong argument in favour of any system which can cope with general sets in this sense.
In the community of dependent type theories, sets in the sense of Bishop are often known as setoids. They also appear in other guises in some areas of mathematics. They can be seen as Ω-enriched groupoids, and, equivalently, as 0-groupoids. To categorically minded people, they may also remind the topos theoretic presentation of set theory.
Functions from set A to set B are supposed to be maps from A to B. But, much for the same reasons that all functions from A to B cannot necessarily be lifted to be functions from a quotient of A to B, not all maps are eligible to be functions. Only those maps which respect equality are:
Function A B
f : A B
_ : ∀a1=Aa2. f a1 =B f a2
We will usually use functions as their inner map.
Functions are exactly why a structural equality is desirable: if the equality on A is structural (more generally, if it coincides with Leibniz equality), all maps can be trivially lifted as functions, otherwise the programmer bears the burden of proof. Again, this lifting issue is not an unknown problem to mathematicians, not only in the case of quotients but also in the case of algebraic structures, where the appropriate morphisms are those which respects the structure. A customary move when playing with morphisms is to move to a categorical abstraction in which everything is, by construction, morphism. We shall do it for abelian groups, however, desirable though it is, we could not achieve it in a satisfactory way in the case of sets (see Chapter 5 for details).
It is time to define our first set construction, namely the set of functions from A B (written A −→ B). Its equality is the so-called extensional equality:
El (A −→ B) = Function A B
f = g = ∀a. f a = g a
The set A −→ B −→ C (to be read as A −→ (B −→ C)) will be used to encode functions from A and B to C. Equivalently, we could have chosen the set (A × B) −→ C – to be defined below – but the former is more customary in type theory.
A function f :A −→ B is said to be injective when ∀x y : A. f x = f y→x = y. A subset of B is defined as being any such injection, like subobjects in a category are defined to be any monomorphism.
Given a set A, a set of functions of particular interest is the set A −→ Ω of predicate over A, where Ω is considered up to equivalence:
El Ω = Ω
p = q = p ⇐⇒ q
A predicate P can be seen as a subset of A. To emphasise this point of view, we shall sometimes say part instead of predicate, and write x ε P for P x. Any part P defines a subset, called a strong subset:
{x : A | x ε P}
El {x : A | x ε P} = x ε P
x : A
(x, _) = (y, _) = x =A y
Given a function f :A −→ B, we can define its image IM f :B −→ Ω as b ε IM f =∃a:A. b = f a.
Cartesian product
Set also have a have a cartesian product:
A × B
El (A × B) = A × B
(a1, b1) = (a2, b2) = a1 = a2 ∧ b1 = b2
Set sum
And a sum, sometimes known as disjoint union whose carrier is the type theoretic A + B and the equality is:
( =A+B ):(A+B) (A+B) Ω
( =A+B ) ι1 a ι1 a′ = a = a′
( =A+B ) ι2 b ι2 b′ = b = b′
( =A+B ) _ _ = ⊥
Numbers & booleans
The sets N of natural numbers, Z of integers and B of booleans are lifted canonically to sets in the obvious way. For instance the equality on N can be computed as
( =N ):NNΩ
( =N ) 0 0 = ⊤
( =N ) 0 _ = ⊥
( =N ) _ 0 = ⊥
( =N ) n p = (n − 1)=N(p − 1)
From now on, we shall consider these three as sets.


Homological algebra, in particular effective homology, fit very well in a categorical framework. From a programming perspective, categories will play the role of abstraction barriers hiding the unnecessary details of, say, the definition of abelian groups to the algorithms computing homology groups.
Although Bishop does not give such a definition, there is a notion of category which follows naturally from his definition of sets and deserves to be called Bishop categories.
O : Type
Hom : O O Set
1A : Hom A A
; :Hom A B −→ Hom B C −→ Hom A C
_ : f ; (g; h) = (f ; g); h
_ : f ; 1 = 1; f = f
Notice the order of the composition: f ; g (often written simply f g) corre-sponds to the arguably more usual g ◦ f .
The sets (Hom A B) are called homsets, their elements are called eitherf morphisms or arrows. We usually write A −−−→ B instead of f :Hom A B. An important feature of these Bishop categories is that the type O of objects is not a set. Consequently, the question whether two objects are equal or not does not make sense: equality belongs to sets. This contrasts with the usual definition of category where there objects are ZF-sets (often there is even a set of all objects). ZF-sets can be compared. However, in many areas of category theory, it is bad practice to compare objects or even outright banned. Hence Bishop categories are arguably a better definition of categories than those based on ZF.
Additionally, as categories are not sets, there is no need to restrict the category of sets to some small set of a sort. There is a category of all sets and functions. This is supported by the type theory of Coq, where we define categories at a higher sort than sets (in a sense, categories are bigger than sets).
Monomorphism & epimorphism
In a category C, we say that an arrow A −−−→ B is a monomorphism if for any
g h
two X −−−→ A and X −−−→ A with gf = hf , then g = h. We also say that f
is a mono, for short, or that f is monic. We also call subobject of A a mono
s .
S −−−→ A
In the category of sets, the monomorphisms are the injective functions. In particular subsets coincide with subobjects.
Dually, an epimorphism is an arrow A −−−→ B such that for any two
g h
B −−−→ X and B −−−→ X with f g = f h, we have g = h. We also say that f is an epi, or that f is epic.
In the category of sets, the epimorphisms are the surjective functions.
While less obvious than for monos, it is not hard to prove.
Initial & terminal objects
An initial object 0 of a category C is such that for any object A of C, there is
a unique arrow 0 . There an initial object in the category of sets: the 0 −−−→ A
empty set.
It is easy to prove that surjective functions are epic. Conversely,
given an epimorphism A −−−→ B, let us consider two parts of B: ⊤ and IM f . By definition of IM f , f ; ⊤ = f ; IM f . Since f is epic, ⊤ = IM f , that is, f is sur-jective.
Dually, a terminal object 1 is such that for any object A, of C, there is a unique arrow ! . The one element set is terminal in the category of A−−→1 sets.
Phrases such as “there is only one such arrow” may benefit from a small clarification. They are to be understood relative to a given set, and mean, as in classical mathe-matics “for any two such arrows, they are equal”. What changes from classical maths, however, is that two equal element of a set do not necessarily share the same representation. Hence, when we name an element, we choose, im-plicitely, a particular representa-tion (presumably that which we believe will behave the best in programs).
Given two objects A and B in a category C, a product of A and B is an object
π1 π2
A × B together with two arrows A × B −−−→ A and A × B −−−→ B such that
f g ( f,g )
for arrows C −−−→ A and C −−−→ A, there is a unique arrow C −−−−−→ A × B
such that (f, g)π1 = f and (f, g)π2 = g.
f h g
A × B
π1 π2
This could be also stated as a product of A and B is a diagram composed π1 π2 of two arrows A × B −−−→ A and A × B −−−→ B which is universal. Universal definitions are common in the realm of categories. They feature an arrow such as (f, g) which has to be unique. The relevance of the uniqueness can be understood from the perspective of type theory as an extensional property. In the case of the product, the unicity of (f, g) is equivalent to the statement that for any x we have . This property is often called X −−−→ A × B (xπ1, xπ2) = x surjective pairing.
When a category C has a product A × B for every choice of A and B we say that C has all products. This terminology can be used with any suitable concept. We can also say that C has enough products when it does not necessarily have all products, but enough for the considered statement to make sense.
In particular the category of sets has all products: the cartesian products is a product in the categorical sense.
Dual to the product is the coproduct, also called sum. Namely, a coproduct of two objects and is an object together with two arrows ι1
A B A+B A −−−→ A+B
ι2 f g
and B −−−→ A + B such that for any arrows A −−−→ C and A −−−→ C, there is
a unique arrow A + B −−−−−→ C such that ι1; [f, g] = f and ι2; [f ; g] = g.
ι1 ι2
A + B
f h g
The category of sets has all coproducts, as the sum of two sets is a coprod-uct.
Equaliser & coequaliser
f g
Given two arrows A −−−→ B and A −−−→ B, an equaliser of f and g is an arrow E −−−→ A such that ef = eg. It needs to be a universal such arrow, that x x′ is for any X −−−→ A with xf = xg there is a unique arrow X −−−→ E such that x′e = x.
The category of sets has all equalisers: the equaliser of f and g is given by the strong subset E = {a : A | f a = g a} with e the canonical injection into A, and for an x as above, x′ is the lifting of x to E. Note that equalisers are necessarily monic.
Dually, there is a notion of coequaliser: given two arrows A −−−→ B and
g q
A −−−→ B, a coequaliser of f and g is an arrow B −−−→ Q such that f q = gq.
Moreover, for any x such that there is a unique arrow ′
B −−−→ X f x = gx x
such that qx′ = x.
The category of sets has all coequalisers. It is given as Q = B R with R the smallest relation such that for all a:A, f a = g a. The function q is the canonical projection onto Q and x′ is the lifting of x to be of domain B R. Again, coequalisers must be epimorphisms.
Let E e A be the equaliser of
f g
A −−−→ B and A −−−→ B. Let us y
consider two arrows Y −−−→ A
and Y z A with = . As
−−−→ ye ze yef = yeg there exist a unique arrow w such that we = ye. As both y and z qualify as such, they must be equal.

READ  Skill rating with hypernode graphs 


Principle of choice
If a function f :A −→ B is surjective (i.e. ∀b. ∃a. f a = b), the constructive interpretation gives a map g from B to A such that ∀b. f (g b) = b, however this has no reason to be a function.
Indeed, supposing that all surjection had a preinverse, then let P be an arbitrary proposition. Consider B the set of booleans, and S the set where the base type is the booleans and where the equality is defined as
e : B B Ω
e true false = P
e false true = P
e _ _ = ⊤
Now the function
The terminology preinverse is bor-rowed from a categorical intu-ition: g is a preinverse of f if g followed by f is the identity.
Dually, a postinverse is a function g such that f followed by g is the identity.
This is a variant of Diaconescu’s argument[20], which proves that the principle of choice is stronger than the excluded middle in topoi.
If f is injective, for any two equal
b1 and b2, g b1 = g b2 follows from f (g b1) = f (g b2). Hence g is a function.
f :B−→S
f true = true
f false = false
is surjective. However, a preinverse function g would decide the truth of P, as g true = g false implies ¬P and ¬g true = g false implie P (equality on booleans is decidable). This is contradictory with the fact that provability is not decidable. The statement that all surjective functions have a preinverse is the principle of choice. Let us phrase it in a catchy slogan: choice: surjections have a section. Phrased this way – rather than referring to families of inhabited sets, the principle of choice can be read as property of a category, provided we read epimorphisms instead of surjections. The principle of choice, hence, is not valid in the category of Bishop sets (surjective functions are indeed the epimorphisms of the category of sets).
Principle of unique choice
On the other hand, if f is also injective then g is indeed a function and actually an inverse of f .
This observation leads to the principle of unique choice. Functions which are both injective and surjective are called bijections. Hence we can state the the principle of unique choice as follows: unique choice: bijections have an inverse.
The principle of unique choice is, again, a property of a category (provided that “bijections” are replaced by “morphism which are both epic and monic”).
The aforementioned principle of unique choice can be a liability rather than an asset. Indeed, the fact that a bijective function is tractable does not mean it has a tractable inverse. Typical examples of this often come from cryptography. For instance, let us consider a group G of order n and g a generator of G. The function from Z nZ to G which maps p to gp is bijective. However, there is no known efficient algorithm for its inverse, called discrete logarithm. A number of cryptographic protocols actually rely on the hope that there will never be an efficient algorithm for discrete logarithm – the most famous being the Diffie-Hellman key exchange protocol.
If the principle of unique choice is valid in our category of sets, an inverse function can be devised automatically. As mentioned, every known proof of bijectivity of exponentiation leads to intractable discrete logarithms. As a matter of fact, all the computational content of the inverse found using the principle of unique choice is contained in the proof of bijectivity (more precisely in the underlying proof of surjectivity).
Concretely, we are left with two choices if we want to control the compu-tational complexity of our functions. Either we need to control the computa-tional complexity of the proofs we write, in particular, when writing proofs of bijectivity, we devise specific inverses. Or we make arrangements so that the principle of unique choice is not valid.
The former option precludes from using mostly any form of automation, as they produce proofs whose complexity cannot be known in advance. Also, it is fairly restrictive in what can be proved, or, in other words, proofs of surjectivity which cannot be used to find an inverse, can still be used for other purposes. Yet, we would be avoiding these. Therefore we shall choose the latter option: leaving aside the principle of unique choice.
As we have seen, the principle of unique choice is a direct consequence of the fact that given a proof of ∀a:A. ∃b:B. P a b, we can extract a map f :A B such that ∀a:A. P a (f a). This property can be seen a reflection on the constructive nature of the proof, or as an internal skolemisation. It is a natural principle of systems such as the Calculus of Inductive Constructions which is a foundation of Coq. Fortunately for our application, Coq has a sort Prop which explicitly does not enjoy this property.
Now, our mathematics is constructive. This means that anyone inspecting a proof of bijectivity can extract an inverse from it. The important point, though, is that this cannot be done inside the system.
This leads to a distinction between computational and static parts of proofs. The computational parts – programs – cannot reflect on the content of static parts: they are computationally irrelevant. This does not mean that computational parts do not use static ones at all. In fact, static proofs in programs can be used for three purposes:
Cutting branches: when some position in a program cannot be reached, it is sufficient to prove it, there is no need to provide computational code.
Termination: a proof can assert that a particular map never loops on any input.
Type coercion: when two types are provably identical, an element of the former can be used as one of the latter.
In this work we shall make use only of the first one of these usages. Indeed, in both other cases, as they are currently implemented in Coq, the computational content of the static proof is relevant. It would, hence, be unsuited for our goals. Not to mention that it is not really clear what it means for two types to be identical. All the maps defined here are structurally recursive, which makes them obviously terminating in the eyes of Coq.

Table of contents :

0 Introduction 
0.1 Effective homology
0.2 Coq
0.3 Conventions & notations
0.4 Premises
I Mathematics to compute 
1 A theory of sets 
1.1 Bishopian toolkit
1.2 Categories
1.3 Choice!
2 Homological algebra in type theory 
2.1 Homology
2.2 Abelian categories will not fit
2.3 Preabelian categories
2.4 Graded objects and chain complexes
2.5 Kernels of matrices
II Intermezzo: Down to Coq Implementation 
3 Efficient computations 
3.1 A brief history of N
3.2 Going native
3.3 Performance
3.4 Related works
4 A new tactic engine 
4.1 Refinement
4.2 Combining tactics
4.3 About the implementation
4.4 Further work
III Faster, Higher, Stronger 
5 On the category of sets 
5.1 Topoi
5.2 Quasitopoi
5.3 Internal language
6 Sharing more code 
6.1 Categories & additive categories
6.2 Sets as categories and beyond
6.3 The category of graded objects is preabelian
A Coq development for Kernel computations
A.1 Kernels are finite dimensional
A.2 Testing the program
B Strong subsets are classified


Related Posts