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