Bx Examples Repository

Title: weakVsStrongContinuity

Version: pre 0.1 (editing in progress!)

Type: Precise



$M = \mathbb R \cup \{C_M\}$

$N = (\mathbb B \times \mathbb R) \cup \{C_N\}$.


$R(C_M, C_N)$ and $R(m, (\_, m))$ for all $m \ne C_M$

Consistency Restoration

$\overleftarrow{R}(m,n)$ has no choice given that we want correctness: it returns the unique $m'$ consistent with $n$.

$\overrightarrow{R}(C_M,n) = C_N$ for any $n$

If $m = x_m$ and $n = (b,x_n)$ are both drawn from the copies of $\mathbb R$, we must return $(b',x_m)$ for some $b'\in\mathbb B$. If in fact $x_m=x_n$, hippocraticness tells us we must return exactly $n$. Otherwise, we could legally return a result which is on the other branch from $n$, that is, flip the boolean as well as changing the real number. It is easy to argue, though, that to do so violates any reasonable least change principle, since the boolean-flipping choice gives us a change in the model which is larger by our chosen metric, with no obvious prospect for any compensating advantage. Let us suppose we agree not to do so.

The interesting case is $\overrightarrow{R}(x_m, C_N)$ for real $x_m$. We must return either $(\top, x_m)$ or $(\bot, x_m)$; neither correctness nor hippocraticness place any further restrictions, and when we look at one restoration scenario in isolation, our metric does not help us make the choice, either. We could, for example:

  1. pick a boolean value and always use that, e.g. $\overrightarrow{R}(x_m, C_N) = (\top, x_m)$ for all $x_m \in \mathbb R$;
  2. return $(\top, x_m)$ if $x_m \ge 0$, $(\bot, x_m)$ otherwise; or we could even go for bizarre behaviour such as
  3. return $(\top, x_m)$ if $x_m$ is rational, $(\bot, x_m)$ otherwise.


Correct and hippocratic.



This is Example 4.7 from

author = {James Cheney and Jeremy Gibbons and James McKinna and Perdita Stevens},
title = {Towards a Principle of Least Surprise for Bidirectional Transformations},
booktitle = {Proceedings of {Bx} 2015},
year = 2015,
ee = {http://ceur-ws.org/Vol-1396/p66-cheney.pdf},
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
volume = 1396


Perdita Stevens



Unless otherwise stated, the content of this page is licensed under GNU Free Documentation License.