# Bx Examples Repository

# Title: Non-difunctional / non-leak-free span of lenses

## Version: 0.1

## Type: Precise

## Overview

Presents two variant spans of lenses that are both *minimally interfering* and *history ignorant*, but each satisfy exactly one of the properties *freedom from leaks* and *projectional difunctionality*.

This demonstrates that the latter two conditions are both 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_C=\mathbb{Z}$, while $S=V_B= \mathbb{Z}\times\mathbb{Z}$.

## Consistency

The other three models are determined by $S$ via the following functions:

$\langle a,c \rangle.{GET}_A := a$

$\langle a,c \rangle.{GET}_B := \langle\lfloor (a + c)/2 \rfloor, c \rangle$

$\langle a,c \rangle.{GET}_C := c$

## Consistency Restoration

The following restorers complete the lenses $A,B,C$:

$\langle a,c\rangle.{PUTBACK}_A(a')=\langle a',c\rangle$

$\langle a,c\rangle.{PUTBACK}_B(\langle b'_1,b'_2\rangle)=\langle 2b'_1 - b'_2 + ((b'_2 + a) \bmod 2), b'_2\rangle$

$\langle a,c\rangle.{PUTBACK}_C(c')=\langle a,c'\rangle$

In other words, $A$ respectively $C$ reads and writes the first resp. second component of the source tuple, preserving the other; while $B$ reads and writes all information in the source, except $a\bmod 2$.

## Properties

- The span formed by lenses $A,B$ is
*minimally interfering*and*history ignorant*and*free from leaks*, but not*projectionally difunctional*.- In particular, source states $\langle 0,0\rangle,\langle 1,0\rangle $$ witness that B-value $\langle 0,0\rangle$ is cross-consistent with A-values $0,1$. Also, source state $\langle{0,1}\rangle$ witnesses that B-value $\langle{0,1}\rangle$ is cross-consistent with A-value $0$. But it is not cross-consistent with A-value $1$ (since $\langle{1,1}\rangle.{GET}_B=\langle{1,1}\rangle$), violating projectional difunctionality.

- On the other hand, the span formed by lenses $B,C$ is
*minimally interfering*and*history ignorant*and*projectionally difunctional*, but not*free from leaks*.- In particular, source states $\langle 0,0\rangle,\langle 1,0\rangle $$ are congruent in B, both yielding $\langle 0,0\rangle$. Applying ${PUTBACK}_C(1)$ leads to source states $\langle 0,1\rangle,\langle 1,1\rangle $$, respectively yielding $\langle{0,1}\rangle, \langle{1,1}\rangle$ ; thus B is not free from leaks via C.

## Discussion

C is actually the complement of A, making the two above observations in fact equivalent (to be discussed in a future paper).

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