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.
