=Paper=
{{Paper
|id=Vol-2355/paper7
|storemode=property
|title=Symmetric c-Lenses and Symmetric d-Lenses are Not Coextensive
|pdfUrl=https://ceur-ws.org/Vol-2355/paper7.pdf
|volume=Vol-2355
|authors=Michael Johnson,François Renaud
|dblpUrl=https://dblp.org/rec/conf/bx/JohnsonR19a
}}
==Symmetric c-Lenses and Symmetric d-Lenses are Not Coextensive==
https://ceur-ws.org/Vol-2355/paper7.pdf
Symmetric c-Lenses and Symmetric d-Lenses are Not
Coextensive
Michael Johnson François Renaud
Macquarie University Université Catholique
Sydney de Louvain
Abstract
This short paper addresses a long standing open question about sym-
metric lenses, with the result succinctly summarised by the paper’s
title.
1 Introduction
It has been clear for some years that symmetric lenses of various kinds can be constructed in a systematic way as
equivalence classes of spans of asymmetric lenses of corresponding kinds [4]. For example, given a definition of
asymmetric delta lens [1], referred to here and elsewhere as a d-lens [3], one can systematically construct a notion
of symmetric d-lens [2, 5], and a category whose morphisms are those symmetric d-lenses. Among the d-lenses
there are some particularly useful lenses, called c-lenses [7] (and previously known to the mathematical community
as split opfibrations) which have an attractive universal property that in many applications corresponds to least
change updating. Naturally there has been interest in symmetric c-lenses, which can again be systematically
constructed, and which might be expected to have an attractive universal property which could perhaps in
applications capture a new notion of least change symmetric lens updating [6]. However, the effects of the
universal properties of the component c-lenses of a span of c-lenses occur mainly in the peak of the span, and
that corresponds in applications to hidden data. Indeed, it can be shown that every span of c-lenses, viewed
as a symmetric lens, is equivalent to a span of d-lenses in which the component d-lenses are not themselves
c-lenses. In other words, the behaviour of a symmetric c-lens can always be obtained from a span of lenses which
themselves do not have the c-lens universal property. And that raises the until now open question of whether
there are in fact any differences at all between symmetric c-lenses and symmetric d-lenses.
In this paper we show that a span of c-lenses does have a weak symmetric lens universal property, and that
there are spans of d-lenses that do not exhibit this property, establishing that there are symmetric d-lenses which
never arise as symmetric c-lenses.
In mathematical terms: We look at spans of functors (G, D) with common domain R, and the induced relation
(R, G, D) between the codomain categories. We discuss properties of these relations that are satisfied when the
legs of the span are opfibrations. More precisely when the left leg G admits a splitting, the relation admits
an induced so called a left-right behaviour δ. Roughly it associates a related morphism on the right to a given
morphism on the left. If the splitting is opfibrant then given a factorization on the left, whose composite is related
to a morphism on the right, there is a related factorization on the right built from the left-right behaviour δ and
the universal property of the left leg G. We build a counter-example showing that such a factorization on the
right cannot always be obtained from a factorization on the left when G is not opfibrant.
Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In: J. Cheney, H-S. Ko (eds.): Proceedings of the Eighth International Workshop on Bidirectional Transformations (Bx 2019),
Philadelphia, PA, USA, June 4, 2019, published at http://ceur-ws.org
66
2 Definitions
G /
Let R and G be categories and R G be a functor between them.
2.1 Splittings and Opfibrations
Definition 2.1. Assuming that all our categories are conveniently small, a splitting P for the functor G is a
family (Px )x∈Ob(R) of functions, indexed by the objects x of R, between unions of homsets with fixed domain:
G(G(x), −)
Px
/ R(x, −)
S S
The notation R(x, −) denotes the union y∈Ob(R) R(x, y), and similarly G(G(x), −) = z∈Ob(G) G(G(x), z). The
image Px (f ) of a morphism f with domain G(x) is called the lifting of f at x (by P ) and is required to satisfy
G(Px (f )) = f .
Moreover a splitting is required to satisfy:
1. identities of G are lifted to identities of R;
2. if f and g are composable morphisms in G with liftings Px (f ) with codomain y say, and Py (g), then the
composite of the liftings, Py (g)Px (f ), is equal to the lifting of the composite, Px (gf ).
Definition 2.2. A morphism x
f
/ y in R is said to be opcartesian (with respect to G) if for any other
morphism x
g
/ z such that there exists a morphism G(y) t /
G(z) in G with G(g) = tG(f ), there is a unique
t0 /
morphism y z in R such that g = t0 f and G(t0 ) = t:
6 G(z)
O 6 zO
G(g) g
if t then t0
/ G(y) x /y
G(x) f
G(f )
Definition 2.3. • The functor G is said to be an opfibration if for every object x in R, each morphism
0
G(x)
f
/ y in G admits an opcartesian lifting x f / y 0 (i.e. an opcartesian arrow f 0 such that G(f 0 ) = f ).
• Moreover a splitting P for an opfibration G is a splitting in the sense of Definition 2.1 such that all liftings
by P are opcartesian.
G /
The above definitions give precise mathematical representations of d-lenses and c-lenses: d-lenses R G
G /
are splittings, and c-lenses R G are split opfibrations.
2.2 Spans, Relations, and Left-Right Behaviours
Given again categories R and G and R / G a functor between them, let D be another category and R / D
G D
another functor so that we have the span (R, G, D):
R
G D
z $
G D
Definition 2.4. We define the relation (R, G, D) between G and D associated to the span (G, D) as follows.
• Two objects x in G and y in D are defined to be related xRy if and only if there is w in R such that G(w) = x
and D(w) = y. We then call w the witness and we sometimes include w in the notation by writing xRw y.
• The relation on morphisms is defined similarly.
67
Of course we have that if f Rq g then the domains and codomains of f and g are related by (R, G, D) with
witnesses the domain and codomain of q. Also xRy if and only if idx R idy .
Definition 2.5. Left-right behaviour of (R, G, D):
• Given an object x in R we have G(x)Rx D(x), and then G(x) and D(x) are called synchronized states.
Then consider a morphism G(x)
f
/ y , which we may call a change of state in G, from G(x) to y.
• We say that (R, G, D) has a left-right behaviour δ if for each such choice of x and f , there is a corre-
sponding synchronisation in D, i.e. there is a given morphism (change of state) δ(f, x) of D with domain
D(x) and such that f Rδ(f, x).
• One can define a right-left behaviour of a span similarly.
• Suppose that G admits a splitting P . Then there exists an induced left-right behaviour, denoted δP , de-
Px (f )
fined, for x and f as before, by the lifting of f , x / y 0 in R, which yields a common change of state in R.
δP (f,x)..=D(Px (f ))
It then suffices to take the image by D in order to obtain the synchronisation D(x) / D(y) .
When G and D are both d-lenses, the induced left-right behaviour corresponds to the forward propagation of
the corresponding symmetric d-lens, and similarly, the induced right-left behaviour corresponds to the backward
propagation.
2.3 Weakly Opcartesian Behaviours
We identify now a property of behaviours of (R, G, D) which is not necessarily satisfied in general but which is
always satisfied when G is an opfibration.
Definition 2.6. Suppose that (R, G, D) has both a given left-right behaviour δ and a given right-left behaviour
γ. We define what it means for δ to be weakly opcartesian with respect to γ.
• Let G(x)Rx D(x) be synchronized states and let G(x)
f
/ y be a change of state which is carried by the
δ(f,x)
forward behaviour to D(x) / D(y 0 ) .
k /
• Consider a change of state D(x) z in D, which is carried by the backward behaviour to γ(k, x):
6 G(z )
00 5z
γ(k,x) k
/y D(x) / D(y 0 ).
G(x) δ(f,x)
f
l /
• Now suppose that there exists a morphism y G(z 00 ) such that γ(k, x) = lf , we then say that δ is weakly
opcartesian with respect to γ if and only if for each such x, f , k and l, there is an induced l0 in D such
that lRl0 and k = l0 δ(f, x):
00 5 zO
γ(k,x)
6 G(zO ) k
l0
l
/y D(x) / D(y 0 )
G(x) δ(f,x)
f
Remark 2.7. One may want to think of Definition 2.6 as a particular instance of the property of (R, G, D)
which we call left-right-compatible with factorizations: if kRk 0 and k factorizes as k = lf in G, then there
are l0 and f 0 in D such that lRl0 , f Rf 0 and l0 f 0 = k 0 .
68
Now symmetric lenses are equivalence classes of spans of asymmetric lenses, and it is important to note
that the induced left right behaviour is an invariant of the equivalence. Indeed, the reason the equivalence was
introduced for symmetric lenses was because differences that aren’t visible in left-right or right-left behaviours
are irrelevant for symmetric lenses.
Thus, if a span of lenses induces a left-right behaviour δ which is weakly opcartesian with respect to its right-
left behaviour γ, then any equivalent span of lenses also exhibits a left-right behaviour that is weakly opcartesian
with respect to its right-left behaviour. In other words, the left-right behaviour being weakly opcartesian with
respect to the right-left behaviour is an invariant among representatives of the equivalence class.
3 Observations
Lemma 3.1. Given (R, G, D), if G is an opfibration and P is a splitting for it in the sense of Definition 2.3,
while D is a functor and S is a splitting for it (so in the sense of Definition 2.1), then the induced left-right
behaviour δP , is weakly opcartesian with respect to the induced right-left behaviour γS .
Proof. Given a synchronization G(x)Rx D(x) and a morphism k : D(x) → z in D, if γS (k) factorizes as ts in
G, then by the universal property of the opcartesian lifting Px (s) of s, there is an induced t0 , as in the diagram
below, such that G(t0 ) = t. Taking the image by D then concludes the proof:
7 yO z = D(y)
6 G(y)
O Sx (k) 5 O
γS (k,x) 0 k
yields t
and thus D(t0 )
t
x /z 0
/ D(z 0 )
G(x) /z Px (s) D(x)
s δP (s,x)
Counter-example 3.2. Consider the categories R, G, D, and the functors G, D illustrated in the diagram
below. ;u
l
5y
f O
t
x /z
s D(u)
:
G D D(l)
G(f )=G(l) 5 G(y)
O y % 5 D(y)
O
G(t) D(f ) D(t)
G(x) / G(z) D(x) / D(z)
G(s) D(s)
We observe that the relation (R, G, D) is not left-right-compatible with factorizations since G(l) admits a
factorization through G(s) but D(l) does not factorize through D(s). Also G and D may be equipped with
splittings, but G cannot be an opfibration since s, the only possible lifting of G(s), is not opcartesian. Under
Definition 2.1 there can in this case be only one choice of a splitting for each functor. The splitting of G, P say,
gives us an induced left-right behaviour δP , and the splitting of D, S say, gives us an induced right-left behaviour
γS .
The left-right behaviour δP is not weakly opcartesian with respect to γS .
4 Conclusion
We have just provided a relatively simple counterexample to resolve a longstanding open question. The question
was whether the symmetric lenses obtained as equivalence classes of spans of c-lenses, and those obtained as
equivalence classes of spans of d-lenses were in fact different.
If the counterexample is so simple, why has it taken so long? It is the theoretical work of this paper that
makes the above span of d-lenses into a counterexample. The difficulty is a common problem: Proving that there
is no span of c-lenses that is equivalent to the span of d-lenses shown above is, a priori, very difficult. What we
have done in this short paper is identify a property of a span of c-lenses that is also present in all equivalent spans
of d-lenses. Since that property is not exhibited by the span of d-lenses above, that span cannot be equivalent
to any span of c-lenses, thus resolving the question and showing that c-lenses and d-lenses are not coextensive.
69
References
[1] Diskin, Z., Xiong, Y. and Czarnecki, K. (2011) From State- to Delta-Based Bidirectional Model Transfor-
mations: the Asymmetric Case, Journal of Object Technology 10, 1–25. doi:10.5381/jot.2011.10.1.a6
[2] Zinovy Diskin, Yingfei Xiong, Krzysztof Czarnecki, Hartmut Ehrig, Frank Hermann and Francesco Orejas
(2011) From State- to Delta-Based Bidirectional Model Transformations: the Symmetric Case. Lecture Notes
in Computer Science 6981, 304–318. doi:10.1007/978-3-642-24485-8-22
[3] Johnson, M. and Rosebrugh, R. (2013) Delta lenses and opfibrations. Proceedings of the 2nd International
Workshop on Bidirectional Transformations, Rome Electronic Communications of the EASST 57, 18pp.
[4] Johnson, M. and Rosebrugh, R. (2016) Unifying set-based, delta-based and edit-based lenses. Proceedings
of the 5th International Workshop on Bidirectional Transformations, Eindhoven CEUR Proceedings 1571,
1–13.
[5] Johnson, M. and Rosebrugh, R. (2017) Symmetric delta lenses and spans of asymmetric delta lenses. Journal
of Object Technology, 16, 2:1–32.
[6] Johnson, M. and Rosebrugh, R. (2017) Universal updates for symmetric lenses. CEUR Proceedings 1827,
39–53.
[7] Johnson, M., Rosebrugh, R. and Wood, R. J. (2012) Lenses, fibrations and universal translations. Mathe-
matical Structures in Computer Science 22, 25–42.
70