Much of the existing bx literature, especially that from the PL community on lenses, has described extensional, state-based formalisms. More recently, attention has turned to incorporating intensional information about edits (typically based on monoid actions), or more generally, deltas (typically based on categories), describing how models are updated. Pervasive in both the conceptual modelling, and the mathematics, of varieties of such bx, is the role played by the complement, which generalises the `constant complement' case of the view-update problem in databases. Complements typically reify, or correspond to, data which is abstracted away by passing from a source to a view. In this paper, we present an alternative perspective, which has perhaps been implicit in the lens literature, but not, to our knowledge, previously made explicit anywhere: namely that elements of the complement are witnesses to the consistency relation maintained by the transformation. We illustrate this idea with examples drawn from the bx literature, especially that on lenses.
This short paper can be seen as an attempt to formalise an extended suite of observations, which are implicit in the bx literature (though they may be well-known to cognoscenti), especially that on lenses: namely that the (auxiliary) datastructures known as complements, witness instances of an underlying consistency relation, itself often left implicit. Moreover, that the lens operations, and the laws they are intended to satisfy, are precisely in the service of witnessing that the lens operations involved do indeed restore consistency after a model change.
Our starting point is the by-now familiar framework, due originally to Meertens [Mee98] and formalised by Stevens [Ste10] in her analysis of the OMG QVT-R standard, of bx considered as forward and backward transformations to restore a consistency relation R(a; b) between elements a; b of model spaces A; B respectively.
In the search for a unifying framework for bx, in which such consistency relations play a computational r^ole, the paper introduces a de nition, that of generalised complement below, which uses the ideas of abstract realisability [Lau70], to address the questions
What are proofs of consistency? Where/How may they be treated in a computational theory of bx?
The de nition o ers the slightly more permissive view
rst-class citizens A fundamental idea in the development of mathematical logic in the 20th century is that a proposition should be identi ed with the type of its proofs, popularised as the \Curry-Howard-de Bruijn" correspondence [NG14, for example]. From the point of view of ordinary mathematics, a proposition P holds if and only if we have a proof of it, and we do not care to distinguish between di erent proofs. This view accords with that of classical logic, where propositions are either true, or false, and hence the set of proofs of P may be identi ed with a singleton set (if P is true), or the empty set (in case P is false). Indeed, one may take a distinguished singleton set, 1 =def f g, as standing once-and-for-all as a representative of such singleton sets; such an interpretation of propositions in terms of sets is nowadays called proof irrelevant. Indeed, even in the categorical reconstruction of set theory (along intuitionistic lines) [LS88] carried out by Lawvere, Tierney and others in the 1960s and 1970s, a similar move is made, identifying a proposition with a subset of 1, namely P ' f? : 1 j P g.
By contrast, since Kleene's pioneering interpretation [Kle45] of intuitionistic logic in terms of sets of natural numbers (encoding recursive functions), and Kripke's poset-of-possible-worlds interpretation of modal logic [Kri63], there has been a separate tradition of proof relevant interpretations of logic. Lauchli's framework of abstract realisability [Lau70] ushered in the modern era, de ning interpretations by identifying, for each well-formed formula P , a set Prf (P ) of abstract realisers r of P , which one may think of as candidate, or potential, proofs of P , together with a relation, r realises P , such that the proposition P is then identi ed as that subset of candidate proofs which do in fact realise, or witness, that the proposition holds:
P ' fr : Prf (P ) j r realises P g 3
To motivate the eventual de nition of generalised complement, let us begin with Barbosa et al.'s alternative reformulation [BCF+10] of the by-now familiar de nition of (very-well-behaved) asymmetric lens. In the interests of brevity in what follows, many technical details and proofs have been omitted. 3.1
An asymmetric lens [FGM+07] between non-empty source type S and view V , with complement C, may be given by the following data: a `get' function get :S ! V . a `put' function put :V C ! S, and a `residual' function res :S ! C, satisfying the following properties: `GetPut', put (get s; res s) = s; `PutGet', get (put (v; c)) = v; and `PutRes', res (put (v; c)) = c. The consistency relation enforced by such a lens is given by R(s; v) =def v = get s. The PutGet law then states that consistency is indeed restored after an update, i.e. R(put (v; c); v).
What, then, of the complement set C? We argue that the element c = res s is a (indeed: the unique) witness to the consistency of s and get s. Accordingly, consider the sets
T (s; v) =def fres s j R(s; v)g; for each s : S; v : V Then, any inhabitant of T (s; v) establishes the corresponding proposition that R(s; v) holds. With S and V non-empty, PutRes implies that res is surjective, and hence that the image of res , viz. Ss;v T (s; v), is equal to C. Thus, every c : C arises as a witness c = res s to the corresponding proposition R(s; get s) for some s : S. 3.2
Given sources A; B, subject to a consistency relation R A B, say that a set C, together with a family of sets T (a; b) (for a : A; b : B) forms a generalised complement for the relation R, if and only if: (y) 8a : A; b : B: T (a; b) inhabited i
R(a; b) and; additionally; (z)
[
C That is to say, C is a set of abstract realisers for R, with T (a; b) delineating those which actually witness R(a; b). NB. When A (or B), is empty, let T (a; b) =def ;; then any C determines a generalised complement for R =def ;. Ahman and Uustalu have recently considered the following de nition [AU14] of update lens between source type S and view V , which combines a state-based account of S and V , together with an edit-based account of view update, using an edit monoid P =def (P; ; ): an update lens consists of a `lookup' function lkp :S ! V , an `action' function act :V P ! V , and an `update' function upd :S P ! S such that `action' is a (right-) action of P on V , and `update' a (right-) action of P on S `lookup' determines a homomorphism between these two actions (Further details are omitted)
Update lenses do not explicitly identify a notion of lens complement, nor indeed a notion of consistency relation between source and view types. Nevertheless, the foregoing analysis still applies: we may de ne a consistency relation R(s; v) =def v = lkp s. Given any update p to v yielding new view v0 = act (v; p), it su ces, in order to restore consistency, to take s0 =def upd (s; p), since lkp is a homomorphism of monoid actions. Furthermore, in particular R(s; v) holds if and only if 2 T (s; v) =def fp j act (lkp s; p) = vg, that is, if a distinguished special witness, the identity element , belongs to T (s; v). More generally, consider the the relation between s and v de ned by 9p : P:p 2 T (s; v), with the monoid element p : P representing the \extent to which s and v may be considered consistent". For this relaxed notion of consistency, the carrier P of the monoid, together with the sets T (s; v), de nes a generalised complement.
Furthermore, since lkp is a homomorphism, if p 2 T (s; v), then for any p0 we have p p0 2 T (s; act (v; p0)), likewise p0 2 T (upd (s; p); act (v; p0)). Thus, if R(s; v) holds, i.e. 2 T (s; v), then p0 2 T (s; act (v; p0)), and hence also 2 T (upd (s; p0); act (v; p0)), by straightforward equational reasoning. Thus the more strict notion R of consistency is also restored by the update operations on source and view. 3.3.2
Hofmann et al. de ne a symmetric lens [HPW11] between X and Y with complement C in terms of two functions putXY :X C ! Y C, putYX :Y C ! X C subject to certain equational stability laws governing round-tripping (omitted). Then the set C, together with the sets
T (x; y) =def fc j putXY (x; c) = (y; c) ^ putYX (y; c) = (x; c)g then de nes a generalised complement for the consistency relation R(x; y) =def 9c : C:c 2 T (x; y), that is, prescribing R in such a way that the conditions (y) and (z) hold by de nition. Then the round-trip laws ensure that given x; y such that R(x; y) holds (witnessed by inhabitants c of T (x; y)), and an updated model x0, the operation putXY (x0; c) computes an updated model y0, and a new witness c0 2 T (x0; y0), and similarly for putYX . 3.3.3
Technically perhaps the most intricate of the lens constructions developed by Pierce and his collaborators, an edit lens [HPW12] between pointed sets (X; x0) and (Y; y0) with pointed complement (C; c0) consists of:
C; and a set K
X
C
Y , called the consistency relation subject to the conditions (ignoring those governing initial states) if (x; c; y) 2 K, x0 = p X x is de ned for p 2 @X, and putXY (p; c) = (q; c0), then y0 = q Y y is de ned and (x0; c0; y0) 2 K; and the corresponding condition for edits q in @Y .
Then, as above, the complement C, together with the sets T (x; y) =def fc j (x; c; y) 2 Kg , de nes a generalised complement for the relation R(x; y) =def 9c : C:c 2 T (x; y). The conditions on K indeed then specify that well-de ned updates in X, resp. Y , give rise to well-de ned updates in Y , resp. X, such that consistency in the sense of R is restored. Diskin et al. introduced asymmetric and symmetric variants of a notion of delta lens [DXC11a, DXC+11b], based on the fundamental notion of model space as category, generalising previous accounts of updates-via-editmonoids. Indeed, one can see the (partial) monoid actions (X; @X) of a symmetric edit lens as a attening out of such structure, with homsets HomX (x; x0) given by f 2 @X j X x = x0g etc.
Given categories A, B, a delta lens between them is then de ned in terms of an assignment of corrs (for correspondences ), abstract links rab relating an object a of A to object b of B. The diagram-theoretic properties demanded of such corrs, and their interaction with the structure of identities and composition in A, resp. B, amount to the prescription of such links as abstract witnesses to consistency between models a and b, for a generalised complement de ned by T (a; b) =def frab j rab is a corr between a and bg and (an implicit) C simply given by the union of all such sets of corrs. The bx literature is rich in competing approaches, not directly comparable to the approach of the PL literature on lenses. Nevertheless, we consider it fruitful to try to identify candidate structures within such frameworks which may play the role of (generalised) complements, as a basis for further comparison and discussion of the \proof-relevant" perspective on witnessing consistency sketched here.
Indeed, the original starting point for this investigation was an attempt to understand the intricacies of Barbosa et al.'s de nition [BCF+10] of matching lens. There, the structure of the complement plays a dual ro^le, enforcing both \chunk consistency", and for each chunk, consistency with respect to the underlying basic lens. Space considerations forbid further discussion of this example, postponed instead to a future full paper. 4
This paper formalises an observation, which deserves to be more commonplace, in terms of the de nition of generalised complement given above, and illustrated through various examples, namely that: the consistency relations maintained by bx are witnessed by elements of appropriate auxiliary datastructures; such datastructures already play a well-de ned role in the formulation, and construction, of such bx, namely in terms of a well-de ned generalisation of the notion of (lens) complement.
Such a modest, and perhaps simple-minded, observation, leads us to the conclusion that the designers and implementors of new bx formalisms, or variations thereof, should place front-and-centre of their proposals: the consistency relation intended to be maintained by such bx; the datastructures which de ne witnesses to such consistency; and, the (obvious) hygiene check that the manipulation of such complements during forward and back restoration steps does, indeed, compute witnesses to such consistency between models being restored.
One may, with good reason, consider that most, if not all, existing bx de nitions in the literature ful l such goals, along the lines sketched in our catalogue of examples. The modest proposal of the current paper is simply that such considerations be made explicit, and thus hopefully provide further insight into the design and implementation of future proposals for bx as computational artefacts.
I speculate that one reason that existing bx/lens de nitions do not make such data explicit arises from the essentially opportunistic choice of programming language infrastructure, which, at least until recently, has been insu ciently rich to support the notion of types-as-propositions inherent in the de nition of generalised complement. Elsewhere [McK16], I intend to pursue the theme of this paper, with a proposal to bring under one foundational roof, in terms of the language and insights from dependent type theory, most if not all existing bx formalisms.
This work is funded by EPSRC (EP/K020218/1). I thank the Bx 2016 PC and referees, and my colleagues at Edinburgh and Oxford for their feedback and support during its development. [AU14]
Danel Ahman and Tarmo Uustalu. Coalgebraic update lenses. ENTCS, 308:25{48, 2014. [HPW11] [HPW12]
Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner. Symmetric lenses. In POPL, pages 371{384. ACM, 2011.
Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner. Edit lenses. In POPL, pages 495{508. ACM, 2012.
S.C. Kleene. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10(4):109{124, 1945. doi:10.2307/2269016.
S. Kripke. Semantical Analysis of Modal Logic I. Normal Modal Propositional Calculi. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 9:67{96, 1963.
Lambert Meertens. Designing constraint maintainers for user interaction. Unpublished manuscript, available from http://www.kestrel.edu/home/people/meertens/, June 1998.
Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof. CUP, 2014.