Russell O’Connor’s Blog2020-12-13T02:30:15ZRussell O’Connorhttp://r6.ca/http://r6.ca/blog/http://r6.ca/blog/20201213T023015Z.htmlCarbon Tax: Running my Numbers2020-12-13T02:30:15Z2020-12-13T02:30:15Z
<p>I am so excited to read today that the Liberal government is <a title="Prime Minister announces Canada’s strengthened climate plan to protect the environment, create jobs, and support communities" href="https://pm.gc.ca/en/news/news-releases/2020/12/11/prime-minister-announces-canadas-strengthened-climate-plan-protect">planning to raise the tax on carbon</a> up to $170 per tonne by 2030.
The biggest problem with the previous carbon pricing program was that $50 per tonne was way too low.
The price needs to be large enough such that capturing carbon is preferable to paying the tax.
This announcement would finally put us into that ballpark.
</p><p>Last fall I was discussing with someone who claimed that the carbon tax was just a tax grab and did not believe that the Liberal government was really going to pay the funds back out through the Climate Action Incentive tax credit.
I did believe it would be paid out, but to be certain, I figured I should run the numbers.
</p><p>The major carbon tax payments for my household is (1) natural gas for heating, and (2) gasoline for driving.
Between April 2019 and March 2020, I paid $61.83 in carbon taxes for natural gas heating.
During the same period I bought approximately 651.612 litres of gasoline.
At a price of 4.42 cents per liter, I estimate I paid about $28.80 in carbon taxes for that gasoline.
That brings me to a total of $90.63 paid in carbon taxes for that period.
</p><p>On my 2018 tax return I received a $231 Climate Action Incentive tax credit for my household.
That leaves me with a net benefit of $140.37 as a reward for emitting less carbon than average.
This is to be expected because average household carbon emissions are much higher than median household emissions due to a relatively few high emitters.
</p><p>I am omitting carbon tax charges for other incidentals, most notably for airfare.
If anyone has any methods for calculating the carbon tax on airfares, please let me know.
However, I have little doubt in my mind that this $140.37 more than covers any other outstanding carbon tax costs.
Also keep in mind that the Climate Action Incentive tax credit was paid in <em>advance</em> with my 2018 income tax return, before I paid any carbon taxes at all.
</p><p>Some people on twitter were wrongly arguing that the Climate Action Incentive tax credit is income based.
I filled out my income tax return and the $231 value was based on the size of my household and was independent of my income.
</p><p>The carbon tax program is great because it lets market forces determine how best to reduce carbon emissions.
Those few households that are emitting most of the carbon are financially incentivized to change their consumption patterns.
For reasons that I do not understand, both the federal and Ontario Conservative parties hate market solutions.
Their "solution" to the carbon problem is to have their governments pick winners and losers themselves.
No doubt that way they can make sure their cronies just happen to be among the winners.
</p><p>One could argue that I am being selfish, because the more the tax on carbon increases, the more rewards I earn.
On the other hand, perhaps those Canadians who are arguing against the carbon tax should run their own numbers and see how much they benefit from this carbon program.
</p>http://r6.ca/blog/20200929T023701Z.htmlIt Is Never a Compiler Bug Until It Is2020-09-29T02:37:01Z2020-09-29T02:37:01Z
<p>Last week I was trying to add some <a href="https://github.com/bitcoin-core/secp256k1/pull/822/commits/2456616cb1bb34178ff83b24eaf738f0fee3d82b#diff-b04459e37839cd223176618536295715R429">testing code to libsecp256k1</a> and I was pulling out my hair trying to get it to work.
No amount of <code>printf</code> was working to illuminate what I was doing wrong.
Finally, out of desperation, I thought I would do a quick check to see if there are any compiler bugs related to <code>memcmp</code>, and lo and behold, I found <a href="https://gcc.gnu.org/bugzilla/show_bug.cgi?id=95189">GCC bug #95189: memcmp being wrongly stripped like strcmp</a>.</p><p>Honestly this was a pretty horrifying bug to read about.
Under some circumstances GCC 9 and 10 will cause <code>memcmp</code> to return an incorrect value when one of the inputs is statically known array that contains <code>NULL</code> bytes.
As I rushed to <a href="https://gist.githubusercontent.com/roconnor/2b8e22e829ed80088ed6690cc3c7f3a8/raw/455571a6d9053c597c1585debe6f9dbd6af85071/gistfile1.txt">recompile my computer system using GCC 8</a>, I contemplated what the vast consequences of such a bug could be, and pondered how it was possible that computers could function at all.</p><p>However over the week, with the help of my colleagues, we managed to get a better understanding of the scope of the bug.
The bug can only convert non-zero values to zero values.
The static array needs to have a <code>NULL</code> byte within the first 4 bytes.
Most importantly, the <code>memcmp</code> result must not immediately be compared to <code>0</code> for equality or inequality, or any equivalent test.
A different code path is taken in the compiler in that case.
That explained why computers were still functioning.
I expect the vast majority of the uses of <code>memcmp</code> does an immediate test for equality with <code>0</code>.</p><p>I still wondered though, how much code was being affected. My colleague Tim suggested that it would be possible to instrument GCC to emit a message when it was about to miscompile a program.
Together we came up with <a href="https://gcc.gnu.org/bugzilla/attachment.cgi?id=49276&action=diff">a patch</a> to GCC 9 and 10 that would print a debugging message.
Once again, I recompiled my entire system, to see what GCC was miscompiling.
This is what I found:</p><ul>
<li><a href="https://github.com/unicode-org/icu/blob/4fb47b12a70737ee12326220e71c2d73c5ec658f/icu4c/source/common/uniset_props.cpp#L709">https://github.com/unicode-org/icu/blob/4fb47b12a70737ee12326220e71c2d73c5ec658f/icu4c/source/common/uniset_props.cpp#L709</a></li>
<li><a href="https://github.com/xiph/flac/blob/ce6dd6b5732e319ef60716d9cc9af6a836a4011a/src/flac/decode.c#L1310">https://github.com/xiph/flac/blob/ce6dd6b5732e319ef60716d9cc9af6a836a4011a/src/flac/decode.c#L1310</a></li>
<li><a href="https://github.com/torvalds/linux/blob/fb0155a09b0224a7147cb07a4ce6034c8d29667f/drivers/atm/zatm.c#L1172">https://github.com/torvalds/linux/blob/fb0155a09b0224a7147cb07a4ce6034c8d29667f/drivers/atm/zatm.c#L1172</a></li>
<li><a href="https://github.com/nss-dev/nss/blob/1f3746f5107535a47bb4e3969f561e1bd1314bab/gtests/pk11_gtest/pk11_chacha20poly1305_unittest.cc#L425">https://github.com/nss-dev/nss/blob/1f3746f5107535a47bb4e3969f561e1bd1314bab/gtests/pk11_gtest/pk11_chacha20poly1305_unittest.cc#L425</a></li>
<li><a href="https://github.com/GNOME/glib/blob/010569b3734f864fcf584f771915b78bd391eb5f/glib/tests/refstring.c#L70">https://github.com/GNOME/glib/blob/010569b3734f864fcf584f771915b78bd391eb5f/glib/tests/refstring.c#L70</a></li>
<li><a href="https://github.com/heimdal/heimdal/blob/7ae2dfd853c87f9cbecb6f399de4dad09bad4606/lib/gssapi/krb5/arcfour.c#L390">https://github.com/heimdal/heimdal/blob/7ae2dfd853c87f9cbecb6f399de4dad09bad4606/lib/gssapi/krb5/arcfour.c#L390</a>, <a href="https://github.com/heimdal/heimdal/blob/7ae2dfd853c87f9cbecb6f399de4dad09bad4606/lib/gssapi/krb5/arcfour.c#L661">https://github.com/heimdal/heimdal/blob/7ae2dfd853c87f9cbecb6f399de4dad09bad4606/lib/gssapi/krb5/arcfour.c#L661</a>, <a href="https://github.com/heimdal/heimdal/blob/7ae2dfd853c87f9cbecb6f399de4dad09bad4606/lib/gssapi/krb5/arcfour.c#L1279">https://github.com/heimdal/heimdal/blob/7ae2dfd853c87f9cbecb6f399de4dad09bad4606/lib/gssapi/krb5/arcfour.c#L1279</a></li>
<li><a href="https://github.com/zeromq/libzmq/blob/22d218a182855f28038e865cb75bf5897ff0c786/tests/test_mock_pub_sub.cpp#L203">https://github.com/zeromq/libzmq/blob/22d218a182855f28038e865cb75bf5897ff0c786/tests/test_mock_pub_sub.cpp#L203</a></li>
<li><a href="https://github.com/pigoz/mplayer-svn/blob/8d651873a9eb193f5155ffb51ece206f187cf00f/sub/sub_cc.c#L391-L412">https://github.com/pigoz/mplayer-svn/blob/8d651873a9eb193f5155ffb51ece206f187cf00f/sub/sub_cc.c#L391-L412</a></li>
</ul>
<p>On my entire system I only found 10 lines of code that were miscompiled.
Three lines are tests.
All of the lines could be rewritten as a comparison to 0.
None of the lines looked that serious.
I am not sure which one is the worse: the reduced message integrity code(?) from some ARCFOUR implementation or the something something from an ATM driver?</p><p>The mplayer miscompilation is the most mysterious.
The code surrounding that function all appears to be immediately compare <code>memcmp</code> with <code>0</code>.
And given that my debug message refused to point to exactly what line is being miscompiled in that function, I fear some set of optimizations has happened to allow this code to be miscompiled in some way.</p><p>With more hardware I could do <a href="https://hydra.nixos.org/jobset/nixpkgs/trunk#tabs-jobs">a more thorough investigation</a> of the consequences of this GCC bug.
Until then I am going to stick with GCC 8 until GCC 9 and 10 have a new point releases.
</p>http://r6.ca/blog/20191209T203122Z.htmlStochastic Elections Canada 2019 Results2019-12-09T20:31:22Z2019-12-09T20:31:22Z
<p>It is time to announce the results from Stochastic Elections Canada for the 43<sup>rd</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 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 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 2019 election used the stochastic election method">
<caption>2019 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">116</td>
<td class="number">34.3%</td>
<td class="number">33.1%</td>
</tr>
<tr>
<td>Conservative</td>
<td class="number">102</td>
<td class="number">30.2%</td>
<td class="number">34.4%</td>
</tr>
<tr>
<td>NDP-New Democratic Party</td>
<td class="number">61</td>
<td class="number">18.0%</td>
<td class="number">15.9%</td>
</tr>
<tr>
<td>Bloc Québécois</td>
<td class="number">25</td>
<td class="number">7.40%</td>
<td class="number">7.69%</td>
</tr>
<tr>
<td>Green Party</td>
<td class="number">23</td>
<td class="number">6.80%</td>
<td class="number">6.50%</td>
</tr>
<tr>
<td>People’s Party</td>
<td class="number">6</td>
<td class="number">1.78%</td>
<td class="number">1.64%</td>
</tr>
<tr>
<td>Christian Heritage Party</td>
<td class="number">1</td>
<td class="number">0.296%</td>
<td class="number">0.105%</td>
</tr>
<tr>
<td>Parti Rhinocéros</td>
<td class="number">1</td>
<td class="number">0.296%</td>
<td class="number">0.0535%</td>
</tr>
<tr>
<td>Independent</td>
<td class="number">3</td>
<td class="number">0.888%</td>
</tr>
</tbody>
</table>
<p><a href="http://r6.ca/StochasticElection/2019Results.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 eighty-one elected candidates differ from the actual 2019 election outcome.
</p><p>The People’s 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 163 votes and the Conservative and <abbr title="New Democratic Party">NDP</abbr> together have 163 votes.
The People’s Party’s 6 votes that is enough to decide which side reaches 169.
</p><p>The rise in the Green Party’s popular vote allowed them to gain more seats this election.
The Green Party has close to the same number of seats as the Bloc Québécois which reflects the fact that they have close to the same popular vote, even though the Green Party’s votes are more dilluted throughout Canada.
This illustrates how sortition is a form of proportional electoral system.
</p><p>Many proportional election systems require candidates to run under a party, or at least it is advantageous to be a run under a party.
One notable advantage of sortition is that independent or unaffiliated candidates are not disadvantaged.
While we did not select <a href="https://en.wikipedia.org/wiki/Jody_Wilson-Raybould">Jody Wilson-Raybould</a> for her riding, <a href="https://en.wikipedia.org/wiki/Jane_Philpott">Jane Philpott</a> was elected to <a href="https://en.wikipedia.org/wiki/Markham%E2%80%94Stouffville">Markham—Stouffville</a>.
Also Archie MacKinnon was elected to <a href="https://en.wikipedia.org/wiki/Sydney%E2%80%94Victoria">Sydney—Victoria</a>.
And, with sortition, even the 396 residents of <a href="https://en.wikipedia.org/wiki/Miramichi%E2%80%94Grand_Lake">Miramichi—Grand Lake</a> get a turn to have their choice of Mathew Grant Lawson to represent them in parliament.
</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 2019 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="20191030T035352Z.html">2019 stochastic election expected results</a></li>
<li><a href="20151116T042026Z.html">2015 stochastic election 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/20191030T035352Z.htmlStochastic Elections Canada 2019 Update2019-10-30T03:53:52Z2019-10-30T03:53:52Z
<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 11, 2019. For now, we can bring you our seat expectation chart based on preliminary 2019 election results:
</p><table class="election" summary="This table lists the expected number of seats each party would receive if the 2019 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 Protection Party</td>
<td>0 – 1</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAY0lEQVR42u3VUQ3AMAxDwXIqoREqjREImqDxOOxjirQ7CJaevJJ09752gJFWkqpSKagUUCmoFFApoFJQKaBSUCmgUkCloFJApYBKQaWASuF3lZ77mANGV%2BpOYXSlL3S3%2BeADD4TcUNgAD9xDAAAAAElFTkSuQmCC"/></td>
</tr>
<tr>
<td>Bloc Québécois</td>
<td>17 – 33</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAABAUlEQVR42u3cPQuCQByAcb%2B9Y36A5mjOxoaIZkGXOBoqyCJyEIqg0%2FMaBAcRX8L0oOfHzQ4HD%2F%2FjOLS01kII3RM%2FUrYn%2FUhpAD2xtNau6%2Fb1OduT%2BWJnARMrne6SotLNJWVzAeMqLRJlnAImVro4pKVKVcb2AiZVWkqUcQpQKUClXazDtLLS8MmpFzCj0spEGacAlQJU2s58n9RU6t15hwSMXWlNooxTgEoBKm3iBLKxUicgVGC8ShsTzdebV73AKJXOau%2BNOPcCI1d6e2XtE7U9ub1y2QsMWOnp0S3RfK3OHHyB31cqYrU8pl8kmq%2BJL0WsRMxcBTpW%2Bj96%2FH0MMIwPr9rIsyY8Y%2FEAAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>CFF - Canada’s Fourth Front </td>
<td>0</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAW0lEQVR42u3TMQ0AMQwEwfCnYzSWDMP9PYH0n2IGwkp7knT3zAR40klSVS4FlwIuBZcCLgVcCi4FXAouBVwKuBRcCrgUcCm4FHApuBR47NLdlQPevfSquwWC3318pn9d1Hzy0AAAAABJRU5ErkJggg%3D%3D"/></td>
</tr>
<tr>
<td>Christian Heritage Party</td>
<td>0 – 2</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAdElEQVR42u3VsQ2AMAxFQabNTsyRNSJRu6JLCRINpdmAgsoSdyN868lLZkbEaGsCJS2Z2XtXKagUUCmoFFApoFJQKaBSUCmgUuBjpfc8zAGlK%2FVOQaWASkGlgEqB10qvmBaB0pWOtp7bbhSoWGlZEeFI%2FNwDSmY%2B9YiLRCIAAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>Communist</td>
<td>0 – 1</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAYElEQVR42u3VwQmAQBRDwe3OQizxd%2BLJVBOLEGHBmRICj6y2SXoeBba02s6MSkGlgEpBpYBKAZWCSgGVgkoBlQIqBZUCKgVUCioFVAr%2Fq%2FS%2BzAF7V%2BpOYedKv5PEyvDGAwGRV%2BkuCdY4AAAAAElFTkSuQmCC"/></td>
</tr>
<tr>
<td>Conservative</td>
<td>99 – 130</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAABY0lEQVR42u2ay0rDUBgG%2B7CuxY3gxjdwqYJ4ARHEZTFoUSmCdCNK8S5BqIhURGiqxjYxaRJ%2FOFDEoNXk5ALOMIWuespXBpqQShRFpmlGoJWeG85u22NzHVHeNK5dNoHEVORlGAZDaOTpJVB9fnb3xGEZoNKyEE9UWT3sMw5QafFMrna%2Fq1S8uveYCKi0SBb37B8SVQYBOwGVFsTBpTsyUSVbAZWW63I0bq3JnSSg0tyZXn%2F%2BfaVi69FnNKDS%2FLi48%2F6UKP97gUpzxRuECRIVF3Zs1gMqLdflaNz9c55JAirNmK3jfppKxbY1YEag0qy4efBTJsoFKlBphpzeeloSFSeWLfYEKtWM44W6ElXO17iTBFSqj%2FqZozdR5Uz1tWPz9CBQaWo2j%2FpZJDpUPp%2BRgUqTYLb9jUZvaq2baaJKOUXOYnOg0hE0W%2B%2FKlfrb%2BJKVQ5xflENFOX34TfhR%2FnulAFBaPgCr791bGRZ%2BcwAAAABJRU5ErkJggg%3D%3D"/></td>
</tr>
<tr>
<td>Green Party</td>
<td>14 – 31</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAABEklEQVR42u3VzQoBURiAYTcpW7kA9%2BAiLNhgI2U5pazs1IiFJI1CIpGyYBbyd3x1NkoYf3PO1Pv0qZkpZ%2FHV24kppTzPU1%2FYH%2F2cG5eRBwXg12LycxznmyN0onpYKGBdpWt%2FfFupvLJTwK5KbxPlOgWsq%2FR8Od1XKh9ZK2BLpfeJcp0CVApQaWCr3fBRpe6szGYB85U%2BSpTrFIhGpafzgeUCJivtr%2BrPK%2BU6BQxX%2BjJRKgUiUGmlm2a%2FgJlKS51UkEq5TgFjlQZMVCbfSrBiIOxKnUEmeKUyvWWNLQPhVdqZV99KVI%2F8i0UDYVS62PY%2FSFRPc1pk18AfK51sWo1R9uNE9RTaSTlEjpJh78DblQKw1hVi4250MVS1bgAAAABJRU5ErkJggg%3D%3D"/></td>
</tr>
<tr>
<td>Liberal</td>
<td>97 – 130</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAABd0lEQVR42u2bzUvCYACH%2FXuDDmEMKQSJQLpEIUEIXaJLSIcaUZ0i6IOiTwTBwlsdbDa1tZyWrTdeMSms5t65Qc%2FDT%2FC28YwH9IXFXNctFosuqKNxdFjPLt6PjoiJL2%2B2jRPwQ0x8dF1HhCqqc7Oyz969VgzMAJVGAjM9%2FT1ROeQAlYaPlVvtl6hYJTmBIqDSMHEuzn9IVM4YH0MUUGk4tC3r10TlGgf76AIqDYE%2FJto5SSqXMQZUOlSeNtY9VcpJElDpUGkWCl4T%2FThJmkygDqg0ir91e%2BecnWIPqDRwaguZgSsVa9drOAQqDRB7Z9tPovxBBSoNllap5D9RsYepFDKBStXTzOeVJNo5SUpoKAUqVUnj5Fhhop33ZpayiAUqVcPz3q7yROWqmfm2aWIYqHRwXu5uzZl0QIl2Z29tohqo1DOtm2trLRd0n5%2FnSamkuJy4KOaBSvviXF3KPa4sG1p8aH1%2BfYFGi4sb6N6MGI%2Fmv1cKAJHlHUHllThxnsXeAAAAAElFTkSuQmCC"/></td>
</tr>
<tr>
<td>Libertarian</td>
<td>0 – 1</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAa0lEQVR42u3VMQ2AQBBE0bOEcorrMICGlUBL6CgGE1scyXsSJvmZkaSq7mMEWNJIMudUKagUUCmoFFApoFJQKaBSUCmgUkCloFJApYBKQaVAe6XPuZkDlq7UncIPKn2v3SKwaKVdqsqm0OsDZHFbBakkZqgAAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>ML</td>
<td>0 – 1</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAX0lEQVR42u3VUQ3AMAxDwQItvDIojgHw94B4NCLtDoKjp6y2SZ69C4y02t57VQoqBVQKKgVUCqgUVAqoFFQKqBRQKagUUCmgUlApoFL4XaXvOeaA0ZV6pzC60pmSuBB8VPNCy5hreF4AAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>National Citizens Alliance</td>
<td>0</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAXklEQVR42u3TMRGAUAwFwdhCFsp%2BEQVYoIuaR4uEFLsSbuYqyczcdQVYqZJ0t0vBpYBLwaWASwGXgksBl4JLAZcCLgWXAi4FXAouBVwKLgWWXfqeRw7Ye%2BnfzOgCe3zrGV0RX1CvyAAAAABJRU5ErkJggg%3D%3D"/></td>
</tr>
<tr>
<td>Nationalist</td>
<td>0</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAVklEQVR42u3TMQ0AMRADwfCnc2gsHRd%2F93XKFDMQVtrTNsnuFnjSaTszLgWXAi4FlwIuBVwKLgVcCi4FXAq4FFwKuBRwKbgUcCm4FHApcH%2FpL4ko8JQPGkmDDnWg3sQAAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>NDP-New Democratic Party</td>
<td>43 – 68</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAABWUlEQVR42u2bsUvDQBSH%2B6c6F8HJTXBxEVwKXQQXqThUhELsUFSQVgqiLjq0AQcplOIgrdC0aWxyXkhIQRFjTNJX%2FD5exuMCPz7e3YMrKKVM01SyeX9qjY%2FWdE2vSt5srAD%2BEwX9GYYh%2BRedTiNQNCpiAywVhPv6%2FElRXZOzLZIDLJXCV0WDmt1WCA%2BwdPnY1%2FvfWeqfez2X%2FABLhTZSLqiApSKYNHZ%2BtNR9GxAhYKncRko7BSxdJtbpRkxL7ZtDUgQszZ25E1NR2ilgqeizblTTyz2CBCzND%2BfR%2BK2l%2Fhhp1CdLwFKhjZRzL2Bprlgn64kt1WuJE7A0W%2BxmObGi4by3WSZRwNLMrqPd8z8qGk6SLnYJFbA0A0UfaqkoGr6YqW%2B7wx7RApamw%2Fyla9U2U1R08Wjm7ph0AUuTmtm712W3D6xqMQs%2FF%2FOkalHvoivYkbBhtS0FALF8AABVPGGAX6OOAAAAAElFTkSuQmCC"/></td>
</tr>
<tr>
<td>Parti Rhinocéros Party</td>
<td>0 – 1</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAa0lEQVR42u3VsQ2AMBAEQfffjgugDX9OhuTEBRwlEBBgpJkS7rX6lqSqxjECbKkl6b2rFFQKqBRUCqgUUCmoFFApqBRQKaBSUCmgUkCl8MNK5znNAVtX6p2CSoHXla5rWQQ2rfQTVeUA8OgGHZBeLJ6HyIUAAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>PC Party</td>
<td>0 – 1</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAXUlEQVR42u3TMRHAMBADQaM1LnMwjRBQFShKFwxf7EK4mVttk%2Bz9FBhptb33uhRcCrgUXAq4FHApuBRwKbgUcCngUnAp4FLApeBSwKXgUmDYpee8csDcS39JRIFRPpV3b3zaChvbAAAAAElFTkSuQmCC"/></td>
</tr>
<tr>
<td>People’s Party</td>
<td>1 – 10</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAA0UlEQVR42u3VPWvCYBSAUX%2B2dK0%2FwK1kaXB2EBpx6mQHF8FJNEtppyIOXSodX18oiB%2FEQYdcyjncLEmmCw%2B3k1Kq6zqdeuw%2BJyCGTn6qqjp%2BNSgmKoXQleZE8xT9ke1A6EqdU1ApcFOlu59flULoSg%2BJ5imfxhYEoSt1TkGlgErh31c6n63sCAJVut18n1XqnEKsSi8TVSmoFLi70t5DaU0QulLnFKJUOn1dNFWaP9kUtF9pU6J%2F8%2FH%2BZVnQZqUvw7frlebJ%2F6yXn1YG7VQKhLUHuS7kwVedoccAAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>Pour l’Indépendance du Québec</td>
<td>0</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAYElEQVR42u3VwQnAQAwDweu%2FHVdjuDr8VVrIKxgyU4Jg0UnS3ffeACudJFWlUlApoFJQKaBSQKWgUkCloFJApYBKQaWASgGVgkoBlcLvKp0Zc8DqSt0prK70pe42GXzsAZa3eaKwDShAAAAAAElFTkSuQmCC"/></td>
</tr>
<tr>
<td>Radical Marijuana</td>
<td>0</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAX0lEQVR42u3TMQ2AQBREwfMf3BxK6DYIoEbB0iLhFzMSXvJW2yTXeRQYabXde7sUXAq4FFwKuBRwKbgUcCm4FHAp4FJwKeBSwKXgUsCl4FJg2KXvc8sBcy%2F9S6ILzPEB1YZ4OnaSrhkAAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>Stop Climate Change</td>
<td>0</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAVklEQVR42u3TMQ0AMRADwfCnc2gsHRd%2F8QRSppiBsNKetkl2t8CTTtuZcSm4FHApuBRwKeBScCngUnAp4FLApeBSwKWAS8GlgEvBpYBLgftLf0kUgdd8TICD8nDp25MAAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>UPC</td>
<td>0</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAWklEQVR42u3TMQ0AUQgFwe%2FfDmpIkEH%2Frj0JFDMSNtmXpLtnJsBJL0lVuRRcCrgUXAq4FHApuBRwKbgUcCngUnAp4FLApeBSwKXgUuDYpbsrB9y99K%2B7dYE7Pvs%2FgglCH49BAAAAAElFTkSuQmCC"/></td>
</tr>
<tr>
<td>VCP</td>
<td>0 – 1</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAX0lEQVR42u3VMQ0AQQwDweNPJ2gihUgqP4i%2F4ooZCJZWPkm6e2YCPOkkqSqVgkoBlYJKAZUCKgWVAioFlQIqBVQKKgVUCqgUVApcr3R3zQFPV%2BpOQaXAj0ov6m6zwkUf9JRukgdiy5wAAAAASUVORK5CYII%3D"/></td>
</tr>
<tr>
<td>Independent</td>
<td>0 – 4</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAgklEQVR42u3csQnAIBRF0ey%2FjtMITqBYCPZGCGkCqfMJ54AO8OBi57HWyjnvu5SygHiOfVJKKgWVAioFlQLfVzrGsAiErtRzCnEr7b2rFEJXWm4WAZUCKgWVAioF3iuttRoFQlfqOQWVAiqF31faWrMLhK50m3OaBmJVysP1ywxEcALYtCdkW8OHSQAAAABJRU5ErkJggg%3D%3D"/></td>
</tr>
<tr>
<td>No Affiliation</td>
<td>0 – 1</td>
<td><img alt="" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATcAAAAUCAIAAABnD%2B1JAAAABmJLR0QA%2FwD%2FAP%2BgvaeTAAAAW0lEQVR42u3TQQ0AQQgEwfVvBzUkGEDF3P8U8KiS0Em%2FJN09MwFOekmqyqXgUsCl4FLApYBLwaWAS8GlgEsBl4JLAZcCLgWXAi4FlwLHLt1dOeDupT%2FdLQ0c8QHe8IEEO2Oq4wAAAABJRU5ErkJggg%3D%3D"/></td>
</tr>
</tbody>
</table>
<p>Related info</p><ul>
<li><a href="20151116T042026Z.html">2015 stochastic election 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/20190825T183857Z.htmlCounterfactual Definiteness and the EPR paradox2019-08-25T18:38:57Z2019-08-25T18:38:57Z
<p>Many articles have been written on the EPR paradox and Bell’s inequality.
I want to write down, for my own reference, what the crux of the paradox is, how it relates to a counterfactual definiteness, what the various philosophical resolutions are, and why I feel that Everett’s many worlds interpretation is the least objectionable.
By and large, I will be following Guy Blaylock’s paper “<a href="https://arxiv.org/abs/0902.3827">The EPR paradox, Bell’s inequality, and the question of locality</a>”, and you probably ought to be reading that paper instead of this blog post.
</p><p>Counterfactual definiteness is the claim that experiments that were not performed but could have been performed would have had definite outcomes if they had been performed.
For most people, counterfactual definiteness is intuitive, after all, science is all about making prediction about the outcomes of experiments that may or may not actually be performed.
However, counterfactual definiteness is problematic in the face of predictions made by quantum mechanics and special relativity as we shall see.
</p><p>Let us set up a standard EPR thought experiment.
Suppose Alice and Bob are placed very far apart from each other and at rest relative to each other and have synchronized their clocks.
They are each sent a stream of photons entangled with the other party’s stream; let us say a thousand pairs of entangled photons.
While this experiment could be analyzed with just a single pair of entangled photons, the paradox is more clear with a stream of entangled photons.
Alice and Bob simultaneously choose an angle to measure their photon streams at, and then simultaneously measure the polarization of their stream of photons at their chosen angle.
Let us say they end up choosing the same angle, which we will label as measuring at 0°.
We postulate Alice and Bob are far enough apart that all of Alice’s measurements are preformed in a space-like separated manner from all of Bob’s measurements.
Alice and Bob record the results of their measurements and travel to meet up afterward to compare notes.
</p><p>Let us say Alice tabulated the following results for her measurements: <code>+---+--+-+--+--+…</code>, where <code>+</code> means the photon was measured as parallel to the alignment of her detector and <code>-</code> means the photon was measured perpendicular to the alignment of her detector.
Bob will have recorded the following result: <code>+---+--+-+--+--+…</code>.
Their results are identical because the both performed measurements of entangled photons at the same measurement angle.
Nothing surprising here.
</p><p>But suppose, counterfactually, Alice had decided to measure her photons at an angle of 41.4° instead.
What would have happened at Alice and Bob’s meeting?
Presumably since Bob’s experiment has not changed, and his experiment was space-like separated from Alice’s experiment, his results do not depend on what experiment Alice decides to perform, so his notes would still record the result: <code>+---+--+-+--+--+…</code>.
Quantum mechanics predicts that counterfactual Alice and Bob’s results should differ in about 25% of the entries in this counterfactual scenario.
So counterfactual Alice’s notes would have perhaps recorded something like <code>-+--+--+--+-+--+…</code>, or perhaps something different.
But whatever she recorded, it would be something that differed in about 25% of the entries when compared to Bob’s result.
So far so good.
</p><p>Now suppose, counterfactually, Bob decided to measure at an angle of -41.4° and it was Alice who kept her measurement at 0°.
What would have happened at Alice and Bob’s meeting in this case?
By the same logic, Alice’s measurements at 0° would still get the result <code>+---+--+-+--+--+…</code>, and it is counterfactual Bob whose reported measurement differ in 25% of the entries.
Because counterfactual Bob measures at a negative angle, we don’t expect it to necessarily agree with the previous notes of counterfactual Alice.
Maybe counterfactual Bob’s notes would have recorded something like <code>++--++-+-+--+--+…</code>, or perhaps something different, or perhaps it might even agree the notes of counterfactual Alice.
Everything is still okay, but maybe we are getting a little nervous.
</p><p>Finally, let us suppose, counterfactually, Alice had decided to measure her photons at an angle of 41.4° and Bob had decided to measure his photons at an angle of -41.4°.
What would have happened at Alice and Bob’s meeting in this case?
Alice and Bob’s experiments are space-like separated so neither of their choices should influence the outcomes of each other’s experiments.
Presumably Alice’s notes would be the same as what we wrote above for counterfactual Alice’s notes: <code>-+--+--+--+-+--+…</code>.
Similarly Bob’s notes would be the same as what we wrote above for counterfactual Bob’s notes: <code>++--++-+-+--+--+…</code>.
Here is the crux of the EPR paradox.
Quantum mechanics predicts that counterfactual Alice and counterfactual Bob’s notes ought to differ in approximately 87.5% of the entries in this scenario!
But no matter how we rearrange counterfactual Alice and counterfactual Bob’s notes, they can only differ between 0% and 50% of their entries on average.
This is what it means for Bell’s inequality to be violated.
</p><p>Clearly something is wrong in our naive description of the hypothetical experiments above.
What are some proposed philosophical resolutions to this EPR paradox?
</p><p>One possible resolution is that Alice’s choice in her measurement does somehow affect the outcome of Bob’s experiment!
The problem with this is that Alice and Bob’s experiments are space-like separated.
This implies that an observer traveling rapidly towards Bob and away from Alice will observe that Bob’s experiments conclude before Alice even begins her experiment when she makes her choice to whether to measure at angle 0° or 41.4°.
According to this resolution, this observer sees Alice’s choices affecting the outcome of already completed experiments!
</p><p>A symmetric possible resolution is that it is Bob’s choice in his measurement that affects the outcome of Alice’s experiment.
But we have the same issue as above.
There still exists an observer, this time traveling towards Alice and away from Bob, who observes that Alice completes her experiments before Bob begins his experiment.
</p><p>Non-local interpretations of quantum mechanics, including the Copenhagen interpretation and hidden variable interpretations such as pilot wave theory, resolve the EPR paradox in the above manner.
They suggest there is some special global reference frame that is used to absolutely decide which of Alice and Bob’s experiments are performed first and whichever experiment comes first is this special reference frame is the one whose outcome affects the other’s experiment.
They suggest that the rest of the laws of physics conspire to keep all agents in the dark about which reference frame is this special global reference frame, as
there are no experiments that can determine which reference frame is the special one.
In particular, we cannot acutally perform an experiment where we go back in time to see would have happened if Alice or Bob had choosen a different angle of measurement.
</p><p>Furthermore, in general relativity, I suspect it is more difficult, and probably impossible, to come up with any globally consistent universal reference frame to resolve the order of all events.
</p><p>Of course, it could also be the case that both Alice and Bob’s choice affect the outcome of each other’s experiments.
But this only makes the problem worse as it would mean that in every reference frame there are future events affecting past outcomes.
</p><p>Another resolution to the EPR paradox is that Alice and Bob could not have chosen different angles of polarization; if they both measure at angle 0° then that is the only choice they could have made and Alice and Bob do not have free choices in the matter.
This resolution is called superdeterminism.
We can make our thought experiment more extreme by taking Alice and Bob’s free choice out of the picture.
Instead we have Alice first measures the polarization of a <abbr title="Cosmic Microwave Background">CMB</abbr> photon coming from the constellation Leo and chose her measurement setting, 0° or 41.4°, based on the outcome of that measurement.
We have Bob measure the polarization of a <abbr title="Cosmic Microwave Background">CMB</abbr> photon from Aquarius on the opposite side of the visible universe to chose his setting, 0° or -41.4°.
Now superdeterminism requires that the universe has been conspiring since near the beginning of time so that the plasma of the early universe would cause two photons photons to be released and travel for 13 billion years to a point where life developed and would be setting up a quantum correlation experiment and pass through their measuring devices in such a way to force them to align their measurement settings to get exactly the correlation in their records that is predicted by quantum mechanics.
</p><p>Furthermore, in a superdeterminstic world there could be arbitrarily extreme violations of Bell inequalities, even beyond the violations predicted by quantum mechanics.
Yet the cosmic conspiracy chooses never to produce statisitical results that exceed the Bell-style voilations predicted by quantum mechanics for some reason.
</p><p>A third resolution to the EPR paradox is to say that the question of what would have happened if Alice or Bob had done a different experiment is not a well-formed question.
This is the resolution captured by the “shut-up and calculate” interpretation of quantum mechanics.
There is not much else to say about this resolution beyond saying that I do not find the rejection of the very question to be particularly satisfying.
</p><p>Lastly we come to Everett’s many world interpretation.
This interpretation resolves the EPR paradox by saying that all possible experimental outcomes of Alice and Bob’s experiment all happen and they exist together in a superposition.
The phase of Alice and Bob’s superposition changes based on the polarization they choose to make their measurements with, but no matter their measurement choice, all 2<sup>1000</sup> possible outcomes of Alice experiment happen and exist together and similarly for Bob.
Later, when Alice and Bob meet to compare their notes, the superposition of Alices and the superposition of Bobs interfere with each other and split up in such a way that "most" of the Alices meet up with a version of Bob whose recorded outcomes have the correlations predicted by the quantum mechanics (or in the case of perfect phase alignment "all" of the Alices meet up with the corresponding Bob who has identical recorded noted).
</p><p>This resolution violates counterfactual determinism because it does not predict any specific outcome for counterfactual Alice. It predicts a similar superposition of Alices but in a different phase. In that situation, the various Bobs in superposition could have met up with any number of possible different counterfactual Alices when they interfered.
Furthermore, the different phase that the counterfactual Bobs would have been in would definitely influence this interference when meeting up with the superpositions of counterfactual Alices.
It is not the case that Bob’s experimental choices affects Alice’s results, but his choices does affect the interference that happens when Alice and Bob meet, and does influence which version of the superposition of Alices he (or rather they) meet up with.
</p><p>The many worlds interpretation is not without its own problems. If multiple words are all equally as real, why is it that we assign less probability to those worlds with the lesser probability amplitudes. After all, those words are, in some sense, just as real as the worlds associated with larger probability amplitudes.
A better way of phrasing the problem might be: why is it rational to behave as if we expect outcomes with probability in accordance to the probability amplitudes of quantum mechanics?
</p>http://r6.ca/blog/20190223T161625Z.htmlHow can basic arithmetic make a self-referential sentence?2019-02-23T16:16:25Z2019-02-23T16:16:25Z
<p>On <a href="https://news.ycombinator.com/item?id=19177384">Hacker news</a>, imh asks,
</p><blockquote>
<p>I never understood the step about how a system that can do basic arithmetic can express the "I am not provable in F" sentence. Does anyone have an ELI30 version of that?</p>
</blockquote>
<p>I think this is a great question and I would like to try to answer it.
</p><p>First of all, it is important to understand that we have quite a bit more than just basic arithmetic.
Let us define basic arithmetic as a language with symbols for the constants <code>0</code> and <code>1</code>, the operations for <code>+</code> and <code>×</code>, and the <code>=</code> relation (anything similar to this will work as well).
</p><p>On top of basic arithemetic we add the language of first-order logic.
That is we add logical operations for <code>and</code>, <code>or</code>, <code>not</code>, etc., we add an infinite number of logical variables <code>x</code>, <code>y</code>, etc., and we add universal quantification, <code>∀</code>, and existential quantification, <code>∃</code>.
</p><p>We provide logical and arithmetic axioms that defines these symbols to be our usual interpretation of them.
The domain of the quantifiers is implicit in first-order logic.
We intend our domain to be the natural numbers, and our axioms are compatible with this interpretation.
Technically there will be other valid interpretations of our axioms, but that will not matter for our purposes today.
</p><p>Our language of first-order logic over basic arithmetic is vastly more expressive than basic arithmetic alone.
Building a formula in this language that expresses “I am not provable in F” requires three key ingredients.
</p><p class="header">Cantor pairing function
</p><p>The first ingredient is the ability to define data structures.
To do this, I will be using the <a href="https://en.wikipedia.org/w/index.php?title=Pairing_function&oldid=853876462#Cantor_pairing_function">Cantor pairing function</a>,
to define a functional relation that maps ordered pairs of natural numbers to a single natural number:
</p><pre>Pair(x, y, p) := p = ((x + y + 1) × (x + y)) ÷ 2 + y</pre>
<p>To encode a pair of numbers, say 2 and 3, we plug them into the <code>x</code>, <code>y</code> parameters.
Then the variable <code>p</code> is forced to be the value 18, which represents the ordered pair, ⟨2, 3⟩.
To decode a number, say 7, we plug it into the <code>p</code> parameter.
Then the variables <code>x</code>, and <code>y</code>, which are natural numbers, are forced to be the values 2 and 1, which is the ordered pair that 7 represents.
</p><p>We have a problem that the our definition of <code>Pair</code> does not quite fit our definition of basic arithemtic because of the <code>÷</code> operator.
However this is easily fixed by providing an equivalent definition that does not use <code>÷</code>.
</p><pre>Pair(x, y, p) := 2 × p = (x + y + 1) × (x + y) + 2 × y</pre>
<p>where <code>2 := 1 + 1</code> (in general we will let <code><var>n</var></code> denote the sum of <var>n</var> occurances of the numeral <code>1</code>).
</p><p>Using first-order logic we can compose this ‘<code>Pair</code>’ relation to encode and decode nested pairs and start building fancy data structures that you find in computer programming.
In particular, we can build data structures like lists or structures for the language of basic arithmetic or the language of first-order logic.
For example we may choose to represent a formula from basic arithemetic with the following recursive structure.
</p><pre>⸢0⸣ := ⟨0, 0⟩
⸢1⸣ := ⟨1, 0⟩
⸢X + Y⸣ := ⟨2, ⟨⸢X⸣, ⸢Y⸣⟩⟩
⸢X × Y⸣ := ⟨3, ⟨⸢X⸣, ⸢Y⸣⟩⟩
⸢X = Y⸣ := ⟨4, ⟨⸢X⸣, ⸢Y⸣⟩⟩</pre>
<p>By using the Cantor pairing function, we can encode and decode these sturctures, letting us represent any basic arithemetic formula as a single natural number.
</p><p>I should note that Gödel did not use the Cantor pairing function, and instead use prime decomposition.
However, the computer scientist in me perfers the pairing function, and it has a simpler arithmetic relation that defines the encoding.
</p><p class="header">Gödel’s β function
</p><p>The second ingredient is Gödel’s β function.
While the Cantor pairing function can be use to build lists, the problem is that it only possible to access fixed location of that list.
The β function encodes lists in such a way that it is easy to access a variable locations within the list.
The β function is defined as
</p><pre>β(x, y, i) := x mod (1 + (i + 1) × y)</pre>
<p>Gödel’s β funciton lets us encode a list of numbers, <code>a</code><sub>0</sub>, <code>a</code><sub>1</sub>, ..., <code>a</code><sub><code>n</code></sub> with a pair of numbers <code>x</code> and <code>y</code>.
in such a way that for all <code>i</code> less than <code>n</code>, the <code>β(x, y, i) = a<sub>i</sub></code>.
It is possible to choose <code>y</code>’s value to find arbitrarly large and arbitrarily long arithemetic sequences of mutually coprime numbers.
Then, given a sufficent <code>y</code> value, the Chinese remainder theorem lets us encode the content of the list as a single value <code>x</code>.
</p><p>Below we define β as functional arithemetic relation.
</p><pre>BETA(x, y, i, a) := ∃q. x = q × (1 + (i + 1) × y) + a and ∃z. a + z = (i + 1) × y</pre>
<p><code>BETA</code> is defined so that <code>BETA(x, y, i, a)</code> holds if and only if <code>β(x, y, i) = a</code>.
</p><p>Using the Cantor pairing function we could pair up the values <code>x</code> and <code>y</code> and <code>n</code> into a single number that represents any list of numbers.
Using this new ability we can now define a structure that represents a trace for arbitrary computations.
For example we can define a relation that defines the substitutions for our encoding of formulas of first-order logic.
</p><pre>SUB(f, i, t, a) := “there exists a trace of the computation of substituting the arithmetic term encoded by t<br/>into the variable labeled by i within the formula f and the result of that computation is a.”</pre>
<p>the result being that the functional relation <code>SUB(⸢φ⸣, i, ⸢t⸣, a)</code> that holds if and only if <code>a</code> equals <code>⸢φ[x<sub>i</sub>↦t]⸣</code>.
</p><p>Similarly we can define a functional relation <code>CODE(x, y)</code> such that it holds if an only if <code>y</code> equals ⸢1 + 1 + … + 1⸣ where there are <code>x</code> number of occurances of <code>1</code>. We can also define predicate <code>PROVABLE_IN_F(x)</code> that defines what it means for an encoding of a formula to be provable in some axiomatic system <var>F</var>, as long as it is decidable what the axioms of <var>F</var> are.
</p><p class="header">Quines
</p><p>We now have a basic idea how we can specify datastructures and computations of those data structures using arithemtic.
But how do we build a self-referential formula?
While we can define arbitrary computations using first-order logic, it is not like we can write a computer program with a variable that has a contains a copy of the entire program itself.
Or can we?
</p><p>A <a href="https://en.wikipedia.org/w/index.php?title=Quine_(computing)&oldid=881902282">Quine</a> is a program that that prints out its own source code.
However, it is just as easy to write a program that creates a variable contains the entire source code of program itself; a self-referential program!
The technique to do this is the same as found in the proof of Kleene’s recursion theorems, and the implementation of the <a href="https://en.wikipedia.org/wiki/Fixed-point_combinator#Fixed_point_combinators_in_lambda_calculus">Y Combinator</a>.
In this way we can build self-referential arithemtic formulas.
</p><p>Theorem. For any formula <code>ψ(y)</code>, there exists a formula <code>φ</code> such that <code>φ</code> is equivalent to <code>ψ(⸢φ⸣)</code>.
</p><p>In other words, if we have a formula with a free variable <code>y</code>, we can build a self-referential formula by subsituting that variable with the encoding of the resulting formula.
Like the <a href="https://en.wikipedia.org/wiki/Fixed-point_combinator#Fixed_point_combinators_in_lambda_calculus">Y Combinator</a>, the proof of this theorem is both short and confusing.
</p><p>Proof.
Let <code>θ := ∃y. ψ(y) and ∃z. SUB(x<sub>0</sub>, 0, z, y) and CODE(x<sub>0</sub>, z)</code>.
Let <code>φ := θ[x<sub>0</sub>↦⸢θ⸣]</code>.
Then <code>φ</code> is equal to <code>∃y. ψ(y) and ∃z. SUB(⸢θ⸣, 0, z, y) and CODE(⸢θ⸣, z)</code>.
By the property of <code>CODE</code>, the variable <code>z</code>, must be equal to <code>⸢⸢θ⸣⸣</code>,
and by the property of <code>SUB</code>, the variable <code>y</code>, must be equal to <code>⸢θ[x<sub>0</sub>↦⸢θ⸣]⸣</code>, which is equal to <code>⸢φ⸣</code>.
Thus <code>φ</code> is equivalent to <code>ψ(⸢φ⸣)</code>.
Qed.
</p><p>Now we can finally build the self-referential Gödel formula by applying <code>ψ(y) := not (PROVABLE_IN_F(y))</code> to the above theroem to get a formula <code>φ</code> such that <code>φ</code> is equivalent to <code>not (PROVABLE_IN_F(⸢φ⸣))</code>.
</p>http://r6.ca/blog/20180225T160548Z.htmlWhy Is It Taking 20 Minutes to Mine This Bitcoin Block?2018-02-25T16:05:48Z2018-02-25T16:05:48Z
<p>Does this sound familiar?
</p><p>You have just made a Bitcoin transaction and you are eager to see if it appears in the next block.
You know that the expected time between Bitcoin blocks is 10 minutes.
You check the log of your Bitcoin node.
It has been 7 minutes since the previous block.
You recall that blocks occurrences in Bitcoin are a Poisson process, which is memoryless.
Even though it has been 7 minutes since the previous block, you still expect to wait another 10 minutes.
</p><p>Five minutes pass.
No new blocks have appeared.
You have been staring at your Bitcoin node’s log this entire time.
It has now been 12 minutes since the previous block.
All your waiting has not changed anything.
Even though you have been waiting for 5 minutes, the math says that you are still expected to wait 10 minutes before the next block will appear.
A Poisson process is memoryless.
</p><p>After staring at your Bitcoin node’s log for a further 8 minutes, you finally see a new block.
“I swear that this always happens to me,” you say to yourself.
“Whenever I’m waiting for my transaction to be confirmed, it always seems that the particular block I’m waiting for takes like 20 minutes to mine.”
</p><p>My friend, if this has happened to you, you are not alone.
This phenomenon is real.
</p><p>Under the simplifying assumption that Bitcoin’s hashrate is constant, we know that a new block is mined once every 10 minutes on average, and this mining process can be well modeled by a Poisson process.
Because Poisson processes are memoryless, at any given time we always expect that the next block will appear, on average, in 10 minutes.
This holds no matter how long we have already been waiting.
This memorylessness property applies just as well backwards in time as it does forwards in time.
That is, if you pick a random point in time, on average, the previous block will have been mined 10 minutes earlier.
</p><p>This is clear because if you sample a series of events from a Poisson process and take a second sample and reverse the occurrences of that series of events, the two samples will be indistinguishable.
Therefore, by this symmetry, it must be the case that when you pick a random point in time, the expected time until the next event is the same as the expected time since the previous event.
</p><p><i>“Wait a minute.
You are saying that, if I pick a random point in time, we expect the previous block to have been mined 10 minutes in the past, and we expect that the next block will be mined 10 minutes in the future.
Doesn’t that mean that we expect a total of 20 minutes between blocks?”</i>
</p><p>Correct, that is exactly what I am saying.
If you pick a random point in time, you expect 20 minutes between the previous block and the next block on average.
</p><p><i>“That cannot be true because we know that there are, on average, 10 minutes between blocks, not 20 minutes.”</i>
</p><p>This apparent paradox is essentially the same as the <a title="How long will you wait hitchhiking on the road?" href="https://the8layers.com/2016/10/30/how-long-will-you-wait-hitchhiking-on-the-road/">hitchhiker’s paradox</a>.
To resolve this paradox we need to understand that the question, “What is the expected time between blocks?” is underspecified.
To compute an expected value we need to know which distribution we are computing the expected value with respect to.
</p><p>Suppose we observe the Bitcoin blockchain for a while, and we make a list of the time between each successive block.
When we average this list of numbers, we will get a value that is <a href="https://twitter.com/pwuille/status/1098651788343955456">close to 10 minutes</a>.
Averaging this way corresponds to a distribution where each block interval is sampled with equal probability.
</p><p>More precisely, the <abbr title="probability density function">pdf</abbr> for this distribution of non-negative interval durations is the exponential distribution pdf<sub>1</sub>(<var>t</var>) = <var>N</var><sub>1</sub> <b>e</b><sup>−<var>λ</var> <var>t</var></sup>, where <var>λ</var> is 0.1 min<sup>-1</sup>, Bitcoin’s block rate, and where <var>N</var><sub>1</sub> is a normalization constant (which in this case is also 0.1 min<sup>-1</sup>).
The expected value of this distribution is ∫<var>t</var> pdf<sub>1</sub>(<var>t</var>) d<var>t</var> = 10 min.
</p><div class="figure"><img alt="graph of (0.1*exp(-0.1*x)" src="images/1bfb4335d3c0d5d90efb4c39fd9b1242671353ea663abd315d351c64efb990ac.svg"/><br/>pdf<sub>1</sub>: exponential distribution</div>
<p>Suppose we observe the Bitcoin blockchain for a while, and every day we write down the duration of the block whose interval crosses the 9:00 am mark.
When we average this list of numbers, we will get a value that is close to 20 minutes.
Averaging this way corresponds to a distribution where each block interval is sampled, not with equal probability, but proportional to how long the interval lasts.
For example, we are twice as likely to sample an interval that lasts for 14 minutes than we are to sample an interval that lasts for 7 minutes simply by virtue of the fact that 14 minute intervals last twice as long as 7 minute intervals.
</p><p>We can take the <abbr title="probability density function">pdf</abbr> for the exponential distribution above and multiply it by a linear factor to reweight the probabilities in accordance with how long the interval is.
After normalization, the resulting <abbr title="probability density function">pdf</abbr> for this distribution is the gamma distribution (which shape parameter 2) pdf<sub>2</sub>(<var>t</var>) = <var>N</var><sub>2</sub> <var>t</var> <b>e</b><sup>−<var>λ</var> <var>t</var></sup> (whose normalization constant <var>N</var><sub>2</sub> is 0.01 min<sup>-2</sup>).
The expected value of this distribution is ∫<var>t</var> pdf<sub>2</sub>(<var>t</var>) d<var>t</var> = 20 min.
</p><div class="figure"><img alt="graph of (0.01*x*exp(-0.1*x)" src="images/8a44ba1ae657b45020b86f8bb66534a770c19be4d76dab8e69ae572f3042c59c.svg"/><br/>pdf<sub>2</sub>: gamma distribution with shape parameter 2</div>
<p>We can double-check this result by recalling the time reversing symmetry argument above.
When we pick a random point in time, the time until the next block is some random variable <var>X</var> whose <abbr title="probability density function">pdf</abbr> is pdf<sub>1</sub>, and the time since the previous block is a random variable <var>Y</var> whose <abbr title="probability density function">pdf</abbr> is also pdf<sub>1</sub>.
Therefore, the total time between the last block and the next block is the random value <var>X</var> + <var>Y</var>.
We can compute the distribution for this sum by taking the convolution of pdf<sub>1</sub> with itself, and we indeed get pdf<sub>2</sub> as a result.
</p><p>The bias towards picking longer blocks intervals by using the second sampling method accounts for the discrepancy between the two different results when computing average block interval durations.
However, the word “bias” is not meant to be pejorative.
This other sampling method is not incorrect or with prejudice; it is simply a different way of sampling.
The distribution of intervals you need to use depends on the application you are using it for.
If you want to compute the throughput of the Bitcoin, you will need to use the exponential distribution.
If you want to know “why is does it take 20 minutes to mine the Bitcoin block with my transaction in it?”, you need to use this gamma distribution.
</p>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>