Non-minimally interfering span of lenses

Title: Non-minimally interfering span of lenses

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.

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.