Bx Examples Repository
Title: weakVsStrongContinuity
Version: pre 0.1 (editing in progress!)
Type: Precise
Overview
Models
$M = \mathbb R \cup \{C_M\}$
$N = (\mathbb B \times \mathbb R) \cup \{C_N\}$.
Consistency
$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:
- 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$;
- return $(\top, x_m)$ if $x_m \ge 0$, $(\bot, x_m)$ otherwise; or we could even go for bizarre behaviour such as
- return $(\top, x_m)$ if $x_m$ is rational, $(\bot, x_m)$ otherwise.
Properties
Correct and hippocratic.
Discussion
References
This is Example 4.7 from
@inproceedings{cheney15:bx,
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
}
Author(s)
Perdita Stevens
