Russell O’Connor’s Blog2018-01-06T16:40:28ZRussell O’Connorhttp://r6.ca/http://r6.ca/blog/http://r6.ca/blog/20180106T164028Z.htmlVerifying Bech32 Checksums with Pen and Paper2018-01-06T16:40:28Z2018-01-06T16:40:28Z
<p>Today we are going to learn how to verify a <a title="Base32 address format for native v0-16 witness outputs" href="https://github.com/bitcoin/bips/blob/master/bip-0173.mediawiki">Bech32</a> checksum using only pen and paper.
This is useful in those cases where you need to urgently validate the checksum of a Bech32 address, but the electricity has gone out in your home or office and you have lost your smartphone.
</p><p>We are going to do a worked example of verifying the checksum of <code>BC1SW50QA3JX3S</code>, which is one of the test vectors from the <a title="Base32 address format for native v0-16 witness outputs" href="https://github.com/bitcoin/bips/blob/master/bip-0173.mediawiki">Bech32 specification</a>.
However, before we begin, we need to make some preparations.
We will need three tables.
</p><table summary="The table of power embodies the essence of the Goddess of Power, Din.">
<caption>The table of power</caption>
<tbody>
<tr>
<th><tt>a</tt></th>
<td><tt>xe86fe</tt></td>
</tr>
<tr>
<th><tt>c</tt></th>
<td><tt>wt5v4t</tt></td>
</tr>
<tr>
<th><tt>d</tt></th>
<td><tt>4vljgv</tt></td>
</tr>
<tr>
<th><tt>e</tt></th>
<td><tt>ukpcrk</tt></td>
</tr>
<tr>
<th><tt>f</tt></th>
<td><tt>0reszr</tt></td>
</tr>
<tr>
<th><tt>g</tt></th>
<td><tt>a7vy57</tt></td>
</tr>
<tr>
<th><tt>h</tt></th>
<td><tt>k5glc5</tt></td>
</tr>
<tr>
<th><tt>j</tt></th>
<td><tt>7xmfyx</tt></td>
</tr>
<tr>
<th><tt>k</tt></th>
<td><tt>yfatwf</tt></td>
</tr>
<tr>
<th><tt>l</tt></th>
<td><tt>t2ymv2</tt></td>
</tr>
<tr>
<th><tt>m</tt></th>
<td><tt>39zex9</tt></td>
</tr>
<tr>
<th><tt>n</tt></th>
<td><tt>vmwajm</tt></td>
</tr>
<tr>
<th><tt>p</tt></th>
<td><tt>ja45ka</tt></td>
</tr>
<tr>
<th><tt>q</tt></th>
<td><tt>qqqqqq</tt></td>
</tr>
<tr>
<th><tt>r</tt></th>
<td><tt>lwk4nw</tt></td>
</tr>
<tr>
<th><tt>s</tt></th>
<td><tt>n4cgp4</tt></td>
</tr>
<tr>
<th><tt>t</tt></th>
<td><tt>zs638s</tt></td>
</tr>
<tr>
<th><tt>u</tt></th>
<td><tt>5yjwly</tt></td>
</tr>
<tr>
<th><tt>v</tt></th>
<td><tt>832x73</tt></td>
</tr>
<tr>
<th><tt>w</tt></th>
<td><tt>2zf8mz</tt></td>
</tr>
<tr>
<th><tt>x</tt></th>
<td><tt>hu9r0u</tt></td>
</tr>
<tr>
<th><tt>y</tt></th>
<td><tt>60xz20</tt></td>
</tr>
<tr>
<th><tt>z</tt></th>
<td><tt>dnrp9n</tt></td>
</tr>
<tr>
<th><tt>0</tt></th>
<td><tt>clundl</tt></td>
</tr>
<tr>
<th><tt>2</tt></th>
<td><tt>sd093d</tt></td>
</tr>
<tr>
<th><tt>3</tt></th>
<td><tt>pgduhg</tt></td>
</tr>
<tr>
<th><tt>4</tt></th>
<td><tt>m8t7a8</tt></td>
</tr>
<tr>
<th><tt>5</tt></th>
<td><tt>f672t6</tt></td>
</tr>
<tr>
<th><tt>6</tt></th>
<td><tt>rchdsc</tt></td>
</tr>
<tr>
<th><tt>7</tt></th>
<td><tt>eh306h</tt></td>
</tr>
<tr>
<th><tt>8</tt></th>
<td><tt>9pshep</tt></td>
</tr>
<tr>
<th><tt>9</tt></th>
<td><tt>gjnkuj</tt></td>
</tr>
</tbody>
</table>
<br/>
<table summary="The matrix of wisdom embodies the essence of the Goddess of Wisdom, Nayru.">
<caption>The matrix of wisdom</caption>
<tbody>
<tr>
<th></th>
<th><tt>acde</tt></th>
<th><tt>fghj</tt></th>
<th><tt>klmn</tt></th>
<th><tt>pqrs</tt></th>
<th><tt>tuvw</tt></th>
<th><tt>xyz0</tt></th>
<th><tt>2345</tt></th>
<th><tt>6789</tt></th>
</tr>
<tr>
<th><tt>a</tt></th>
<td><tt>q9sy</tt></td>
<td><tt>5420</tt></td>
<td><tt>tzxw</tt></td>
<td><tt>ua7d</tt></td>
<td><tt>kp3n</tt></td>
<td><tt>melj</tt></td>
<td><tt>hvgf</tt></td>
<td><tt>8r6c</tt></td>
</tr>
<tr>
<th><tt>c</tt></th>
<td><tt>9q4p</tt></td>
<td><tt>3s02</tt></td>
<td><tt>w8rt</tt></td>
<td><tt>ecmg</tt></td>
<td><tt>ny5k</tt></td>
<td><tt>7u6h</tt></td>
<td><tt>jfdv</tt></td>
<td><tt>zxla</tt></td>
</tr>
<tr>
<th><tt>d</tt></th>
<td><tt>s4q5</tt></td>
<td><tt>y96l</tt></td>
<td><tt>mjk7</tt></td>
<td><tt>vdwa</tt></td>
<td><tt>x3pr</tt></td>
<td><tt>tf0z</tt></td>
<td><tt>8uce</tt></td>
<td><tt>hn2g</tt></td>
</tr>
<tr>
<th><tt>e</tt></th>
<td><tt>yp5q</tt></td>
<td><tt>s3wt</tt></td>
<td><tt>0xz2</tt></td>
<td><tt>ce6f</tt></td>
<td><tt>j94h</tt></td>
<td><tt>lamk</tt></td>
<td><tt>ngvd</tt></td>
<td><tt>r87u</tt></td>
</tr>
<tr>
<th><tt>f</tt></th>
<td><tt>53ys</tt></td>
<td><tt>qp7m</tt></td>
<td><tt>lkj6</tt></td>
<td><tt>gf2e</tt></td>
<td><tt>z498</tt></td>
<td><tt>0dtx</tt></td>
<td><tt>rcua</tt></td>
<td><tt>nhwv</tt></td>
</tr>
<tr>
<th><tt>g</tt></th>
<td><tt>4s93</tt></td>
<td><tt>pql6</tt></td>
<td><tt>7hnm</tt></td>
<td><tt>fgtc</tt></td>
<td><tt>r5yx</tt></td>
<td><tt>wv28</tt></td>
<td><tt>zeau</tt></td>
<td><tt>jk0d</tt></td>
</tr>
<tr>
<th><tt>h</tt></th>
<td><tt>206w</tt></td>
<td><tt>7lq9</tt></td>
<td><tt>pgvy</tt></td>
<td><tt>kh58</tt></td>
<td><tt>utme</tt></td>
<td><tt>3n4c</tt></td>
<td><tt>axzr</tt></td>
<td><tt>dfsj</tt></td>
</tr>
<tr>
<th><tt>j</tt></th>
<td><tt>02lt</tt></td>
<td><tt>m69q</tt></td>
<td><tt>ydfp</tt></td>
<td><tt>nj3z</tt></td>
<td><tt>ew7u</tt></td>
<td><tt>5ksa</tt></td>
<td><tt>cr8x</tt></td>
<td><tt>gv4h</tt></td>
</tr>
<tr>
<th><tt>k</tt></th>
<td><tt>twm0</tt></td>
<td><tt>l7py</tt></td>
<td><tt>qfd9</tt></td>
<td><tt>hk4x</tt></td>
<td><tt>a26c</tt></td>
<td><tt>sj5e</tt></td>
<td><tt>u8rz</tt></td>
<td><tt>vg3n</tt></td>
</tr>
<tr>
<th><tt>l</tt></th>
<td><tt>z8jx</tt></td>
<td><tt>khgd</tt></td>
<td><tt>fqyv</tt></td>
<td><tt>7lu0</tt></td>
<td><tt>5rn3</tt></td>
<td><tt>emas</tt></td>
<td><tt>4w2t</tt></td>
<td><tt>9pc6</tt></td>
</tr>
<tr>
<th><tt>m</tt></th>
<td><tt>xrkz</tt></td>
<td><tt>jnvf</tt></td>
<td><tt>dyqg</tt></td>
<td><tt>6mct</tt></td>
<td><tt>s8h4</tt></td>
<td><tt>ale5</tt></td>
<td><tt>32w0</tt></td>
<td><tt>p9u7</tt></td>
</tr>
<tr>
<th><tt>n</tt></th>
<td><tt>wt72</tt></td>
<td><tt>6myp</tt></td>
<td><tt>9vgq</tt></td>
<td><tt>jnsr</tt></td>
<td><tt>c0la</tt></td>
<td><tt>4h3u</tt></td>
<td><tt>ezx8</tt></td>
<td><tt>fd5k</tt></td>
</tr>
<tr>
<th><tt>p</tt></th>
<td><tt>uevc</tt></td>
<td><tt>gfkn</tt></td>
<td><tt>h76j</tt></td>
<td><tt>qpz3</tt></td>
<td><tt>2ad0</tt></td>
<td><tt>89rw</tt></td>
<td><tt>ts54</tt></td>
<td><tt>mlxy</tt></td>
</tr>
<tr>
<th><tt>q</tt></th>
<td><tt>acde</tt></td>
<td><tt>fghj</tt></td>
<td><tt>klmn</tt></td>
<td><tt>pqrs</tt></td>
<td><tt>tuvw</tt></td>
<td><tt>xyz0</tt></td>
<td><tt>2345</tt></td>
<td><tt>6789</tt></td>
</tr>
<tr>
<th><tt>r</tt></th>
<td><tt>7mw6</tt></td>
<td><tt>2t53</tt></td>
<td><tt>4ucs</tt></td>
<td><tt>zrqn</tt></td>
<td><tt>gl0d</tt></td>
<td><tt>98pv</tt></td>
<td><tt>fjkh</tt></td>
<td><tt>eayx</tt></td>
</tr>
<tr>
<th><tt>s</tt></th>
<td><tt>dgaf</tt></td>
<td><tt>ec8z</tt></td>
<td><tt>x0tr</tt></td>
<td><tt>3snq</tt></td>
<td><tt>mvu7</tt></td>
<td><tt>k5jl</tt></td>
<td><tt>6p9y</tt></td>
<td><tt>2wh4</tt></td>
</tr>
<tr>
<th><tt>t</tt></th>
<td><tt>knxj</tt></td>
<td><tt>zrue</tt></td>
<td><tt>a5sc</tt></td>
<td><tt>2tgm</tt></td>
<td><tt>qh89</tt></td>
<td><tt>d0fy</tt></td>
<td><tt>p67l</tt></td>
<td><tt>34vw</tt></td>
</tr>
<tr>
<th><tt>u</tt></th>
<td><tt>py39</tt></td>
<td><tt>45tw</tt></td>
<td><tt>2r80</tt></td>
<td><tt>aulv</tt></td>
<td><tt>hqsj</tt></td>
<td><tt>6c7n</tt></td>
<td><tt>kdfg</tt></td>
<td><tt>xzme</tt></td>
</tr>
<tr>
<th><tt>v</tt></th>
<td><tt>35p4</tt></td>
<td><tt>9ym7</tt></td>
<td><tt>6nhl</tt></td>
<td><tt>dv0u</tt></td>
<td><tt>8sqz</tt></td>
<td><tt>2gwr</tt></td>
<td><tt>xaec</tt></td>
<td><tt>kjtf</tt></td>
</tr>
<tr>
<th><tt>w</tt></th>
<td><tt>nkrh</tt></td>
<td><tt>8xeu</tt></td>
<td><tt>c34a</tt></td>
<td><tt>0wd7</tt></td>
<td><tt>9jzq</tt></td>
<td><tt>g2vp</tt></td>
<td><tt>ylm6</tt></td>
<td><tt>5sft</tt></td>
</tr>
<tr>
<th><tt>x</tt></th>
<td><tt>m7tl</tt></td>
<td><tt>0w35</tt></td>
<td><tt>sea4</tt></td>
<td><tt>8x9k</tt></td>
<td><tt>d62g</tt></td>
<td><tt>qzyf</tt></td>
<td><tt>vhnj</tt></td>
<td><tt>ucpr</tt></td>
</tr>
<tr>
<th><tt>y</tt></th>
<td><tt>eufa</tt></td>
<td><tt>dvnk</tt></td>
<td><tt>jmlh</tt></td>
<td><tt>9y85</tt></td>
<td><tt>0cg2</tt></td>
<td><tt>zqxt</tt></td>
<td><tt>w43s</tt></td>
<td><tt>76rp</tt></td>
</tr>
<tr>
<th><tt>z</tt></th>
<td><tt>l60m</tt></td>
<td><tt>t24s</tt></td>
<td><tt>5ae3</tt></td>
<td><tt>rzpj</tt></td>
<td><tt>f7wv</tt></td>
<td><tt>yxqd</tt></td>
<td><tt>gnhk</tt></td>
<td><tt>cu98</tt></td>
</tr>
<tr>
<th><tt>0</tt></th>
<td><tt>jhzk</tt></td>
<td><tt>x8ca</tt></td>
<td><tt>es5u</tt></td>
<td><tt>w0vl</tt></td>
<td><tt>ynrp</tt></td>
<td><tt>ftdq</tt></td>
<td><tt>976m</tt></td>
<td><tt>43g2</tt></td>
</tr>
<tr>
<th><tt>2</tt></th>
<td><tt>hj8n</tt></td>
<td><tt>rzac</tt></td>
<td><tt>u43e</tt></td>
<td><tt>t2f6</tt></td>
<td><tt>pkxy</tt></td>
<td><tt>vwg9</tt></td>
<td><tt>qml7</tt></td>
<td><tt>s5d0</tt></td>
</tr>
<tr>
<th><tt>3</tt></th>
<td><tt>vfug</tt></td>
<td><tt>cexr</tt></td>
<td><tt>8w2z</tt></td>
<td><tt>s3jp</tt></td>
<td><tt>6dal</tt></td>
<td><tt>h4n7</tt></td>
<td><tt>mqy9</tt></td>
<td><tt>t0k5</tt></td>
</tr>
<tr>
<th><tt>4</tt></th>
<td><tt>gdcv</tt></td>
<td><tt>uaz8</tt></td>
<td><tt>r2wx</tt></td>
<td><tt>54k9</tt></td>
<td><tt>7fem</tt></td>
<td><tt>n3h6</tt></td>
<td><tt>lyqp</tt></td>
<td><tt>0tjs</tt></td>
</tr>
<tr>
<th><tt>5</tt></th>
<td><tt>fved</tt></td>
<td><tt>aurx</tt></td>
<td><tt>zt08</tt></td>
<td><tt>45hy</tt></td>
<td><tt>lgc6</tt></td>
<td><tt>jskm</tt></td>
<td><tt>79pq</tt></td>
<td><tt>w2n3</tt></td>
</tr>
<tr>
<th><tt>6</tt></th>
<td><tt>8zhr</tt></td>
<td><tt>njdg</tt></td>
<td><tt>v9pf</tt></td>
<td><tt>m6e2</tt></td>
<td><tt>3xk5</tt></td>
<td><tt>u7c4</tt></td>
<td><tt>st0w</tt></td>
<td><tt>qyal</tt></td>
</tr>
<tr>
<th><tt>7</tt></th>
<td><tt>rxn8</tt></td>
<td><tt>hkfv</tt></td>
<td><tt>gp9d</tt></td>
<td><tt>l7aw</tt></td>
<td><tt>4zjs</tt></td>
<td><tt>c6u3</tt></td>
<td><tt>50t2</tt></td>
<td><tt>yqem</tt></td>
</tr>
<tr>
<th><tt>8</tt></th>
<td><tt>6l27</tt></td>
<td><tt>w0s4</tt></td>
<td><tt>3cu5</tt></td>
<td><tt>x8yh</tt></td>
<td><tt>vmtf</tt></td>
<td><tt>pr9g</tt></td>
<td><tt>dkjn</tt></td>
<td><tt>aeqz</tt></td>
</tr>
<tr>
<th><tt>9</tt></th>
<td><tt>cagu</tt></td>
<td><tt>vdjh</tt></td>
<td><tt>n67k</tt></td>
<td><tt>y9x4</tt></td>
<td><tt>weft</tt></td>
<td><tt>rp82</tt></td>
<td><tt>05s3</tt></td>
<td><tt>lmzq</tt></td>
</tr>
</tbody>
</table>
<br/>
<table summary="The list of courage embodies the essence of the Goddess of Courage, Farore.">
<caption>The list of courage</caption>
<tbody>
<tr>
<th><tt>bc1</tt></th>
<td><tt>rzqrrp</tt></td>
</tr>
<tr>
<th><tt>tb1</tt></th>
<td><tt>z5qrrp</tt></td>
</tr>
</tbody>
</table>
<p>Print out these tables and keep them with your emergency supplies so that you can find them when you need them.
</p><p>Now we can begin.
Split the message <code>BC1SW50QA3JX3S</code> into its prefix, <code>BC1</code>, and suffix <code>SW50QA3JX3S</code>.
Take the suffix and write it vertically on a piece of paper, leaving a gap after each letter and then a line.
</p><pre>S
─────────────
W
─────────────
5
─────────────
0
─────────────
Q
─────────────
A
─────────────
3
─────────────
J
─────────────
X
─────────────
3
─────────────
S
─────────────</pre>
<p>Find the prefix in the list of courage and write the associated word after the first letter, <tt>S</tt>, placing a diagonal line between each letter.
For new prefixes, you may need to add them to the list of courage beforehand.
</p><pre>S\r\z\q\r\r\p
─────────────
W</pre>
<p>Take the last letter, which is <tt>p</tt>, and look it up in the table of power to find its associated word, which is <tt>ja45ka</tt>.
Write this word in the gap under the <tt>Srzqrrp</tt>, extending the diagonal lines between each letter.
</p><pre>S\r\z\q\r\r\p
\j\a\4\5\k\a\
─────────────
W</pre>
<p>For each letter of this power word, we need to use the matrix of wisdom to add it to the letter above and to the left of it.
For example, we look up row <tt>S</tt> and column <tt>j</tt> in the matrix of wisdom and we find the letter <tt>z</tt>. Write <tt>z</tt> after the <tt>W</tt> below the line, separating it with a diagonal line again.
</p><pre>S\r\z\q\r\r\p
\j\a\4\5\k\a\
─────────────
W\z</pre>
<p>We look up row <tt>r</tt> and column <tt>a</tt> in the matrix of wisom to find the number <tt>7</tt>. We add <tt>7</tt> after the <tt>z</tt>, and keep doing this until every pair of letters is done. The matrix of wisdom is symmetric, so you do not have to worry about whether you are looking up by row/column or column/row.
</p><pre>S\r\z\q\r\r\p
\j\a\4\5\k\a\
─────────────
W\z\7\h\5\4\7</pre>
<p>We repeat this process with the next line. First we lookup <tt>7</tt> in the table of power to find <tt>eh306h</tt> and write it underneath.
</p><pre>W\z\7\h\5\4\7
\e\h\3\0\6\h\
─────────────
5</pre>
<p>Then, for each pair of letters, we add them using the matrix of wisdom.
</p><pre>W\z\7\h\5\4\7
\e\h\3\0\6\h\
─────────────
5\h\4\0\c\w\z</pre>
<p>We keep doing this until we go through all the letters of the suffix.
</p><pre>S\r\z\q\r\r\p
\j\a\4\5\k\a\
─────────────
W\z\7\h\5\4\7
\e\h\3\0\6\h\
─────────────
5\h\4\0\c\w\z
\d\n\r\p\9\n\
─────────────
0\e\y\k\w\a\a
\x\e\8\6\f\e\
─────────────
Q\f\q\r\v\8\y
\6\0\x\z\2\0\
─────────────
A\6\x\x\p\x\g
\a\7\v\y\5\7\
─────────────
3\q\y\2\z\4\c
\w\t\5\v\4\t\
─────────────
J\l\t\s\x\h\7
\e\h\3\0\6\h\
─────────────
X\t\g\6\l\u\q
\q\q\q\q\q\q\
─────────────
3\x\t\g\6\l\u
\5\y\j\w\l\y\
─────────────
S\9\z\e\x\9\m
\3\9\z\e\x\9\
─────────────
\p\q\q\q\q\q</pre>
<p>The final result should be <tt>pqqqqq</tt>, where <tt>q</tt> is the most powerful letter and <tt>p</tt> is the wisest letter.
If you did not get this result, start over from the beginning because you probably made a mistake.
Remember to mind your <tt>p</tt>'s and <tt>q</tt>'s.
</p><p>After a couple years of practice doing this by hand, the operations become natural.
For example, you learn that <tt>x</tt> and <tt>y</tt> equals <tt>z</tt>, and so forth.
</p><p>Exercise for the reader: Create a variant of this procedure for computing Bech32 checksums.
</p><p>P.S. This article is not meant to be taken seriously.
</p>http://r6.ca/blog/20171010T001746Z.htmlFunctor-Oriented Programming2017-10-10T00:17:46Z2017-10-10T00:17:46Z
<p>My style of Haskell programming has been evolving over the 15 years that I have been working with it.
It is turning into something that I would like to call “functor oriented programming”.
The traditional use of typed functional programming focuses on data types.
One defines data types to model the data structures that your program operates on, and one writes functions to transform between these structures.
One of the primary goals in this traditional methodology is to create data structures that exclude erroneous states to the extent that is reasonably possible.
As long as one ensures that pattern matching is complete, then the type system catches many errors that would otherwise lead to these erroneous states, which have been crafted to be unrepresentable.
</p><p>Functor oriented programming is a refinement of this traditional focus on data types.
I was reminded of this concept recently when I was working with <a title="unification-fd: Simple generic unification algorithms." href="https://hackage.haskell.org/package/unification-fd">wren’s fantastic unification-fd library</a>.
With functor oriented programming, one divides data structures into layers of functors that, when composed together, form the data structures that your program operates on.
Instead of writing transformations between data structures, one writes natural transformations between functors, where a natural transformation between functors <code>F</code> and <code>G</code> is a polymorphic function of type <code>forall a. F a -> G a</code>.
While traditional functions often operate on products of multiple inputs and/or outputs, with functor oriented programming one will often see functions operating on compositions of functors, including but not limited to distribution functions of type <code>forall a. F (G a) -> G (F a)</code> and half-way distribution functions <code>forall a. F (G a) -> G (H a)</code>, and many others.
</p><p>By dividing data structures up into layers of functors, one can create a separation of concerns that does not occur in traditional functional programming.
With functor oriented programming, polymorphism is not necessarily about using functions polymorphically.
Instead, polymorphism provides correctness guarantees by ensuring that a particular function can only touch the specific layers of functors in its type signature and is independent of the rest of the data structure.
<strong>One benefits from polymorphism even when a function is only ever invoked at a single type.</strong>
</p><p>The appearance of many natural transformations is one hallmark of functor oriented programming.
Higher-order natural transformations will invoke <code>Rank2Types</code> and <code>RankNTypes</code>, which is another hallmark of functor oriented programming.
Other hallmarks of functor oriented programming include open recursive types, which allows one to divide up recursive types into their layers of recursion and create natural transformations that operate on a single layer at a time.
Open recursive types plays an important role in wren’s unification library.
</p><p>As fine of a language that Haskell is, it is not actually that suitable for functor oriented programming.
The problem is that, under normal circumstances, there is no reduction or equivalence classes at the type level.
For example, the identity functor does not transparently disappear during composition, the <code>Compose</code> functor is not transparently associative, and the <code>Swap</code> functor composed with itself does not reduce to the identity functor.
To cope with this one must litter one’s code with <code>newtype</code> wrapper and unwrappers to make all these natural transformations explicit.
In principle, these transformations should have no run-time consequences, but when they are used in higher-order ways, unfortunately they sometimes do.
Despite the problems, I am not aware of any another practical language that better supports this style of programming.
I think Haskell’s higher-kinded type classes and the progression of <code>Monad</code>, <code>Applicative</code>, <code>Foldable</code>, <code>Traversable</code>, etc. classes have been instrumental in leading to the development of this style of programming as they further motivate the division of one’s data structures into these layers of functors.
</p><p>I have been thinking about writing this post for a few years now, and wanted to write something convincing; however, I do not think I am up to the task.
Instead of trying to persuade the reader, I have elected to try to simply name and describe this style of programming so that the reader might notice it themselves when reading and writing code.
Hopefully someone more capable than me can evangelize this approach, and perhaps even create a practical language suitable for this style of programming.
</p>http://r6.ca/blog/20171008T222703Z.htmlTaking Propositions as Types Seriously2017-10-08T22:27:03Z2017-10-08T22:27:03Z
<p>A while back I decided to try my hand at using <a title="The Agda Wiki" href="http://wiki.portal.chalmers.se/agda/pmwiki.php">Agda</a> and I wrote a proof of the <a title="roconnor's STLC :: hub.darcs.net" href="https://hub.darcs.net/roconnor/STLC">Church-Rosser theorem</a> in it.
It was a fun exercise.
I took all the knowledge I have picked up over the years about using dependent types to represent binders, to define well-typed terms, and what I have learned about the <a title="Categorical Logic and Type Theory" href="https://people.mpi-sws.org/~dreyer/courses/catlogic/jacobs.pdf">Category of Contexts</a> and applied it to <a title="Terms.agda :: hub.darcs.net" href="https://hub.darcs.net/roconnor/STLC/browse/src/STLC/Terms.agda">my definition of Terms for a simply typed lambda calculus</a>.
I am proud of the result.
</p><p>They say you do not understand a topic in mathematics until you can teach it.
And you do not really understand it until you can prove it in Coq.
And you do not really <em>really</em> understand it until you can prove it in Agda.
What really struck me was how my exercise in Adga affected my understanding of “Propositions as Types”.
</p><p>I view types as being divided into roughly two categories.
Some types are propositions.
They are the types that have at most one inhabitant, which is to say types for which you can prove that all their inhabitants are equal.
Other types are data types.
They are types with potentially more than one inhabitant.
As such you can distinguish between values by (possibly indirectly) doing case analysis on them.
Indeed, <a title="Homotopy Type Theory" href="https://homotopytypetheory.org/">HoTT</a> defines propositions in exactly this way.
</p><p>This classification of types is not fundamental in the theory of types.
The theory of types treats both propositions and data types uniformly.
I simply find it a useful way of characterizing types when programming and reasoning about programs with dependent type theory.
The void and unit types, ⊥ and ⊤ respectively, are both propositions.
We can define a function from the Boolean type to the universe of types which map the two Boolean values to these two types.
In this way we can covert any Boolean valued (computable) predicate into a logical (type-theoretical) predicate.
</p><p>To me the phrase “Proposition as Types” just meant the embedding of logical proposition as types with at most one inhabitant.
For example, given a decidable type <var>A</var>, we can compute if a given value of type <var>A</var> is a member of a given list of <var>A</var>s.
This computable predicate can be lifted to a logical predicate to define a logical membership relationship.
Expressions using this logical membership relationship are propositions according to the above definition of proposition.
</p><p>This is a fine way to do formal reasoning.
However, this is not the way that membership is typically defined in Agda.
Instead, Agda defines the membership relation as an inductive family whose constructors witness that an element is either the head of the list, or is a member of the tail of the list.
(Coq also defines the membership relation this way; however it is marked as non-extractable for computation by virtue of being a proposition.)
The type (<var>a</var> ∈ <var>l</var>) is, in general, a data type rather than a proposition.
When the value <var>a</var> occurs multiple times in <var>l</var>, then the type (<var>a</var> ∈ <var>l</var>) has multiple different “proofs” corresponding the the different occurrences of <var>a</var> within <var>l</var>.
Values of this type act as “the type of indexes where <var>a</var> occurs in <var>l</var>”, and one can write programs that operate over this type.
</p><p>Given two lists, <var>l</var><sub>1</sub> and <var>l</var><sub>2</sub>, the “proposition” that one list is a subset of the other states that any element of <var>l</var><sub>1</sub> is also an element of <var>l</var><sub>2</sub>:
</p><p><var>l</var><sub>1</sub> ⊆ <var>l</var><sub>2</sub> ≔ ∀<var>a</var>. <var>a</var>∈<var>l</var><sub>1</sub> → <var>a</var>∈<var>l</var><sub>2</sub>
</p><p>In dependent type theory this implication is represented as a function.
Because our membership relation is a data type, this subset relation is represented by a real program.
Specifically it is a program that, for any value, maps each index where it occurs in <var>l</var><sub>1</sub> to some index where it occurs in <var>l</var><sub>2</sub>; you can really evaluate this function.
This subset type is also, in general, a data type because there can be multiple such functions, which represent all the possible permutations that maps <var>l</var><sub>1</sub> onto <var>l</var><sub>2</sub>.
</p><p>The consequences of this are fantastic.
For example, what you normally think of as a theorem for weakening,
</p><pre>weaken : ∀ {Γ₁ Γ₂ A} → Γ₁ ⊆ Γ₂ → Term Γ₁ A → Term Γ₂ A</pre>
<p>also captures contraction and exchange due to this definition of subset.
All the <a title="Structural rule" href="https://en.wikipedia.org/w/index.php?title=Structural_rule&oldid=736195870">structural rules</a> of the lambda calculus are subsumed within a single theorem!
</p><p>It took me several attempts before I learned to take full advantage of this sort of logic.
For example, I originally defined a module as an inductive family.
However, I eventually settled on a functional representation for modules:
</p><pre>-- A Module is a list of terms of types Δ all in the same context Γ.
-- A Module is a block of terms for simultaneous substitution.
-- A Module is an arrow in the category of contexts.
-- A Module is a profuctor.
Module : List Type → List Type → Set
Module Γ Δ = ∀ {A} → A ∈ Δ → Term Γ A</pre>
<p>This definition means a module can evaluate.
In particular modules can be partially evaluated during type-checking, which greatly simplified many of my proofs as compared to using the inductive family way of defining modules.
</p><p>Notice how we make use of values of <code>A ∈ Δ</code> as data defining an index into the context <code>Δ</code>.
If <code>Δ</code> has multiple occurrences of <code>A</code>, then the term generated by the module can be different depending on which occurrence the index is referencing.
</p><p>In conclusion, although I do like thinking of types as divided between propositional types and data types, it can be fruitful to view expressions that mathematics traditionally treats as propositions instead as real data types, and really program with them.
This is what I mean by taking "Propositions as Types" seriously.
</p>http://r6.ca/blog/20170616T114546Z.htmlSome Random Thoughts of an Advanced Haskeller2017-06-16T11:45:46Z2017-06-16T11:45:46Z
<p>Recently I was thinking about a programming problem that would need access to random values.
I thought it might be fun to write up my though process as an advanced Haskeller while working through this particular problem.
</p><p>In Haskell, one would write such a program by using a random monad to access an oracle providing random numbers.
The traditional way to implement <code>MonadRandom</code> is using the state monad.
The <code>Gen</code> type holds the state of the (pseudo-)random number generator, and the <code>randomInt</code> function returns a new random number and updates the state of the generator.
</p><pre>type Random a = State Gen a
randomInt :: Gen -> (Int,Gen)
randomOracle :: MonadRandom Int
randomOracle = state random</pre>
<p>Then I write my program inside the Random monad, making calls to the <code>randomOracle</code> as needed
</p><pre>myProg :: Random Result
myProg = do
{- ... -}
x <- randomOracle
{- ... -}
y <- randomOracle
{- ... -}</pre>
<p>In order to run my program, I need to provide it with a random seed.
</p><pre>evalRandom :: Random result -> Gen -> result
evalRandom = evalState</pre>
<p>For deterministic testing, we can pass fixed generators to <code>evalRandom</code>.
If we use <code>StdGen</code>, we can map our <code>Random</code> program to <code>IO</code> and use the system random number generator.
</p><pre>type Gen = System.Random.StdGen
randomInt = System.Random.random
evalRandomIO :: Random result -> IO result
evalRandomIO = getStdRandom . runState</pre>
<p>For the most general possible random number generator, the type for the generator state is simply an infinite stream of random values.
</p><pre>data Stream a = Cons a (Stream a)
unfoldStream :: (g -> (a, g)) -> g -> Stream a
unfoldStream next = go
where
go seed = Cons value (go nextSeed)
where
(value, nextSeed) = next seed
type Gen = Stream Int
randomInt (Cons hd tl) = (hd, tl)
evalRandomStdGen :: Random result -> StdGen -> result
evalRandomStdGen rr = evalRandom rr . unfoldStream System.Random.random
evalRandomIO :: Random result -> IO result
evalRandomIO rr = evalRandomStdGen rr <$> newStdGen</pre>
<p>Before, when I was an intermediate Haskeller, I would probably stop at this point pretty satisfied with this.
And let me be clear that this is a fine solution.
However, now that I am an advanced Haskeller, I cannot help but feel a little dissatisfied with this solution.
The problem with this implementation of the <code>Random</code> monad is that the type is too broad.
Since the <code>Random</code> type is the <code>State</code> monad, there are operations allowed by the type that should not be allowed for a <code>Random</code> program.
For instance, within the <code>Random</code> type, someone could store the state of the generator and restore it later causing random values to be replayed, or someone might completely replace the state of the generator with their own value.
</p><p>One way to solve this problem is to use Haskell’s module system to abstract the monad and only expose the <code>randomOracle</code> operation.
While this is a reasonable solution (in fact it is a very good solution as we will see), it would be nicer if we could instead use the type system to create a monad that is only capable of representing the programs we want to allow, and disallows other programs that would try manipulate the generator state in ways we do not want.
Essentially we want our <code>Random</code> programs to only be able to query the random oracle, and that is it.
After reflecting on this problem and the various kinds of monads I know about, I realized that the a suitable free monad captures exactly this notion of providing only an operation to query the random oracle.
Specifically we want <code>Control.Monad.Free.Free (Reader Int)</code> or more directly (but more obtusely written) as <code>Control.Monad.Free.Free ((->) Int)</code>.
We truly want a free monad because any sequence of responses from the random oracle is valid.
</p><p>One problem with this <code>Free</code> monad is that the bind operation can be slow because it needs to traverse through a, possibly long, data structure.
There are several solutions to this, but for this particular free monad, I happen to know that the <a title="van Laarhoven Free Monad" href="20140210T181244Z.html">Van Laarhoven free monad representation</a> is possible:
The type <code>forall m. Monad m => m Int -> m a</code> is isomorphic to <code>Control.Monad.Free.Free ((->) Int) a</code>.
</p><pre>newtype Random a = Random { instantiateRandom :: forall m. Monad m => m Int -> m a }
instance Monad Random where
return a = Random $ \_ -> return a
ma >>= mf = Random . runReaderT
$ ReaderT (instantiateRandom ma) >>= ReaderT . instantiateRandom . mf
instance Applicative Random where
pure = return
(<*>) = ap
instance Functor Random where
fmap = liftM</pre>
<p>In this representation, the random oracle function just fetches the argument.
</p><pre>randomOracle :: Random Int
randomOracle = Random id</pre>
<p>For deterministic testing purposes we can evaluate the random monad by instantiating it with our state monad from before.
</p><pre>evalRandom :: Random result -> Stream Int -> result
evalRandom rr = evalState . instantiateRandom rr . state $ \(Cons hd tl) -> (hd, tl)</pre>
<p>However, we can also directly instantiate it with the <code>IO</code> monad for production purposes.
</p><pre>evalRandomIO :: Random result -> IO result
evalRandomIO rr = instantiateRandom rr evalRandomIO</pre>
<p>This is all very good; however, the advanced Haskeller in me still thinks that I ought to be able to write <code>evalRandom</code> without the need to invoke the <code>State</code> monad.
This is because if we were actually using the <code>Free ((->) Int</code> monad, I would be writing <code>evalRandom</code> using <code>iterA</code>.
</p><pre>iterA :: (Applicative p, Functor f) => (f (p a) -> p a) -> Free f a -> p a
evalFreeRandom :: Free ((->) Int) result -> Stream Int -> result
evalFreeRandom = iterA (\fpa (Cons hd tl) -> fpa hd tl)</pre>
<p>No need for any state monad business in <code>evalFreeRandom</code>.
How can I get that elegant solution with the Van Laarhoven free monad?
One way would be to convert to the <code>Free ((->) Int)</code> representation
</p><pre>freeRandom :: Random result -> Free ((->) Int) result
freeRandom rr = instantiateRandom rr (liftF id)
evalRandom :: Random result -> Stream Int -> result
evalRandom = evalFreeRandom . freeRandom</pre>
<p>Surely there must be a way to do this directly?
</p><p>Before solving this I turned to another interesting problem.
The <code>iterA</code> function recurses over the free monad structure to do its evaluation.
The <code>Free</code> monad comes with its own general recursive elimination function called <code>foldFree</code>
</p><pre>foldFree :: Monad m => (forall x. f x -> m x) -> Free f a -> m a</pre>
<p>This <code>foldFree</code> function is captures everything about the free monad, so it should be possible to write <code>iterA</code> by using <code>foldFree</code> to do all the recursion.
But how is that even possible?
The types of <code>foldFree</code> and <code>iterA</code> look too far apart.
<code>foldFree</code> requires an natural transformation as input, and the arguments to <code>iterA</code> provide nothing resembling that.
</p><p>To solve this I turned to the <kbd>#haskell</kbd> IRC channel for help.
With assistance from glguy, ReinH, and byorgey, I turned the well known idea that if you want turn something to or from a natural transformation you use some sort of Yoneda / continuation like construction.
In this particular case, the <code>Cont (p a)</code> monad seems to capture what we need.
Following the types (and forgetting about the semantics) we end up the following.
</p><pre>iterA :: (Applicative p, Functor f) => (f (p a) -> p a) -> Free f a -> p a
iterA h ff = runCont (foldFree (\fx -> Cont $ \k -> h (k <$> fx)) ff) pure</pre>
<p>As an aside, <a title="myIterA" href="http://lpaste.net/356001">glguy has a more “natural” solution</a>, but it technically has a less general type, so I will not talk about here, even if I do feel it is better.
</p><p>Turning back to our original problem of directly writing <code>evalRandom</code> without using the state monad, we can try to see if <code>Cont</code> will solve our problem.
</p><pre>evalRandom :: Random result -> Stream Int -> result
evalRandom rr = runCont (instantiateRandom rr (Cont $ \k (Cons hd tl) -> k hd tl)) const</pre>
<p>We can compare the <code>Cont</code> solution to the <code>State</code> solution and see that the code is pretty similar.
</p><pre>evalRandom :: Random result -> Stream Int -> result
evalRandom rr = evalState (instantiateRandom rr (state $ \(Cons hd tl) -> (hd, tl)))</pre>
<p>The inner <code>Cont</code> construction looks very similar to the inner <code>state</code> construction.
The outer call to <code>const</code> in the <code>Cont</code> solution discards the final "state" which captures the same functionality that <code>evalState</code> has for the <code>State</code> solution.
Now we can ask, which has better performance, the <code>State</code> solution, with its tupling and untupling of values, or the <code>Cont</code> solution which uses continuations instead?
I will leave it to the GHC experts to figure that one out.
</p><p>Arguably most of this is an exercise in academics, but it only took me a hour or three to go through this whole thought process.
As an advanced Haskeller, I have slowly gathered, over many years, experience with these sorts of abstractions so that it starts becoming easy to do this sort of reasoning.
While it may or may not matter much for my particular application, eventually this kind of reasoning becomes important.
For example, the modern stream fusion in GHC exploits constructions that resemble this kind of reasoning, and that has had a big impact on performance.
</p><p>For the non-advanced Haskellers out there, do not be deterred.
Keep practicing your craft; keep reading about new abstractions, even if you do not fully get it; keep looking out for potential applications of those abstractions to solidify your understanding.
Eventually you will have lots of very powerful problem solving tools at your disposal for making safe software.
</p>http://r6.ca/blog/20151210T033709Z.htmlBell’s Casino Solution2015-12-10T03:37:09Z2015-12-10T03:37:09Z
<blockquote>
<p><a href="20150816T185621Z.html">Bell’s Casino Problem</a></p>
<p>A new casino has opened up in town named “Bell’s Casino”. They are offering a coin game. The game works as follows.
</p>
<p>The house will commit two coins on the table, oriented heads or tails each, and keep them covered. The player calls what the faces of the each of the coins are, either HH, HT, TH, or TT. The
casino reveals the coins and if the player is correct, they win $1, and otherwise they lose $1.
</p>
<dl>
<dt>Problem 1.</dt>
<dd>Prove that there is no strategy that can beat the casino.</dd>
</dl>
</blockquote>
<p>Solution to problem 1.
</p><p>Let <var>p</var><sub>HH</sub> be the probability that the casino orients the coins as HH, and similarly for <var>p</var><sub>HT</sub>, <var>p</var><sub>TH</sub>, and <var>p</var><sub>TT</sub>.
We have <var>p</var><sub>HH</sub> + <var>p</var><sub>HT</sub> + <var>p</var><sub>TH</sub> + <var>p</var><sub>TT</sub> = 1.
If the player calls the orientations <var>X</var><var>Y</var>, the they win $1 with probability <var>p</var><sub><var>X</var><var>Y</var></sub>, and lose $1 with probability 1-<var>p</var><sub><var>X</var><var>Y</var></sub>.
This means the total expected value is 2*<var>p</var><sub><var>X</var><var>Y</var></sub> - 1 dollars.
The casino can minimize the players expected value by choosing each of the four possible orientations with equal proability of 25%.
In the case the players expected value is $-0.50 no matter what orientation they choose to call.
</p><blockquote>
<p>After opening the customers stop coming by to play this boring game, so to boost attendance the casino modifies the game as follows.
</p>
<p>The house will commit two coins on the table, oriented heads or tails each, and keep them covered. The player calls what the faces of each of the two coins are, either HH, HT, TH, or TT. The
casino reveals one coin, of the players choice. After seeing revealed coin, the player can elect to back out of the game and neither win nor lose, or keep going, and see the second coin.
If the player’s call is correct, they win $1, and otherwise they lose $1.
</p>
<dl>
<dt>Problem 2.</dt>
<dd>Prove that there is no strategy that can beat the casino.</dd>
</dl>
</blockquote>
<p>Solution to problem 2.</p><p>Without loss of generality, suppose the player calls HH and they ask for the first coin to be revealed.
With probability <var>p</var><sub>TH</sub> + <var>p</var><sub>TT</sub> the first coin is tails.
At this point the player’s best option is to elect to back out of the game as it is now impossible for them to win.
With probability <var>p</var><sub>HH</sub> + <var>p</var><sub>HT</sub> the first coin is heads.
At this point the player can back out or continue.
If the player always continues then they win $1 with probability <var>p</var><sub>HH</sub> and they lose $1 with probability <var>p</var><sub>HT</sub>.
Their total expected value is <var>p</var><sub>HH</sub> - <var>p</var><sub>HT</sub> dollars.
As before, the casino can choose each of the four possible orientations with equal proability of 25%.
In the case the players expected value is $0 if they chose to continue if the revealed coin is correct, and it is also $0 if they chose to always back out of the game.
No matter what strategy the player chooses, they cannot beat the casino as long as the casino chooses each of the four possible orientations with equal proability.
</p><blockquote>
<p>Even with the new, more fair, game, attendance at the casino starts dropping off again. The casino decides to offer a couples game.
</p>
<p>The house will commit two coins on two tables, oriented heads or tails each, and keep them covered. The couple, together, calls what the the faces of each of the two coins are, either HH, HT, TH, or
TT. Then, each player in the couple gets to see one coin each. Collectively they get to decide whether they are going to back out of the game or not by the following method. After seeing
their revealed coin, each player will raise either a black flag or a red flag. If both players raise the different colour flags, the game ends and no one wins or loses. If both players raise the
same colour flag, the game keeps going. If the couples original call was right, they win $1, and otherwise, they lose $1. To ensure that the couple cannot cheat, the two tables
are places far enough apart such that each player’s decision on which flag to raise is <a title="Space-like interval" href="https://en.wikipedia.org/wiki/Spacetime#Space-like_interval">space-like separated</a>. Specifically the tables are placed 179 875 475 km apart and
each player has 1 minute to decide which flag to raise otherwise a black flag will be raised on their behalf (or, more realistically, the tables are placed 400 m apart and each player has
100 nanoseconds to decide which flag to raise).
</p>
<dl>
<dt>Problem 3.</dt>
<dd>Prove that there is no strategy for the couple that can beat the casino.</dd>
</dl>
</blockquote>
<p>Solution to problem 3.
</p><p>Alice and Bob enter the casino together.
The casino covers two coins, and Alice and Bob call a random choice for the orientation of the coins.
Without loss of generality let us assume they call HH.
</p><p>Alice and Bob are separated by 179,875,475 km so they cannot communicate and simutaneously each of them see the value of one of the coins.
If Alice sees heads on her coin, she can raise a black flag with probability <var>a</var>, and a red flag with probability 1-<var>a</var>.
If she sees tails she can raise a black flag with probability <var>b</var>, and a red flag with probability 1-<var>b</var>.
The pair (<var>a</var>, <var>b</var>) characterizes any strategy that Alice could employ.
Similarly, if Bob sees heads on his coin can raise a black flag with probability <var>c</var>, and a red flag with probability 1-<var>c</var>,
and if he sees tails he can raise a black flag with probability <var>d</var>, and a red flag with probability (1-<var>d</var>).
So the quadruple (<var>a</var>,<var>b</var>,<var>c</var>,<var>d</var>) parameterizes all possible strategies that Alice and Bob can employ together.
</p><p>Given the strategy parameterized by (<var>a</var>,<var>b</var>,<var>c</var>,<var>d</var>) they win $1 if they raise the same colour flag if the coins are both heads.
The probability of this happening is <var>a</var><var>c</var> + (1-<var>a</var>)(1-<var>c</var>).
They lose $1 if they raise the same colour flag if any of the coins are tails.
The probability of that happening is <var>b</var><var>c</var> + (1-<var>b</var>)(1-<var>c</var>), <var>a</var><var>d</var> + (1-<var>a</var>)(1-<var>d</var>), <var>b</var><var>d</var> + (1-<var>b</var>)(1-<var>d</var>)
if only the first coin is tails, or if the second coin is tails, or if both coins are tails, respectively.
If the casino chooses the coins orientations with equal proability, their total expected winnings with their strategy is
</p><p><var>E</var> = (<var>a</var><var>c</var> + (1-<var>a</var>)(1-<var>c</var>) - <var>b</var><var>c</var> - (1-<var>b</var>)(1-<var>c</var>) - <var>a</var><var>d</var> - (1-<var>a</var>)(1-<var>d</var>) - <var>b</var><var>d</var> - (1-<var>b</var>)(1-<var>d</var>))/4.
</p><p>Theorem. If 0 ≤ <var>a</var> ≤ 1, 0 ≤ <var>b</var> ≤ 1, 0 ≤ <var>c</var> ≤ 1, 0 ≤ <var>d</var> ≤ 1, and we
let <var>E</var> = (<var>a</var><var>c</var> + (1-<var>a</var>)(1-<var>c</var>) - <var>b</var><var>c</var> - (1-<var>b</var>)(1-<var>c</var>) - <var>a</var><var>d</var> - (1-<var>a</var>)(1-<var>d</var>) - <var>b</var><var>d</var> - (1-<var>b</var>)(1-<var>d</var>))/4,
then <var>E</var> ≤ 0.
</p><p><a href="data:text/plain;base64,UmVxdWlyZSBJbXBvcnQgUHNhdHouDQpSZXF1aXJlIEltcG9ydCBSZWFscy4NCg0KT3BlbiBTY29wZSBSLg0KDQpHb2FsIGZvcmFsbCBhIGIgYyBkOlIsIDAgPD0gYSA8PSAxIC0%2BIDAgPD0gYiA8PSAxIC0%2BIDAgPD0gYyA8PSAxIC0%2BIDAgPD0gZCA8PSAxIC0%2BDQogIChhKmMgKyAoMS1hKSooMS1jKSAtIGIqYyAtICgxLWIpKigxLWMpIC0gYSpkIC0gKDEtYSkqKDEtZCkgLSBiKmQgLSAoMS1iKSooMS1kKSkvNCA8PSAwLg0KUHJvb2YuDQppbnRyb3MuDQphcHBseSAoUm11bHRfbGVfcmVnX2wgNCk7IFtscmF8XS4NCnVuZm9sZCBSZGl2Lg0KcmV3cml0ZSA8LSBSbXVsdF9hc3NvYy4NCnJld3JpdGUgUmludl9yX3NpbXBsX207IFt8bHJhXS4NCnBzYXR6IFIuDQpRZWQuDQo%3D">Proof by positivstellensatz</a>
</p><p>Let <var>G</var> = <var>b</var><var>c</var><var>d</var> + (1-<var>b</var>)(1-<var>c</var>)(1-<var>d</var>)
+ <var>a</var><var>b</var><var>d</var> + (1-<var>a</var>)(1-<var>b</var>)(1-<var>d</var>)
+ <var>a</var>(1-<var>c</var>)<var>d</var> + (1-<var>a</var>)<var>c</var>(1-<var>d</var>)
+ <var>a</var>(1-<var>b</var>)(1-<var>c</var>) + (1-<var>a</var>)<var>b</var><var>c</var>.
0 ≤ <var>G</var> because <var>G</var> is the sum of products of non-negative numbers.
But <var>E</var> = -<var>G</var>/4, so <var>E</var> ≤ 0.
QED.
</p><p>Thus no matter what strategy Alice and Bob use, they cannot expect to beat the casino.
At least that is what the casino thinks.
</p><blockquote>
<dl>
<dt>Problem 4.</dt>
<dd>Devise a physical procedure that a couple can follow to beat the casino on average at this last game without cheating.</dd>
</dl>
</blockquote>
<p>Solution to problem 4.</p><p>Alice and Bob enter the casino together.
Each of them have one of a pair of maximally entangled qbits.
For concreteness let say they are a pair of entangled photons, even though realistically they will use a different physical realization of their qbits.
</p><p>The casino covers two coins, and Alice and Bob call a random choice for the orientation of the coins.
Without loss of generality assume they call HH.
Currently they only have a 25% chance of being right. In order to shift the odds in their favour they need to substantially increase their odds of
dropping out of the game if they are wrong, but avoid dropping out if they are right.
</p><p>Alice and Bob are separated by 179,875,475 km so they cannot communicate and simutaneously each of them see the value of one of the coins.
Alice follows the following procedure.
If she see an H, she measures the polarization of her qbit at an angle of 0°.
If she sees a T, she measures the polarization of her qbit at an angle of -45°.
In either case, if her measurement is positive she raises a black flag and if her measurement is negative she raises a red flag.
In both cases she has a 50% chance of raising either flag.
</p><p>Bob follows the following procedure.
If he sees an H, he measures the polarization of his qbit at an angle of +22.5°.
If he sees a T, he measures the polarization of his qbit at an angle of +67.5°.
In either case, if his measurement is positive he raises a black flag and if his measurement is negative he raises a red flag.
In either case he has a 50% chance of raising either flag.
</p><p>Because their qbits are entangled, the flags they raise are correlated.
The probability of Alice and Bob raising the same colour flag is cos²(<var>θ</var>), where <var>θ</var> is the difference between their measurement angles.
</p><p>If both coins are heads, then the difference between their measurement angle is 22.5°, and the probability of them raising the same colour flag is
cos²(22.5°) = (2 + √2)/4 ≅ 85.4%.
</p><p>If one coin is heads and the other is tails, then the difference between their measurement angle is 67.5°, and the probability of them raising the same colour flag is
cos²(67.5°) = (2 - √2)/4 ≅ 14.6%.
</p><p>If both coins are tails, then the difference between their measurement angle is 112.5°, and the probability of them raising the same colour flag is
cos²(112.5°) = (2 - √2)/4 ≅ 14.6%.
</p><p>If the casino randomly selects the orientation of their coins with equal probability then Alice and Bob’s expected winnings is
((√2 + 2) - 3*(2 - √2))/16 ≅ $0.103, which is a positive amount.
</p><blockquote>
<p>The casino cannot figure out how they keep losing money on this game and, soon, Bell’s Casino goes bankrupt.</p>
</blockquote>
<p>This physical property that allows Alice and Bob to correlate their flags without communicating is called <dfn>quantum pseudo-telepathy</dfn>.
What surprised me the most is that Bob measurements are not quite aligned with Alice’ measurments.
I would have thought it was better that for Bob to measure at angles 0° and +45°.
</p><div class="figure"><img alt="graph of (cos²(θ) - 2×cos²(θ+45°) - cos²(θ+90°))/4" src="images/988c6064f2b5adf014bef7324c7ab700405aaec9ea2d5334d42d53e9ede06aee.svg"/><br/>Graph of expected value vs angle of Bob’s measurements.</div>
<p>If Bob measures at these angles then when the coins are HH, they are guarenteed to raise the same flag, and when the coins are TT, they are guarenteed to raise opposite flags, which is perfect.
However, when one is tails and one is heads, then they have a 50% chance of raising the same flag.
This makes their expected value 0.25*1 - 0.5*0.5 = $0, and they do not come out ahead.
But by having Bob rotate his measurements by a small amount, Bob can increase the chances of raising the different flags in case of HT or TH, while decreasing the chances of correctly staying or leaving the game in case of HH or TT.
Because of the geometry of the circle, Bob increases the chances of raising different flags in case of HT or TH faster than he decreases the chances of raising the correct flags in case of HH or TT.
If Bob makes measurements at angle φ and φ + 45°, then the optimal expected value occurs at φ = 22.5°.
</p>http://r6.ca/blog/20151116T042026Z.htmlStochastic Elections Canada 2015 Results2015-11-16T04:20:26Z2015-11-16T04:20:26Z
<p>It is time to announce the results from Stochastic Elections Canada for the 42<sup>st</sup> General Election.</p><p>Every vote counts with the <a href="20040603T005300Z.html">stochastic election process</a>, so we had to wait until all election results were validated and <a href="http://enr.elections.ca/JudicialRecount_e.aspx">certified</a> before we could announce our results.
However, stochastic election results are not very sensitive to small changes to the number of votes counted. The distributions for each candidate are typically only slightly adjusted.</p><p>Now that the last judicial recount has been completed, we can announce our <abbr title="member of parliament">MP</abbr> selection.</p><table class="election" summary="This table lists the number of seats each party could receive if the 2015 election used the stochastic election method">
<caption>2015 Stochastic Election Simulation Results</caption>
<thead>
<tr>
<th>Party</th>
<th>Seats</th>
<th>Seat Percentage</th>
<th>Vote Percentage</th>
</tr>
</thead>
<tbody>
<tr>
<td>Liberal</td>
<td class="number">139</td>
<td class="number">41.1%</td>
<td class="number">39.5%</td>
</tr>
<tr>
<td>Conservative</td>
<td class="number">105</td>
<td class="number">31.1%</td>
<td class="number">31.9%</td>
</tr>
<tr>
<td>NDP-New Democratic Party</td>
<td class="number">63</td>
<td class="number">18.6%</td>
<td class="number">19.7%</td>
</tr>
<tr>
<td>Bloc Québécois</td>
<td class="number">19</td>
<td class="number">5.62%</td>
<td class="number">4.66%</td>
</tr>
<tr>
<td>Green Party</td>
<td class="number">11</td>
<td class="number">3.25%</td>
<td class="number">3.45%</td>
</tr>
<tr>
<td>Christian Heritage Party</td>
<td class="number">1</td>
<td class="number">0.296%</td>
<td class="number">0.0870%</td>
</tr>
</tbody>
</table>
<p><a href="http://r6.ca/StochasticElection/2015Results.ods">Results by province and by riding are available (electoral districts on page 2).</a></p><p>The results were generated from <a href="http://enr.elections.ca/DownloadResults.aspx">Elections Canada data</a>. One hundred and seventy-four elected candidates differ from the actual 2015 election outcome.
</p><p>The Christian Heritage Party holds the balance of power in this parliament.
Assuming a Liberal party member becomes speaker of the house,
that means the Liberals together with the Bloc Québécois and Green Party have 168 votes and the Conservative and <abbr title="New Democratic Party">NDP</abbr> together have 168 votes.
In this case, it is the Christian Heritage Party vote that would break the tie.
</p><p>Unfortunately, Liberal leader Justin Trudeau with 52.0% of the vote in the riding of Papineau, still lost to Maxime Claveau of the Bloc Québécois with 12.2% of the vote.
Apparently it is now the Bloc Québécois’s turn to represent their support in Papineau.
If Justin Trudeau wants to be prime minister, his best bet is to try to be appointed to the Senate and rule from there.
Similarly <abbr title="New Democratic Party">NDP</abbr> leader Tom Mulcair lost to Liberal candidate Rachel Bendayan in the riding of Outremont.
Perhaps there is a deal to be struck between the Liberal and <abbr title="New Democratic Party">NDP</abbr> to get their leaders appointed to the Senate.
</p><p class="fine">This is only one example of the results of a stochastic election. Because of the stochastic nature of the election process, actual results may differ.
</p><p class="fine">In Canada’s election process, it is sometimes advantageous to not vote for one’s preferred candidate. The stochastic election system is the only system in which it always best to vote for your preferred candidate. Therefore, if the 2015 election were actually using a stochastic election system, people would be allowed to vote for their true preferences. The outcome could be somewhat different than what this simulation illustrates.</p><p>Related info</p><ul>
<li><a href="20151021T015605Z.html">2015 stochastic election expected results</a></li>
<li><a href="20110530T170250Z.html">2011 stochastic election results</a></li>
<li><a href="20081107T061447Z.html">2008 stochastic election results</a></li>
<li><a href="20060217T201200Z.html">2006 stochastic election results</a></li>
<li><a href="20060122T172700Z.html">2004 stochastic election results</a></li>
</ul>
http://r6.ca/blog/20151021T015605Z.htmlStochastic Elections Canada 2015 Update2015-10-21T01:56:05Z2015-10-21T01:56:05Z
<blockquote>
<p>The rule of the people has the fairest name of all, isonomia, and does none of the things that a monarch does. The lot determines offices, power is held accountable, and deliberation is conducted in public. — Herodotus</p>
</blockquote>
<p>In Athenian democracy, sortition was used to select their magistrates in order to avoid the oligarchs buying their way into the office. What would happen if we used a form of sortition to to select our parliament? Since most people are too busy and unprepared to sit in parliament, I propose the next best thing: the drawing of lots in a riding to select a person to chose the representative for the riding. What would happen?
</p><p>The <a title="Voting System" href="20040603T005300Z.html">resulting system</a> is a unique system that provides local representation and approximately proportional representation. Each party gets a chance to represent a riding in roughly proportion to the amount of support they have in the riding. Democracy means “rule of people”, not “rule of the majority” (nor “rule of the plurality”). Not only is it perfectly democratic for the minority to get an opportunity to be represented in parliament, it is more democratic than what we have in Canada now.
</p><p>Of course, directly selecting a random person in a riding is fraught with difficulties, so instead one would vote, as we do now, for one’s preferred candidate. Then, once the votes are tallied, a candidate is selected randomly with probability proportional to the vote they received. In this system it is <em>always</em> best to vote for your preferred candidate. There will be no more strategic votes or vote splitting. Voting participation would go up since every vote increases the chances of your preferred candidate being selected. The resulting parliament will be close to the proportion of the number of votes received for each party without having MPs selected from a party list.
</p><p>Imagine a world where we have Stochastic Elections Canada. Stochastic Election law requires that all counts be validated and recounted, if requested, before seat selection takes place. Because in every vote influences the outcome, we must await the return of the writs, scheduled by electoral law for Monday, November 9, 2015. For now, we can bring you our seat expectation chart based on preliminary 2015 election results:
</p><table class="election" summary="This table lists the expected number of seats each party would receive if the 2015 election used the stochastic election method">
<caption>Expected Seat Distribution</caption>
<thead>
<tr>
<th>Party</th>
<th>Expected Number of Seats<br/>(95% confidence)</th>
<th>Distribution Shape</th>
</tr>
</thead>
<tbody>
<tr>
<td>Animal Alliance/Environment Voters</td>
<td>0 – 1</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=336033&chd=s:9CAAAAAAA"/></td>
</tr>
<tr>
<td>ATN</td>
<td>0</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=DCDCDC&chd=s:9A"/></td>
</tr>
<tr>
<td>Bloc Québécois</td>
<td>9 – 22</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=87CEFA&chd=s:AAAAAABDHMVgr1895yoeUNIECBBAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>Canada Party</td>
<td>0</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=DCDCDC&chd=s:9A"/></td>
</tr>
<tr>
<td>CAP</td>
<td>0</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=DC143C&chd=s:9AAA"/></td>
</tr>
<tr>
<td>Christian Heritage Party</td>
<td>0 – 2</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=cc6699&chd=s:9TDAAAAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>Communist</td>
<td>0 – 1</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=FF6347&chd=s:9FAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>Conservative</td>
<td>91 – 122</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=6495ED&chd=s:AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABBBCCDEGHKMPTXbfkpty157899752yuqlhcYUROLJHFEDCCBBBAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>Democratic Advancement</td>
<td>0 – 1</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=DCDCDC&chd=s:9CAAA"/></td>
</tr>
<tr>
<td>Forces et Démocratie - Allier les forces de nos régions</td>
<td>0 – 1</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=01af58&chd=s:9MBAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>Green Party</td>
<td>5 – 18</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=99c955&chd=s:AAABEJRdp1895wmcTMHECBAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>Liberal</td>
<td>119 – 153</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=ea6d6a&chd=s:AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABBBCDDEGHJMORVYchlptx1468998752yvrmieaWTQNKIHFEDCCBBBAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>Libertarian</td>
<td>0 – 3</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=f2ba00&chd=s:9sPEBAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>Marxist-Leninist</td>
<td>0 – 1</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=CD5C5C&chd=s:9LBAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>NDP-New Democratic Party</td>
<td>54 – 81</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=F4A460&chd=s:AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABBBCDEGILOSWbgmrw14799863zvqlgbWSPLJHFEDCBBBAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>PACT</td>
<td>0</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=DCDCDC&chd=s:9A"/></td>
</tr>
<tr>
<td>PC Party</td>
<td>0 – 1</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=6666cc&chd=s:9FAAAAAAA"/></td>
</tr>
<tr>
<td>Pirate</td>
<td>0</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=71079f&chd=s:9BAAAA"/></td>
</tr>
<tr>
<td>Radical Marijuana</td>
<td>0 – 1</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=D2B48C&chd=s:9CAAAAAAA"/></td>
</tr>
<tr>
<td>Rhinoceros</td>
<td>0 – 1</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=D8BFD8&chd=s:9JBAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>Seniors Party</td>
<td>0</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=DCDCDC&chd=s:9A"/></td>
</tr>
<tr>
<td>The Bridge</td>
<td>0</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=9370DB&chd=s:9A"/></td>
</tr>
<tr>
<td>United Party</td>
<td>0</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=de3163&chd=s:9A"/></td>
</tr>
<tr>
<td>Independent</td>
<td>0 – 3</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=DCDCDC&chd=s:90TEBAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"/></td>
</tr>
<tr>
<td>No Affiliation</td>
<td>0 – 1</td>
<td><img alt="" src="http://chart.apis.google.com/chart?cht=bvs&chs=311x20&chbh=1,0,0&chco=DCDCDC&chd=s:9PAAAAA"/></td>
</tr>
</tbody>
</table>
<p>Related info</p><ul>
<li><a href="20110530T170250Z.html">2011 stochastic election results</a></li>
<li><a href="20081107T061447Z.html">2008 stochastic election results</a></li>
<li><a href="20060217T201200Z.html">2006 stochastic election results</a></li>
<li><a href="20060122T172700Z.html">2004 stochastic election results</a></li>
</ul>
http://r6.ca/blog/20150827T020314Z.htmlClearing Up “Clearing Up Mysteries”2015-08-27T02:03:14Z2015-08-27T02:03:14Z
<p>I am a big fan of <a title="Jaynes on Entropy" href="20100802T005835Z.html">E. T. Jaynes</a>.
His book <cite>Probability Theory: The Logic of Science</cite> is the only book on statistics that I ever felt I could understand.
Therefore, when he appears to rail against the conclusions of Bell’s theorem in his paper
“<a href="http://bayes.wustl.edu/etj/articles/cmystery.ps.gz">Clearing up Mysteries—The Original Goal</a>”, I take him seriously.
He suggests that perhaps there could be a time-dependent hidden variable theory that could yield the outcomes that quantum mechanics predicts.</p><p>However, after reading Richard D. Gill’s paper,
“<a href="http://arxiv.org/abs/quant-ph/0301059v2">Time, Finite Statistics, and Bell’s Fifth Position</a>”
it is very clear that there can be nothing like a classical explanation that yields quantum predictions, time-dependent or otherwise.
In this paper Gill reintroduces Steve Gull’s computer network, where a pair of classical computers is tasked to recreate probabilities predicted in a <a title="CHSH inequality" href="https://en.wikipedia.org/w/index.php?tilte=CHSH_inequality&oldid=676806380">Bell-CHSH</a> delayed choice experiment.
The catch is that the challenger gets to choose the stream of bits sent to each of the two spatially separated computers in the network.
These bits represent the free choice an experimenter running a <a title="CHSH inequality" href="https://en.wikipedia.org/w/index.php?tilte=CHSH_inequality&oldid=676806380">Bell-CHSH</a> experiment has to choose which polarization measurements to make.
No matter what the classical computer does, no matter how much time-dependent fiddling you want to do, it can never produce correlations that will violate the <a title="CHSH inequality" href="https://en.wikipedia.org/w/index.php?tilte=CHSH_inequality&oldid=676806380">Bell-CHSH</a> inequality in the long run.
This is Gull’s “You can’t program two independently running computers to emulate the EPR experiment” theorem.</p><p>Gill presents a nice analogy with playing roulette in the casino.
Because of the rules of roulette, there is no computer algorithm can implement a strategy that will beat the house in roulette in the long run.
Gill goes on to quantify exactly how long the long run is in order to place a wager against other people who claim they can recreate the probabilities predicted by quantum mechanics using a classical local hidden variable theory.
Using the theory of supermartingales, one can bound the likelihood of seeing the <a title="CHSH inequality" href="https://en.wikipedia.org/w/index.php?tilte=CHSH_inequality&oldid=676806380">Bell-CHSH</a> inequality violated by chance by any classical algorithm in the same way that one can bound the likelihood of long winning streaks in roulette games.</p><p>I liked the casino analogy so much that I decided to rephrase Gull’s computer network as a coin guessing casino game I call <a title="Bell’s Casino Problem" href="20150816T185621Z.html">Bell’s Casino</a>.
We can prove that any classical strategy, time-dependent or otherwise, simply cannot beat the house at that particular game in the long run.
Yet, there is <a title="Bell’s Casino Solution" href="20151210T033709Z.html">a strategy</a> where the players employ entangled qubits and beat the house on average.
This implies there cannot be any classical phenomena that yields quantum outcomes.
Even if one proposes some classical oscollating (time-dependent) hidden variable vibrating at such a high rate that we could never practically measure it, this theory still could not yield quantum probabilities,
because such a theory implies we could simulate it with Gull’s computer network.
Even if our computer simulation was impractically slow, we could still, in principle, deploy it against Bell’s Casino to beat their coin game.
But no such computer algorithm exists, in exactly the same way that there is no computer algorithm that will beat a casino at a fair game of roulette.
The fact that we can beat the casino by using qubits clearly proves that qubits and quantum physics is something truly different.</p><p>You may have heard the saying that “correlation does not imply causation”.
The idea is that if outcomes <var>A</var> and <var>B</var> are correlated, the either <var>A</var> causes <var>B</var>, or <var>B</var> causes <var>A</var>, or there is some other <var>C</var> that causes <var>A</var> and <var>B</var>.
However, in quantum physics there is a fourth possibilty.
We can have correlation without causation.</p><p>In light of Gull and Gill’s iron clad argument, I went back to reread Jaynes’s “Clearing up Mysteries”.
I wanted to understand how Jaynes could have been so mistaken.
After rereading it I realized that I had misunderstood what he was trying to say about Bell’s theorem.
Jaynes just wanted to say two things.</p><p>Firstly, Jaynes wanted to say that Bell’s theorem does not necessarily imply action at a distance.
This is not actually a controversial statement.
The many-worlds interpretation is a local, non-realist (in the sense that experiments do not have unique definite outcomes) interpretation of quantum mechanics.
This interpretation does not invoke any action at a distance and is perfectly compatible with Bell’s theorem.
Jaynes spends some time noting that correlation does not imply causation in an attempt to clarify this point although he never talks about the many-worlds interpretation.</p><p>Secondly, Jaynes wanted to say that Bell’s theorem does not imply that quantum mechanics is the best possible physical theory that explains quantum outcomes.
Here his argument is half-right and half-wrong.
He spends some time suggesting that maybe there is a time-dependent hidden variable theory that could give more refined predictions than predicted by quantum theory.
However, the suggestion that any classical theory, time-dependent or otherwise, could underlie quantum mechanics is refuted by Bell’s theorem and this is clearly illustrated by Gull’s computer network or by Bell’s casino.
Jaynes learned about Gull’s computer network argument at the same conference that he presented “Clearing Up Mysteries”.
His writing suggests that he was surprised by the argument, but he did not want to rush to draw any conclusions to from it without time to get a deeper understanding of it.
Nevertheless, Jaynes larger point was still correct.
Bell’s theorem does not imply that there is not some, non-classical, refinement of quantum mechanics that might yield more informative predictions than quantum mechanics does and Jaynes was worried that people would not look for such a refinement.</p><p>Jaynes spent a lot of effort trying to separate epistemology, where probability theory rules how we reason in the face of imperfect knowledge, from ontology, which describes what happens in reality if we had perfect information.
Jaynes thought that quantum mechanics was mixing these two branches together into one theory and worried that if people were mistaking quantum mechanics for an ontological theory then they would never seek a more refined theory.</p><p>While Bell’s theorem does not rule out that there may be a non-classical hidden variable theory,
Colbeck and Renner’s paper “<a href="http://arxiv.org/abs/1005.5173v3">No extension of quantum theory can have improved predictive power</a>” all but eliminates that possibility
by proving that there is no quantum hidden variable theory.
This can be seen as a strengthening of Bell’s theorem, and they even address some of the same concerns that Jaynes had about Bell’s theorem.</p><blockquote>
<p>To quote Bell [2], <dfn>locality</dfn> is the requirement that “…the result of a measurement on one system [is] unaffected by
operations on a distant system with which it has interacted in the past…” Indeed, our non-signalling conditions reflect
this requirement and, in our language, the statement that P<sub>XYZ|ABC</sub> is non-signalling is equivalent to a statement that
the model is local (see also the discussion in [28]). (We remind the reader that we do not assume the non-signalling
conditions, but instead derive them from the free choice assumption.)
In spite of the above quote, Bell’s formal definition of locality is slightly more restrictive than these non-signalling
conditions. Bell considers extending the theory using hidden variables, here denoted by the variable Z. He requires
P<sub>XY|ABZ</sub> = P<sub>X|AZ</sub> × P<sub>Y|BZ</sub> (see e.g. [13]), which corresponds to assuming not only P<sub>X|ABZ</sub> = P<sub>X|AZ</sub> and P<sub>Y|ABZ</sub> =
P<sub>Y|BZ</sub> (the non-signalling constraints, also called parameter-independence in this context), but also P<sub>X|ABYZ</sub> =
P<sub>X|ABZ</sub> and P<sub>Y|ABXZ</sub> = P<sub>Y|ABZ</sub> (also called outcome-independence). These additional constraints do not follow
from our assumptions and are not used in this work.</p>
</blockquote>
<p>The probabilistic assumptions are weaker in Colbeck and Renner’s work than in Bell’s theorem, because they want to exclude quantum hidden variable theories in addition to classical
hidden variable theories.
Today, if one wants to advance a local hidden variable theory, it would have to be a theory that is even weirder than quantum mechanics, if such a thing is even logically possible.
It seems that quantum mechanics’s wave function is an ontological description after all.</p><p>I wonder what Jaynes would have thought about this result.
I suspect he would still be looking for an exotic hidden variable theory.
He seemed so convinced that probability theory was solely in the realm of epistemology and not ontology that he would not accept any probabilistic ontology at all.</p><p>I think Jaynes was wrong when he suggested that quantum mechanics was necessarily mixing up epistemology and ontology.
I believe the many-worlds interpretation is trying to make that distinction clear.
In this interpretation the wave-function and Schrödinger’s equation is ontology, but the Born rule that relates the norm-squared amplitude to probability ought to be epistemological.
However, there does remain an important mystery here:
Why do the observers within the many-worlds observe quantum probabilities that satisfy the Born rule?
I like to imagine Jaynes could solve this problem if he were still around.
I imagine that would say that something like, “Due to phase invariance of the wave-function … <i>something something</i> … transformation group … <i>something something</i> … thus the distribution must be in accordance with the Born rule.”
After all, Jaynes did manage to use transformation groups to solve the <a href="https://en.wikipedia.org/w/index.php?title=Bertrand_paradox_%28probability%29&oldid=674563212#Jaynes.27_solution_using_the_.22maximum_ignorance.22_principle">Bertrand paradox</a>, a problem widely regarded as being unsolvable due to being underspecified.
</p>http://r6.ca/blog/20150816T185621Z.htmlBell’s Casino Problem2015-08-16T18:56:21Z2015-08-16T18:56:21Z
<p>A new casino has opened up in town named “Bell’s Casino”. They are offering a coin game. The game works as follows.
</p><p>The house will commit two coins on the table, oriented heads or tails each, and keep them covered. The player calls what the faces of the each of the coins are, either HH, HT, TH, or TT. The
casino reveals the coins and if the player is correct, they win $1, and otherwise they lose $1.
</p><dl>
<dt>Problem 1.</dt>
<dd>Prove that there is no strategy that can beat the casino.</dd>
</dl>
<p>After opening the customers stop coming by to play this boring game, so to boost attendance the casino modifies the game as follows.
</p><p>The house will commit two coins on the table, oriented heads or tails each, and keep them covered. The player calls what the faces of each of the two coins are, either HH, HT, TH, or TT. The
casino reveals one coin, of the players choice. After seeing revealed coin, the player can elect to back out of the game and neither win nor lose, or keep going, and see the second coin.
If the player’s call is correct, they win $1, and otherwise they lose $1.
</p><dl>
<dt>Problem 2.</dt>
<dd>Prove that there is no strategy that can beat the casino.</dd>
</dl>
<p>Even with the new, more fair, game, attendance at the casino starts dropping off again. The casino decides to offer a couples game.
</p><p>The house will commit two coins on two tables, oriented heads or tails each, and keep them covered. The couple, together, calls what the the faces of each of the two coins are, either HH, HT, TH, or
TT. Then, each player in the couple gets to see one coin each. Collectively they get to decide whether they are going to back out of the game or not by the following method. After seeing
their revealed coin, each player will raise either a black flag or a red flag. If both players raise the different colour flags, the game ends and no one wins or loses. If both players raise the
same colour flag, the game keeps going. If the couples original call was right, they win $1, and otherwise, they lose $1. To ensure that the couple cannot cheat, the two tables
are places far enough apart such that each player’s decision on which flag to raise is <a title="Space-like interval" href="https://en.wikipedia.org/wiki/Spacetime#Space-like_interval">space-like separated</a>. Specifically the tables are placed 179 875 475 km apart and
each player has 1 minute to decide which flag to raise otherwise a black flag will be raised on their behalf (or, more realistically, the tables are placed 400 m apart and each player has
100 nanoseconds to decide which flag to raise).
</p><dl>
<dt>Problem 3.</dt>
<dd>Prove that there is no strategy for the couple that can beat the casino.</dd>
</dl>
<dl>
<dt>Problem 4.</dt>
<dd>Devise a physical procedure that a couple can follow to beat the casino on average at this last game without cheating.</dd>
</dl>
<p>The casino cannot figure out how they keep losing money on this game and, soon, Bell’s Casino goes bankrupt.
</p>http://r6.ca/blog/20150222T233125Z.htmlParallel Evaluation of the Typed Lambda Calculus2015-02-22T23:31:25Z2015-02-22T23:31:25Z
<p>There is much written about the <a title="Call-by-Value is Dual to Call-by-Name" href="http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf">duality</a> between strict-order (call-by-value) evalutaion for the lambda calculus and the normal-order (call-by-need) evaluation (or semantic equivently, lazy evaluation).
In the simply typed lambda calculus, all evaluation eventually terminates, so both evaluation strategies result in the same values.
However, when general recursion is added to the simply typed lambda calculus (via a fixpoint operator, for example) then evaluation of some expressions does not terminate.
More expressions terminate with normal-order evaluation than with strict-order evaluation.
In fact, if evaluation terminates in any order, then it terminates with normal-order evaluation.
</p><p>I would like to discuss the possibility of a third, even laxer evaluation strategy available for the typed lambda calculus that allows for even more expressions to terminate.
I did just say that normal-order evaluation is, in some sense, a best possible evaluation order, so, in order to beat it, we will be adding more redexes that add the commuting conversions.
</p><p>The typed lambda calculus enjoys certain commuting conversions for case expressions that allow every elimination term to pass through the case expression.
For example, the commuting conversion for the <code>π₁</code> elimination term and the <code>case</code> experssion says that
</p><pre>π₁(case e₀ of σ₁ x. e₁ | σ₂ y. e₂)</pre>
<p>converts to
</p><pre>case e₀ of σ₁ x. π₁(e₁) | σ₂ y. π₁(e₂)</pre>
<p>These commuting conversions are required so that <a title="Proofs and Types" href="http://www.paultaylor.eu/stable/Proofs+Types.html">the subformula property holds</a>.
</p><p>My understanding is that a corollary of this says that
</p><pre>f(case e₀ of σ₁ x. e₁ | σ₂ y. e₂)</pre>
<p>and
</p><pre>case e₀ of σ₁ x. f(e₁) | σ₂ y. f(e₂)</pre>
<p>are denotationally equivalent whenever <code>f</code> is a strict function.
</p><p>I would like to develop a version of the lambda calculus that allows these two expressions to denote the same value for any <code>f</code>.
Call this, the unrestricted commuting conversion property.
A lambda calculus with this property would necessarily be parallel and thus will require a parallel evaluation strategy.
For example, the natural definition of <code>or</code> becomes the parallel-or operation.
</p><pre>or x y := if x then True else y</pre>
<p>This definition has the usual short-circuit property that <code>or True ⊥</code> is <code>True</code> where <code>⊥</code> is defined by
</p><pre>⊥ := fix id</pre>
<p>If we use the unrestricted commuting conversion property then we also have the that <code>or ⊥ True</code> is <code>True</code>:
</p><pre>or ⊥ True
= {definition of or}
if ⊥ then True else True
= {β-expansion}
if ⊥ then const True ⟨⟩ else const True ⟨⟩
= {commuting}
const True (if ⊥ then ⟨⟩ else ⟨⟩)
= {β-reduction}
True</pre>
<p>Hence <code>or</code> is parallel-or.
</p><p>Other parallel functions, such as the majority function, also follow from their natural definitions.
</p><pre>maj x y z := if x then (or y z) else (and y z)</pre>
<p>In this case <code>maj ⊥ True True</code> is <code>True</code>.
</p><pre>maj ⊥ True True
= {definition of maj}
if ⊥ then (or True True) else (and True True)
= {evaluation of (or True True) and (and True True)
if ⊥ then True else True
= {commuting}
True</pre>
<p>It is easy to verify that <code>maj True ⊥ True</code> and <code>maj True True ⊥</code> are also both <code>True</code>.
</p><p>My big question is whether we can devise some nice operational semantics for the lambda calculus that will have the unrestricted commuting conversions property that I desire.
Below I document my first attempt at such operational semantics, but, spoiler alert, it does not work.
</p><p>The usual rule for computing weak head normal form for the case expression <code>case e₀ of σ₁ x. e₁ | σ₂ y. e₂</code> says to first convert <code>e₀</code> to weak head normal form.
If it is <code>σ₁ e₀′</code> then return the weak head normal form of <code>e₁[x ↦ e₀′]</code>.
If it is <code>σ₂ e₀′</code> then return the weak head normal form of <code>e₂[y ↦ e₀′]</code>.
In addition to this rule, I want to add another rule for computing the weak head normal form for the case expression.
This alernative rules says that we compute the weak head normal forms of <code>e₁</code> and <code>e₂</code>.
If we get <code>C₁ e₁′</code> and <code>C₂ e₂′</code> respectively for introduction terms (<abbr title="also known as">a.k.a.</abbr> constructors) <code>C₁</code> and <code>C₂</code>, and
if additionally <code>C₁</code> = <code>C₂</code> then return the following as a weak head normal form, <code>C₁ (case e₀ of σ₁ x. e₁′ | σ₂ y. e₂′)</code>.
If <code>C₁</code> ≠ <code>C₂</code> or if we get stuck on a neutral term (e.g. a varaible), then this rule does not apply.
</p><p>This new rule is in addition to the usual rule for <code>case</code>. Any implementation must run these two rules in parallel because it is possible that either rule (or both) can result in non-termination when recursivly computing weak head normal forms of sub-terms.
I suppose that in case one has unlifted products then when computing the weak head normal form of a <code>case</code> expression having a product type or function type, one can immediately return
</p><pre>⟨case e₀ of σ₁ x. π₁ e₁ | σ₂ y. π₁ e₂, case e₀ of σ₁ x. π₂ e₁ | σ₂ y. π₂ e₂⟩</pre>
or
<pre>λz. case e₀ of σ₁ x. e₁ z | σ₂ y. e₂ z</pre>
<p>This amended computation of weak head normal form seems to work for computing <code>or</code> and <code>maj</code> functions above so that they are non-strict in every argument, but there is another example where even this method of computing weak head normal form is not sufficent.
Consider the functions that implements associativity for the sum type.
</p><pre>assocL : A + (B + C) -> (A + B) + C
assocL z := case z of σ₁ a. σ₁ (σ₁ a) | σ₂ bc. (case bc of σ₁ b. σ₁ (σ₂ b) | σ₂ c. σ₂ c)
assocR : (A + B) + C -> A + (B + C)
assocR z := case z of σ₁ ab. (case ab of σ₁ a. σ₁ a | σ₂ b. σ₂ (σ₁ b)) | σ₂ c. σ₂ (σ₂ c)</pre>
<p>Now let us use unrestricted commuting conversions to evaluate <code>assocR (assocL (σ₂ ⊥))</code>.
</p><pre>assocR (assocL (σ₂ ⊥))
= { definition of assocL and case evaluation }
assocR (case ⊥. σ₁ b. σ₁ (σ₂ b) | σ₂ c. σ₂ c)
= { commuting conversion }
case ⊥. σ₁ b. assocR (σ₁ (σ₂ b)) | σ₂ c. assocR (σ₂ c)
= { definition of assocR and case evaluations }
case ⊥. σ₁ b. σ₂ (σ₁ b) | σ₂ c. σ₂ (σ₂ c)
= { commuting conversion }
σ₂ (case ⊥. σ₁ b. σ₁ b | σ₂ c. σ₂ c)
= { η-contraction for case }
σ₂ ⊥</pre>
<p>Even if η-contraction is not a reduction rule used for computation, it is still the case that <code>t</code> and <code>case t. σ₁ b. σ₁ b | σ₂ c. σ₂ c</code> should always be dentotationally equivalent.
Anyhow, we see that by using commuting conversions that a weak head normal form of <code>assocR (assocL (σ₂ ⊥))</code> should expose the <code>σ₂</code> constructor.
However, if you apply even my ammended computation of weak head normal form, it will not produce any constructor.
</p><p>What I find particularly surprising is the domain semantics of <code>assocL</code> and <code>assocR</code>.
<code>assocL</code> seems to map <code>σ₂ ⊥</code> to <code>⊥</code> because no constructor can be exposed.
<code>assocR</code> maps <code>⊥</code> to <code>⊥</code>.
Therefore, according to the denotational semantics, the composition should map <code>σ₂ ⊥</code> to <code>⊥</code>, but as we saw, under parallel evaluation it does not.
It would seem that the naive denotational semantics appears to not capture the semantics of parallel evaluation.
The term <code>case ⊥. σ₁ b. σ₁ (σ₂ b) | σ₂ c. σ₂ c</code> seems to be more defined than ⊥, even though no constructor is available in the head position.
</p><p>Although my attempt at nice operational semantics failed, I am still confident some nice computation method exists.
At the very least, I believe a rewriting system will work which has all the usual rewriting rules plus a few extra new redexes that says that an elimination term applied to the <code>case</code> expression commutes the elimination term into all of the branches,
and another that says when all branches of a case expression contain the same introduction term, that introduction term is commuted to the outside of the case expression, and maybe also the rules I listed above for unlifted products.
I conjecture this rewriting system is confluent and unrestricted commuting conversions are convertable (probably requiring η-conversions as well).
</p><p>Without proofs of my conjectures I am a little concerned that this all does not actually work out.
There may be some bad interaction with fixpoints that I am not seeing.
If this does all work out then shouldn’t I have heard about it by now?
</p>