# 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.*