Bx Examples Repository
Title: Non-minimally interfering span of lenses
Version: 0.1
Type: Precise
Overview
Presents a span of lenses that are and history ignorant, free from leaks and projectionally difunctional, but not minimally interfering.
This demonstrates that the latter condition is independent from (i.e. not implied by) the other three.
The definition of these four conditions are available in [1].
Models
Let $V_A=V_B=\{ 0,1 \}$, while $S=\{ 0,1 \} \times \{ 0,1 \}$; denote as $\oplus$ the modulo 2 addition operator.
Consistency
The other two models are determined by $S$ via the following two identical functions:
$\langle x,y \rangle.{GET}_A := x$
$\langle x,y \rangle.{GET}_B := x$
Consistency Restoration
The following restorers complete the lenses $A,B$:
$\langle x,y \rangle.{PUTBACK}_A(x') := \langle x',y \rangle$
$\langle x,y \rangle.{PUTBACK}_B(x') := \langle x',y \oplus x \oplus x' \rangle$
In other words, $A$ reads and writes the first component of the source tuple, preserving the second; $B$ reads and writes the first component, preserving the binary sum of the two components.
Properties
- The span formed by lenses $A,B$ is history ignorant, free from leaks and projectionally difunctional, but it is not minimally interfering.
Discussion
Origin, utility, interest, representativeness, related examples in the literature, …
References
[1] Gábor Bergmann: "Controllable and Decomposable Multidirectional Synchronizations". Submitted to SoSyM, in review.
Author(s)
Gábor Bergmann
Reviewer(s)
We intend that examples remain provisional (version 0.x) until reviewed (and approved, if necessary after modification) by other members of the wiki. In the interest of traceability and credit, such reviewers are identified here.
Comments
This is where any member of the wiki can comment.
