Bx Examples Repository
Title: Wikipedia Translation
Version: 0.1
Type: Sketch
Overview
This example demonstrates that the reasonable bx programmer may sometimes want to define bx that are not simply matching. We started off by thinking about whole instances of Wikipedia, but in fact, the interesting issues already arise at the level of single articles, so we write in those terms here. There is nothing special about Wikipedia!
Models
Let $M$ be the set of possibly empty English texts
Let $N$ be the set of possibly empty Portuguese texts
Consistency
$R(m,n)$ iff ($m$ is empty iff $n$ is empty)
(Motivation: if both texts exist, we're going to assume someone has already done an intelligent translation job; we do not attempt to formalise the translation between English and Portuguese.)
Consistency Restoration
Forward
Given $m$ and $n$, return:
- empty, if $m$ is empty
- the result of translating $m$ into Portuguese, if $m$ is non-empty and $n$ is empty
- $n$, otherwise.
Backward
dually.
Properties
Correct, hippocratic. Not history ignorant or even undoable. Not simply matching. (Informally: if it were simply matching, there would be a common abstraction of both kinds of maybe-texts, such that we could reexpress the bx as the tail-to-tail composition of two lenses that each used one kind of maybe-text as the source and the common abstraction as the view, and such that maybe-texts were consistent iff the get functions took them to the same point in the common abstraction, while the consistency restoration function would be the result of using the target-side lens's put function on the original target model and the result of the source-side lens's get function on the source-side model. But the consistency definition forces the common abstraction to be just Boolean (is the text present, or not) which means that the consistency restoration definition cannot be what we want: if we restore consistency on a text on the source side and an absent text on the target side, the lens's put function does not have the original text available to translate.)
Discussion
You can do the same with your favourite bx. Let $R: M \leftrightarrow N$ be a correct and hippocratic bx, with consistency restoration functions $forwardR$ and $backwardR$. Let $M^+$ be the disjoint union of $M$ with NONE, and so on. Let $f : M \rightarrow N$ and $g : N \rightarrow M$ be functions. Then define an optionalised version of $R$, which we denote $R^+ : M^+ \leftrightarrow N^+$, by
$R^+(m,n)$ if: (($m$ is NONE iff $n$ is NONE) and (if neither is NONE then $R(m,n)$ holds).
Given $m$ and $n$, forward consistency restoration returns:
- NONE if $m$ is NONE
- $f(m)$ if $m$ is non-NONE and $n$ is NONE
- $forwardR(m,n)$ otherwise.
Dually for backward consistency restoration, using $g$.
Then $R^+$ is correct and hippocratic provided that $R(m,f(m))$ and $R(g(n),n)$ always hold.
In the actual Wikipedia translation example, we have done this process to the universally consistent bx (which accepts any English text as consistent with any Portuguese one) with translation functions for $f$ and $g$.
Author(s)
Perdita Stevens