1.
Introduction
Kapan
suatu fungsi dilipat? Dalam satu pengertian, definisi dari lipatan menyatakan:
fold : Functor F ⇒ (FA → A) → µF → A fold F f (inF x) = f (F(foldF f ) x)
Sebuah fungsi h :µF →
dapat ditulis dalam sebuah bentuk lipatan lebih tepatnya ketika terdapat f
:F A → A seperti h =
foldF f
. sebagai contoh L A = 1 + Nat × A
sebagai bentuk functor untuk daftar alami, sum : µL → Nat
adalah lipatan: tentunya, sum = foldL add
dimana
add(Inl()) = 0 add(Inr (m, n)) = m + n
Tetapi allEqual :µL → Bool,
Pengujian predikat menyatakan semua elemen dari daftar memiliki nilai yang
sama, bukan lipatan: dengan sedikit upaya (contoh, memperhitungkan panjang
daftar 0, 1, dan 2), salah satu yang dapat meyakinkan bila terdapat no f
dengan allEqual = foldL f .
bagaimanapun, patokan ini kurang memuaskan. Salah satu dapat menggunakan
eksistensi dari f sebagai patokan bukti h adalah lipatan, dengan
memamerkan f ; tetapi sulit untuk menyangkal h adalah sebuah
fold, karena lebih sulit untuk memberikan bukti untuk non-eksistensi apapun
seperti f . Kriteria yang intensional, mengacu ke beberapa sifat f
dari implementasi h, which we may not yet have to hand. Kita mungkin
berharap untuk patokan ekstensional bukannya, menyatakan sepenuhnya sifat h
dari pada impementasi yang mungkin.
Jawaban ekstensional tapi tidak lengkap
diberikan oleh pengamatan bahwa jika h injektif, sehingga terdapat
pasca-inverse h′ dengan h′ ◦ h = id, kemudian
h = foldF (h ◦ inF ◦ Fh′)
2352-2208/©
2015 The Authors. Published by Elsevier Inc. This is an open access article
under the CC BY license ( http://creativecommons.org/licenses/by/4.0/).
dan jadi h
adalah fold. Tetapi injektif pada kondisi yang cukup, bahkan tidak perlu satu, penjumlahan
adalah fold, meskipun tidak injektif. Jadi sekali lagi pengamatan ini tidak
membantu dalam menunjukkan bahwa fungsi bukanlah kali lipat.
Dalam makalah ini, kita membicarakan kondisi yang penting
dan cukup untuk h menjadi lipatan. Hasil telah dijelaskan di awal
makalah [6]. Ternyata
untuk menjadi hasil standar dalam aljabar spesifikasi; lihat contoh [4, §3.10]. Kami menjabarkan awal pekerjaan disini. Presentasi
kami murni dalam segi teori, menangani fungsi berpasang, dan membatasi fungsi.
Disini, kami menunjukkan tambahan sederhana untuk fungsi parsial, dan kami
mempertimbangkan alegoris (yaitu, relasional aksiomatik) presentasi, yang
ternyata menjadi lebih sederhana, dan satu dalam hal kategori biasa, yang
sedikit lebih fleksibel.
Dalam kepentingan singkatnya, kita bicarakan folds dan postfactors. Ada
cerita ganda tentang prefactors, tetapi hubungan yang paling penting dengan
bukan lipatan tidak cukup satu dualitas (Karena dualitas ‘fungsi parsial’ tidak
begitu membantu). Kami meninggalkan rincian untuk pembaca penasaran untuk
mengeksplorasi diri mereka sendiri.
2.
Totally
In this section, we work in the category Set, in which the objects are sets and the arrows are total functions
between sets. In particular, a function f :
A → B is a triple consisting of the source A, the target B,
and the graph, the set of pairs {(a, b) | a ∈ A ∧ b = f a ∈ B} . We write ran f ⊆ B for the range of f .
A
crucial ingredient in the construction is the notion of the kernel of a
function, that is, the set of pairs of arguments
identified
by the function.
Definition 1. The kernel ker f of a total function f : A → B is the set of pairs
ker f = {(a, a′) | a, a′ ∈ A ∧ f a = f a′} ♦
It is
easy to see that this definition yields an equivalence relation on A.
Given h : A
→ C and f
: A → B, when
can h be factorised into g ◦ f for some g : B → C? It is clearly necessary for the function
space B → C to be non-empty, that is, either C = ∅ or B = ∅; otherwise, there can be no such g. Given that proviso, a
necessary and sufficient condition for the existence of such a postfactor g is for
the kernel of h to include the kernel of f :
|
Theorem 2. Given h : A → C and f : A → B such that B → C = ∅,
|
|
|
||
|
(∃g : B
→ C . h = g
◦ f ) ⇔
|
ker
h
⊇ ker f
|
♦
|
|
|
|
Proof. From left to right, suppose that
h = g ◦ f . Then
|
|
|
||
|
(a, a′) ∈ ker h
|
|
]]
|
|
|
|
⇔ [[ definition of kernel
|
|
|
||
|
ha = ha′
|
]]
|
|
|
|
|
⇔ [[ h
= g ◦ f
|
|
|
|
|
|
g (f a) = g (f a′)
|
]]
|
|
|
|
|
⇐ [[ Leibniz
|
|
|
|
|
|
f a = f a′
|
|
]]
|
|
|
|
⇔ [[ definition of kernel
|
|
|
||
|
(a, a′) ∈ ker f
|
|
|
|
|
which
establishes the inclusion. From right to left, suppose that ker h ⊇ ker f ; we construct g as
follows. For b ∈ ran f
, pick any a such that f a = b,
and define gb = h a; by the hypothesis, the
choice of a does not affect the value of gb. For b ∈/ ran f , define gb
arbitrarily; by the assumption that B → C =, this is possible (classically). ✷
Corollary 3. For functor F such that the initial algebra (µF, inF) exists, and for h : µF → A,
(∃g . h = foldF g) ⇔ ker (h ◦ inF) ⊇ ker (Fh) ♦
∃g . h = foldF g
⇔ [[ universal property of fold ]]
∃g . h ◦ inF = g ◦ Fh
|
923
|
(Note that the side condition F A → A = ∅ follows from µF → A = [6],
which follows in turn from the existence of h.) ✷
Remark
4. One can show that
ker (F h) = RelF(ker h), where RelFR denotes the relational lifting of
the relation R on A to a relation
acting pointwise on F A. Moreover, since inF is a bijection, ker (h ◦ inF) is equivalent to just ker h. Finally, given an F-algebra f : F A → A,
we say that a relation R is an F-congruence for f if pointwise-related arguments are
taken by f to related results:
(x, x′) ∈ RelFR ⇒
(f x, f x′)
∈ R
Then the
condition ker (h ◦ inF) ⊇ ker (F h) in Corollary
3 is equivalent to
saying that ker h is an F-congruence for inF, which is the more traditional but
less manipulable formulation. ♦
3.
Partially
The simple characterisation above of the
kernel of a total function needs adaptation, if it is to continue to serve as
an equivalence relation on the source of a partial function:
|
Definition 5. The kernel ker f ⊆ A × A of a partial function f : A →0 B is the set of pairs
|
|
|
|
ker
f
= {(a, a′) |
a, a′
∈ dom f ∧ f a = f a′}
|
♦
|
|
|
∪ {(a, a′) | a, a′ ∈ A − dom f }
|
|
(writing dom f ⊆ A for the domain of
definition of f ). This denotes an equivalence relation again: two
elements are equivalent iff they are treated equivalently by f . When f
is in fact total, dom f = A and Definition
5 reduces to Definition
1.
A postfactor theorem similar to Theorem 2 can be proved for partial functions. The
conditions need to be strengthened in one sense: clearly now it is necessary
for dom f to include dom h . But they may be weakened in another sense: we no longer need
to assume a non-empty space of results, because partial functions exist even to
empty sets.
Theorem 6. Given partial functions h : A →0 C and f : A →0 B,
|
( g
|
:
|
B
|
→0
|
C . h
|
=
|
g
|
◦
|
f )
|
⇔
|
ker h
|
⊇
|
ker f
|
∧
|
dom h
|
⊆
|
dom f
|
♦
|
|
|
∃
|
|
|
|
|
|
|
|
|
|
|
However, the proof is rather more
awkward. It depends on the fact that dom (g ◦ f ) = {a ∈ dom f | f a ∈ dom g}.
Proof. From left to right, suppose that h
= g ◦ f . Then
a ∈ dom h
⇔ [[ h = g ◦ f ]] a ∈ dom (g ◦ f )
⇔
[[ domain ]]
a ∈ dom f ∧ f a ∈ dom g
⇒ [[ weakening ]] a
∈ dom f
|
As for the kernel inclusion,
suppose (a, a′)
|
∈
|
ker
f
, so either (i)
a, a′
|
∈
|
dom
f
and
f a
|
=
|
f a′, or (ii) a, a′
|
/ dom f . In case (i),
either
|
|
|||||||||||||
|
f a, f a′
|
|
|
dom
g, when
a, a′
|
|
dom h and h a
|
|
g (f a)
|
|
g (f a′)
|
|
|
|
|
|
|
∈
|
|
||||
|
∈
|
∈
|
=
|
=
|
=
|
h a′, so (a, a′)
|
∈
|
ker h;
or f a, f a′
/
dom g, when
a, a′
/
dom h, so
|
|
|||||||||||||
|
(a, a′)
|
|
|
|
|
|
|
|
ker h .
|
|
|
∈
|
∈
|
|
||||||||
|
∈
|
ker
h. Finally, in case (ii), again
a, a′
|
/ dom h and so (a, a′)
|
∈
|
|
|
|
|
|
|
||||||||||||
|
|
|
|
|
|
|
∈
|
|
|
|
|
|
|
|
|
|
|
|
|
|||
|
From right to left, suppose that ker h ⊇ ker f
|
and dom h ⊆ dom f ; we construct g
with dom g
= {f a | a ∈ dom h} as follows.
|
|
|||||||||||||||||||
For b
∈ dom g, pick any a ∈ dom h such that f a = b, and define gb = h a; by the hypothesis, the choice of a does
not affect the result (for if a, a′ ∈ dom h ⊆ dom f with f a = f a′,
then (a,
a ′) ∈ ker f ⊆ ker h and so h a = h a′).
Of course, we do not have to consider b ∈/ dom g, so we need no longer resort to classical
reasoning. ✷
4.
Allegorically
The construction in the proof of Theorem 2 essentially involves inverting f ;
this suggests that it might be worth exploring a presentation in terms of the
relational calculus [2]. Rather than work
concretely with relations as sets of pairs, as we did in Section 2 and in [6], we use the
axiomatic presentation of a division allegory [5], falling back on sets of pairs only for
the
purposes of illustration. Formally, we consider typed relations R : A ∼ B ‘from A to B’;
intersection R ∩ S forming a
semi-lattice, and inducing inclusion R ⊆ S as a preorder on relations of a common type;
identity id and composition R ◦
S, forming a monoid, with composition monotonic with respect to ⊆; converse R◦ forming an involution,
contravariant with respect to composition and monotonic with respect to
inclusion; and division operators R / S, R \S discussed in more detail below. One additional
and non-obvious axiom is required, the so-called modular law (R ◦ S) ∩
T ⊆ (R ∩ (T ◦
S◦)) ◦ S.
Four special classes of relations are identified as follows:
|
R injective:
|
R◦ ◦ R ⊆ id
|
R simple:
|
R ◦ R◦ ⊆ id
|
|
R entire:
|
R◦ ◦ R ⊇ id
|
R surjective:
|
R ◦ R◦ ⊇ id
|
We say that R is coreflexive
if R ⊆ id. The domain
of a relation is defined by
dom R = (R◦ ◦ R) ∩ id
with
the universal property that dom R is the smallest
coreflexive S that may be extracted as a prefactor:
|
dom R ⊆ S ⇔ R ⊆ R ◦ S
|
— for coreflexive S
|
|
|
|
Lemma 7. R ◦ dom R = R
|
♦
|
|
|
|
Proof. We have:
|
|
|
|
|
R ◦ dom R
|
]]
|
|
|
|
⊆
|
[[ dom R is coreflexive
|
|
|
|
R
|
[[ instantiate S = dom R in universal property of domain ]]
|
|
|
|
⊆
|
|
||
|
R ◦ dom R
|
✷
|
|
|
|
|
|
|
|
Right
and left division are characterised by their universal properties
|
T ⊆ R/S
|
⇔
|
T ◦ S ⊆ R
|
⇔ S ⊆ R/T
|
|
|
T ⊆ S\R
|
⇔
|
S ◦ T ⊆ R
|
|
These
are the least familiar of the operators of the relational calculus, but they
are truly central: (/S)
forms a Galois con-nection with (◦S ), and (S\) with (S◦), and Galois connections—more generally,
adjunctions—underlie most of the structural equivalences we use in program
calculation [9].
|
Definition
8. The kernel ker R of a relation R is given by
|
|
|
|
ker
R
=
(R\R)
∩ (R\R)◦
|
♦
|
|
|
= (R\R) ∩ (R◦/R◦)
|
|
|
|
In
terms of concrete sets of pairs, the quotients reduce to the following
constructions:
|
|
|
|
(a, b) ∈ R/S ⇔ (∀c . (a, c) ∈ R ⇐ (b, c) ∈ S)
|
|
|
|
(a, c) ∈ S\R⇔ (∀b .
(b, c) ∈ R ⇐ (b, a) ∈ S)
|
|
|
|
and
therefore
|
|
|
|
ker
R
= {(a, a′) |
∀b . (a, b) ∈
R
⇔ (a′, b) ∈ R}
|
|
|
In particular, when R is simple, so
equivalent to a partial function, this agrees with the definition of kernels in
Section 3. We identify three
useful lemmas about kernels, which we will need for the proof of Theorem 12 on postfactors for
Lemma
9. Kernels enjoy
the universal property that
ker R ⊇ S ⇔ R ⊇ R ◦ S ∧ R ⊇ R ◦ S◦ ♦
|
925
|
Proof. This follows from the universal properties of the components:
ker R ⊇ S
⇔
[[ definition of kernel ]]
((R\R) ∩
(R\R)◦) ⊇ S
⇔
[[ universal property of
intersection ]]
(R\R ⊇
S) ∧ ((R\R)◦ ⊇
S)
⇔
[[ converse preserves inclusion ]]
|
(R\R ⊇ S) ∧ (R\R ⊇ S◦)
|
]]
|
|
|
⇔ [[ universal property of division
|
|
|
|
R ⊇ R ◦ S ∧ R ⊇ R ◦ S◦
|
✷
|
|
|
Lemma 10. R◦ ◦ R ⊆ ker R for simple R.
|
|
|
|
♦
|
|
|
|
Proof. We have
|
|
|
|
ker R ⊇ R◦ ◦ R
|
]]
|
|
|
⇔ [[ universal property of kernel
|
|
|
|
R ⊇ R ◦ R◦ ◦ R ∧ R ⊇ R ◦ (R◦ ◦ R)◦
|
|
|
⇔ [[
the
conjuncts are equivalent, by contravariance of converse ]]
R ⊇ R ◦ R◦ ◦ R
⇐
[[ monotonicity ]]
|
id ⊇ R ◦ R◦
|
✷
|
|
Lemma 11. R ◦ ker R ⊆ R
|
♦
|
|
Proof. We have:
|
|
R ◦ ker R ⊆ R
⇔[[ universal property of
division ]] ker R ⊆ R\R
⇔
[[ definition of kernel ]]
true
✷
Theorem 12. For simple T : A ∼ C and R : A ∼ B, there exists simple S : B ∼ C with T = S ◦ R iff ker R ⊆ ker T and dom R ⊇ dom T. ♦
Proof. From left to right,
suppose T = S ◦ R. Then
|
ker R ⊆ ker T
|
]]
|
|
|
|
⇔ [[
|
assumption
|
|
|
|
ker R ⊆ ker (S ◦ R)
|
|
|
|
|
⇔ [[
|
universal property of
kernel ]]
|
|
|
|
S ◦ R ⊇ S ◦ R ◦ ker R ∧ S ◦ R ⊇ S ◦ R ◦ (ker R)◦
|
|
||
|
⇔ [[
|
ker R is symmetric, so the two conjuncts are equivalent ]]
|
|
|
|
S ◦ R ⊇ S ◦ R ◦ ker R
|
|
|
|
|
⇐ [[
|
monotonicity ]]
|
|
|
|
R ⊇ R ◦ ker R
|
]]
|
|
|
|
⇔ [[
|
|
||
|
true
|
|
|
|
|
and
|
|
|
|
|
dom
R
⊇ dom T
|
]]
|
|
|
|
⇔ [[
|
assumption
|
|
|
|
dom
R
⊇ dom (S ◦ R)
|
|
||
|
⇔ [[
|
universal
property of domain (dom R is coreflexive)
]]
|
|
|
|
S ◦ R ◦ dom R ⊇ S ◦ R
|
|
||
|
⇔ [[
|
|
|
|
true
(We don’t actually need the
assumption that R, S, and hence T are simple.) Conversely,
suppose the kernel and domain inclusions on R, T,
and define S = T ◦ R◦. Then T
= S ◦ R:
T
T ◦ dom T
⊆
[[
assumption
]]
T ◦ dom R
|
⊆
|
[[
|
definition of domain ]]
|
|
T
◦ R◦ ◦ R— which
is S ◦ R
|
||
|
⊆
|
[[
|
|
T ◦ ker R
⊆
[[
assumption
]]
T ◦ ker T
T
Moreover, S
is simple:
|
S ◦ S◦
|
||
|
=
|
[[
|
definition of S ]]
|
|
S ◦ R ◦
T◦
|
||
|
=
|
[[
|
by the above, S ◦ R = T ]]
|
T ◦ T◦
⊆
[[
by assumption, T is simple
]]
id
✷
Note that this proof establishes the result in the more general setting
of simple relations, that is, partial rather than total functions, with no
extra fuss. In contrast, the proof of Theorem 6 is rather more complicated than the proof
of Theorem 2, with an awkward
case analysis.
5.
Categorically
One might wonder whether the full structure of a division allegory is
necessary for the postfactors result to hold: the proof in Section 4 uses division heavily, but the more concrete one in Section
2 does not. What abstract structure is actually required?
Definition 13 (Kernel pair). The categorical
analogue of the kernel of a function is the kernel pair of
an arrow, the pullback of the arrow along itself:
|
q0
|
A
|
|
|
f
|
|
|
|
|
|
|
|
|
p0
|
|
Y r
ker f ❅! B
p1
f
q1
A
That is, the kernel
pair of f : A → B is an object X and arrows p0, p1 : X → A satisfying f
◦ p0 = f ◦ p1, with the universal property that, for any other object Y with
arrows q0, q1 : Y → A satisfying f ◦ q0 = f ◦ q1, there is a unique mediating arrow
|
r : Y →
X such that q0 = p0 ◦ r and q1 = p1 ◦ r.
|
♦
|
|
Such
pullbacks do not always exist. They always do in Set, when the object X is just the set of pairs ker f
|
tion 1, and p0, p1 are the left and
right projections; that justifies the use of ‘ker f ’ for X in
the commuting diagram above. More generally,
a finitely complete category possesses all finite limits, and in
particular pullbacks and hence kernel pairs. But for these kernel pairs to be
in some sense well behaved, we need a couple of extra conditions as well.
Definition 14 (Epimorphism,
monomorphism). An arrow g : B → C is an epimorphism
if it is right-cancellable, in the sense that for any h0, h1 : C → D, if h0 ◦ g = h1 ◦ g then h0 = h1.
In Set, the
epimorphisms are the surjections, and the monomorphisms the injections. By
convention, we draw epimorphisms in commuting diagrams with double headed
arrows 
and monomorphisms with hook-tailed arrows 
.
and monomorphisms with hook-tailed arrows .
Definition
15 (Coequaliser). We say
that arrow g :B → C
coequalises a parallel pair of arrows f0 , f1 :A → B if g
◦f0 = g ◦f 1. The coequaliser
of f0, f1 is a
universal such C and g—that is, for any other object D and
arrow h : B → D that
coequalises f0, f1, there is a
unique mediating arrow r : C → D
such that h = r ◦ g.
|
|
f0
|
|
g
|
|
|
|
|
A
|
B
|
|
C
|
|
|
|
|
|
|
|
|
|||
|
|
f1
|
|
|
r
|
|
|
|
|
|
h
|
|
|
|
|
|
|
|
|
|
♦
|
|
|
|
|
|
|
|
D
|
|
In Set, the coequaliser object C is the
quotient of B by the smallest equivalence relation ≡ such that ∀a ∈ A . f0 a ≡
f1 a; that is, the
reflexive, symmetric, transitive closure of the relation induced by f0, f1. It is an instructive exercise to verify that the coequaliser is
necessarily an epimorphism (whatever the category). Not all epimorphisms arise
as coequalisers; those that do are called the regular epimorphisms.
Definition
16 (Regular category). A regular
category is one: that is finitely complete (so in particular has all
kernel pairs); in which every kernel pair has a coequaliser; and in
which regular epimorphisms are stable under pullbacks—that is, if g in
the commuting diagram below is a regular epimorphism, then so is p1.
|
X
|
p0
|
|
A
|
|
|
|||
|
|
|
|
|
|||||
|
p1
|
|
|
|
|
|
g
|
|
|
|
|
|
|
|
|
|
|
|
|
|
A
|
|
|
|
B
|
|
|
||
|
|
f
|
|
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
The category Set is regular.
|
♦
|
|
||||||
Definition 17 (Relation). One can define a notion
of ‘relation’ R : A ∼ B via a span A ← R → B: in a Cartesian category (that
|
is, one with products), R is modelled as a monomorphism R
|
|
A × B into the product:
|
|
|||||
|
|
|
|||||||
|
|
|
R
|
|
|
|
|||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
A
|
|
A × B
|
|
B
|
|
|
|
|
|
fst
|
snd
|
|
|
|
||||
(To be
more precise, one should consider equivalence classes of such spans under
isomorphisms between their apices R. One can also remove the dependence
on products by requiring that the two legs of the span are jointly monic,
suitably defined.) ♦
In Set, this
directly corresponds to thinking of R as a subset of A × B.
But constructing the composition of relations involves taking a pullback of
spans:
•
❅!
R 
S
S
A B C
(and
then taking the ‘image’, as discussed above: the arrow from the apex to A
× C is typically not a monomorphism); in order for
this composition to be associative, one needs the additional well-behavedness
properties of a regular category [5, §1.569]. So regular categories are a somewhat necessary phenomenon
in thinking about relational programming; for a recent
crisp summary, see [7, Section 2].
Definition
18 (Partial map). Similarly,
one can define a partial map f : A →0 B in a
category as a span with a monomorphic left leg:
dom f
f
A 
B
B
writing
f : dom f →
B for the restriction of f to its domain (again, up to
equivalences arising from isomorphisms on the
apices). Composition is again constructed by pullbacks of spans. ♦
Lemma 19
(Image factorisation). An important result about regular
categories is that every arrow f : A → B factorises
into a regular epimorphism followed by a
monomorphism.
|
ker f
|
A
|
f
|
B
|
|
|
|
|
|||
|
|
e
|
|
m
|
|
|
|
|
img f
|
|
|
Indeed,
an alternative chacterisation of regular categories is that they have finite
limits and image factorisations, stable under pull-backs. ♦
In Set, img f is A/ f , the quotient of A into
equivalence classes according to f ; that is, two elements a, a′ ∈ A are equivalent iff f a = f a′ (in other words, (a, a′) ∈ ker f ). So one can
think of e as taking an element of A to its equivalence class,
and m mapping this class into B. Equivalently, one can think of
e as being f but with the target restricted precisely to the range
of f , and m as the embedding of the range back into the target: A/ f is isomorphic to ran f . For more about image factorisation, see Taylor [13].
Theorem 20. Given arrows f : A → B and h : A → C in a regular
category, there exists a partial map g : B →0 C such that h = g ◦ f if and only if there
exists an arrow i : ker f → ker h satisfying p0 = q 0 ◦ i and p1 = q 1 ◦ i, where p0, p1 and q0, q1 are the kernel pairs of f and h respectively. ♦
Proof. The situation is illustrated in the
diagram below:
ker f
|
|
i
|
p0
|
p1
|
|
|
|
|
|
|
|
||
|
ker h
|
q0
|
A
|
h
|
C
|
|
|
|
|
||||
|
q1
|
|
|
|||
|
|
|
|
|
|
|
|
|
|
f
|
e
|
k
|
|
|
|
|
|
|
|
|
|
|
|
B
|
m
|
img f
|
|
|
|
|
|
|
|
From right to left,
suppose we are given i making the two upper left triangles commute; we
construct g as follows. Let m ◦e be the image factorisation of f
(making the lower left triangle commute), so that e is the coequaliser
of p0, p1. Now h also coequalises p0, p1:
|
h
◦ p0 = h ◦ q0 ◦ i = h ◦ q1 ◦ i = h ◦ p1
|
|
|
|
|
|
|
|
|
|
|
so by
the universal property of the coequaliser there exists a unique mediating
arrow k
|
:
|
img f
|
→
|
C
making the upper
right
|
|
||||
|
triangle
commute. We define partial map g : B
→0 C to be the span B
|
m
|
|
k
|
|
|
|
|||
|
|
img
f
|
|
|
C .
|
|
|
|
||
|
|
|
|
|
|
|
||||
We have to show that h = g ◦ f as partial
maps. Since f and h are in fact total, their domain coincides
with their source, and the monomorphic left legs of the spans are the identity.
So for the composition g ◦ f , we have the following situation:|
|
J. Gibbons / Journal of Logical and Algebraic Methods in
Programming 85 (2016) 921–930
|
929
|
|
|
|
X
|
|
|
|
|
❅!
|
|
|
|
A
|
|
img f
|
|
|
f
|
m
|
k
|
|
|
A
|
B
|
C
|
|
and we have to show that the outer span equals h. Let
us factor f into m ◦ e, and see what
effect this has on the pullback diamond:
X
❅! b
|
a
|
Y
|
|
|
|
|
|
|
❅!
|
d
|
|
|
A
|
c
|
img f
|
|
|
|
|
e
|
img f
|
m
|
|
|
|
|
m
B 
We
use two simple standard facts about pullbacks, both of which are
straightforward to prove. Firstly, the pullback of a
|
monomorphism along itself is the identity; so
|
Y
|
=
|
img f
|
, and
|
c
|
=
|
d
|
=
|
id
|
. Secondly, a pullback of
|
the identity (c) is again the
|
|
||||||||||||||
|
|
|
|
|
|
|
|
k e h
|
|
|
|
||||||||||||||||
|
identity; so a = id, and hence X = A and b = e. Therefore,
the outer span is indeed A
|
|
A
|
|
◦ =
|
|
C as required.
|
|
|||||||||||||||||||
|
|
|
|
|
|||||||||||||||||||||||
|
Conversely, given h
= g ◦ f , and kernel
pairs p0, p1 for f
|
and q0, q1
|
for h, we construct the mapping i
: ker f → ker h as
|
|
|||||||||||||||||||||||
|
follows:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
A
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
p0
|
q0
|
|
|
f
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
h
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||
|
ker f
|
i
|
ker h
|
❅
|
|
|
C
|
|
g
|
|
|
B
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||
|
|
|
|
!
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
p1
|
q1
|
h
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
f
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||
|
|
|
|
A
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We have that p0, p1 form a cone over A
|
|
h
|
C
|
|
h
|
|
A :
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||
|
h ◦ p0 = g ◦ f ◦ p0 = g ◦ f ◦ p1 = h ◦ p1
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|||||
|
so by the universal property of the pullback, there exists a
(unique) mediating arrow i : ker f → ker h
|
making the triangles
|
|
||||||||||||||||||||||||
|
p0 = q0 ◦ i and p1 = q1 ◦ i commute.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
✷
|
|
|||
Have we gained anything
by abstracting from Set to
regular categories? If Set were
the only regular category, the answer would be ‘no’ (or at least, ‘not much’:
it is still nice to see precisely which axioms are used, even if those axioms
admit just one model). However, it is a standard result [3] that any
category of Eilenberg–Moore algebras over Set is also regular. In particular, one can think of partial functions
over sets as point-preserving total functions over pointed sets, which are the
homomorphisms between algebras for the monad (1+) ; therefore the category P fun of sets
and partial functions is equivalent to the category of Eilenberg–Moore algebras
for this monad, and hence is regular. So the categorical story is more
flexible; we can instantiate it for free at least to partial functions.
6. Conclusions
Hutton and Thorsten Altenkirch, whose contributions were
invaluable. Bart Jacobs also made some helpful observations about congruences
and images, pointing me towards his paper [8].
Thanks to
comments received at CMCS, I saw how to generalise from total functions to
partial functions; I presented the more general results at Meeting #56 of
WG2.1, in Ameland in September 2001—precisely while the tragedy of the twin
towers was unfolding. Roland Backhouse encouraged me there to use the
relational definition ker R = (R \R)
∩ (R \R)◦ of kernels from Section 4, but we didn’t manage to complete
the proof in the relational style at the meeting. (This notion of kernel turns
out to date back at least to 1948 [12];
it is a special case ker R = syq(R, R) of the ‘symmetric quotient’ used by Schmidt and by Winter
in this volume.) In October 2005, José Oliveira invited me to take part in a
PURe Workshop in Braga; that was the spur I needed to complete the relational
proofs (helped by Shin-Cheng Mu), which I presented there. José liked the results,
because it turned out to be related to work he was doing on pointfree
functional dependency theory [10]; he encouraged me to
write those results up, but I’ve never had the excuse to make time for it—until
now! (Note that the relational definition of
kernels used here is in general incomparable to the definition ker R = R◦
◦ R used by José himself [10,11] as a stepping stone
towards his ‘injectivity preorder’ on relations.)
For help with the categorical construction,
I am indebted to Maciej Piróg for pointing me towards regular categories; to
James McKinna, Ohad Kammar, and Bob Harper, for enlightening discussions; and
especially to Sam Staton, who sketched out the proof of Theorem 20 for me.
Acknowledgements
This work was partially supported by EPSRC
grants Datatype-Generic Programming (GR/S27078/01) and A Theory of
Least Change for Bidirectional Transformations (EP/K020919/1).
