nomeata’s mind shares
http://www.joachim-breitner.de//blog
Joachim Breitners Denkblogadehttp://joachim-breitner.de/avatars/avatar_128.pngnomeata’s mind shares
http://www.joachim-breitner.de//blog
128128Swing Dancer Profile
http://www.joachim-breitner.de/blog/746-Swing_Dancer_Profile
http://www.joachim-breitner.de/blog/746-Swing_Dancer_Profilehttp://www.joachim-breitner.de/blog/746-Swing_Dancer_Profile#commentsmail@joachim-breitner.de (Joachim Breitner)<p>During my two years in Philadelphia (I was a post-doc with <a href="http://www.seas.upenn.edu/~sweirich/">Stephanie Weirich at the University of Pennsylvania</a>) I danced a lot of Swing, in particular at the weekly social “<a href="https://www.jazzattackswings.com/">Jazz Attack</a>”.</p>
<p>They run a blog, that blog features dancers, and this week – just in time for my last dance – they <a href="https://www.jazzattackswings.com/blog/community-spotlight-joachim/">featured me with a short interview</a>.</p>Tue, 07 Aug 2018 12:16:14 -0400The merits of a yellow-red phase
http://www.joachim-breitner.de/blog/745-The_merits_of_a_yellow-red_phase
http://www.joachim-breitner.de/blog/745-The_merits_of_a_yellow-red_phasehttp://www.joachim-breitner.de/blog/745-The_merits_of_a_yellow-red_phase#commentsmail@joachim-breitner.de (Joachim Breitner)<p>In my yesterday <a href="/blog/744">post on Continuity Lines in North America</a> I mentioned in passing that I am big fan of German<a href="#fn1" class="footnoteRef" id="fnref1"><sup>1</sup></a> traffic lights, which have a brief yellow-red phase between the red and and the green phase (3 to 5 seconds, depending on road speed). A German reader of my blog was surprised by this, said that he considers it pointless, and would like to hear my reasons. So where we go…</p>
<h3 id="life-without-yellow-red">Life without Yellow-Red</h3>
<p>Lights that switch directly from red to green cause more stress. Picture yourself at the first car waiting at a traffic light, with a bunch of cars behind you. Can you relax, maybe observe the cars passing in front of you, switch the radio station, or simply look somewhere else for a moment? Well, you can, but you risk missing how the light switches from red to green. When your look at the traffic light again and see it bright green, you have no idea how long it has been on green. Hyper-aware of all the cars behind you waiting to get going, you’ll rush to get started, and if you don’t do that really fast now, surely one of the people waiting behind you will have honked.</p>
<p>So at the next intersection, you better don’t take your eyes off the light – or, alternatively, you develop a screw-you-I-don’t-care-attitude towards the other cars, which might allow you to relax in this situation, but is in general not desirable.</p>
<p>Maybe this is less of a problem on the West Coast, where supposedly everybody is nice, relaxed, and patient, and you can take all the time you want to get rolling. But in the stereotypical East Coast traffic full of angry, impatient and antisocial drivers, you really don’t get away with that.</p>
<h3 id="life-with-yellow-red">Life with Yellow-Red</h3>
<p>The yellow-red phase solves this problem elegantly: As long as the light is red, you don’t have to watch the light constantly and with maximum attention. You can relax: it suffices to check it often enough to catch the red-yellow phase, once every two or three seconds. When you see it, you get ready to start; and when it actually turns green, you start on time.</p>
<p>I would expect that it is not only less stressful, it is also more efficient: Because every car in the lane has the heads-up warning “green in a moment”, the cars can start rolling in quicker succession. Without the warning, every car to account much more for the possible slower reaction of the car before.</p>
<p>PS: A friend of mine wonders whether the German Yellow-Red is needed because cars with manual transmissions are much more common in Germany than in the US, and you need more time to, well, get into gear with these cars.</p>
<div class="footnotes">
<hr/>
<ol>
<li id="fn1"><p>Also Great Britain, Croatia, Latvia, Norway, Austria, Poland, Russia, Saudi-Arabia, Sweden, Switzerland, Hungary and others.<a href="#fnref1">↩</a></p></li>
</ol>
</div>Mon, 30 Jul 2018 17:41:44 -0400Continuity Lines
http://www.joachim-breitner.de/blog/744-Continuity_Lines
http://www.joachim-breitner.de/blog/744-Continuity_Lineshttp://www.joachim-breitner.de/blog/744-Continuity_Lines#commentsmail@joachim-breitner.de (Joachim Breitner)<p>I am currently on a road trip going from Philly going North along the Atlantic Coast into Canada, and aiming for Nova Scotia. When I passed from the US into Canada, I made had an unexpected emotional response to the highways there: I felt more at home!</p>
<p>And I believe it has to do with the pavement markings on US vs. Canadian freeways.</p>
<p>Consider this image, taken from the <em>Manual on Uniform Traffic Control Devices</em> of the United States, an official document describing (among other things) <a href="https://mutcd.fhwa.dot.gov/services/publications/fhwaop02090/fwymarkings_lgview.htm">how the pavement of a freeway ought to be paved</a>:</p>
<div class="figure">
<img src="//www.joachim-breitner.de/various/exit-lane-us.png" alt="Parallel Deceleration Lane for Exit Ramp"/>
<p class="caption">Parallel Deceleration Lane for Exit Ramp</p>
</div>
<p>This is a typical exit ramp from the freeway. On ramps and cloverleaf ramps look similar. Note that the right-most lane goes somewhere else than the left and the middle lane, yet the lanes look completely identical. In particular, the lines between the lanes are shaped the same!</p>
<p>Now, for comparison, the corresponding image in a Canadian manual, namely the <a href="https://www2.gov.bc.ca/assets/gov/driving-and-transportation/transportation-infrastructure/engineering-standards-and-guidelines/traffic-engineering-and-safety/traffic-engineering/traffic-signs-and-pavement-markings/manual_signs_pavement_marking.pdf"><em>Manual of Standard Traffic Signs & Pavement Markings</em> for British Columbia</a>:</p>
<div class="figure">
<img src="//www.joachim-breitner.de/various/exit-lane-ca.png" alt="Canadian off-ramps"/>
<p class="caption">Canadian off-ramps</p>
</div>
<p>Here, there are <em>different</em> lines between the different lanes: normal lane lines left, but a so-called <em>continuity line</em>, with a distinctly different pattern, between the normal lanes and the exit lane. It’s like in Germany!</p>
<p>With this is mind I understand one reason<a href="#fn1" class="footnoteRef" id="fnref1"><sup>1</sup></a> why driving in the US<a href="#fn2" class="footnoteRef" id="fnref2"><sup>2</sup></a> noticeably more stressful: There is just always anxiety whether you are accidentally in an exit lane!</p>
<p><strong>Update (2018-07-30)</strong>: AS Paul Johnson pointed out (see comment below), I was looking at an old version of the MUTCD. The <a href="https://mutcd.fhwa.dot.gov/pdfs/2009r1r2/pdf_index.htm">current version, from 2009</a>, has these lines:</p>
<div class="figure">
<img src="//www.joachim-breitner.de/various/exit-lane-us2.png" alt="Current US off-ramps"/>
<p class="caption">Current US off-ramps</p>
</div>
<p>They have published a (very long) document describing the <a href="http://edocket.access.gpo.gov/2009/pdf/E9-28322.pdf">changes in the new version of the manual</a> , and Section 306 describes the rationale:</p>
<blockquote>
<p>[..] the FHWA adopts language to clarify that dotted lane lines, rather than broken lane lines, are to be used for non-continuing lanes, including acceleration lanes, deceleration lanes, and auxiliary lanes. [..] a number of States and other jurisdictions currently follow this practice, which is also the standard practice in Europe and most other developed countries. The FHWA believes that the existing use of a normal broken lane line for these non- continuing lanes does not adequately inform road users of the lack of lane continuity ahead and that the standardized use of dotted lane lines for non-continuing lanes as adopted in this final rule will better serve this important purpose in enhancing safety and uniformity.</p>
</blockquote>
<p>So all is well! But it means that either Pennsylvania was slower than allowed in implementing these changes (the deadline was December 2016), or it was something else alltogether that made me feel more at home on the Canadian freeway.</p>
<div class="footnotes">
<hr/>
<ol>
<li id="fn1"><p>I say “one reason”, not “the reason”, because there are many more – “Rechtsfahrgebot”, no red-and-yellow-phase in the traffic light, Pennsylvanian road quality…<a href="#fnref1">↩</a></p></li>
<li id="fn2"><p>Supposedly, Pennsylvania is particularly bad with roads in general, but also with this particular problem, and California has exit lanes clearly separated. But, of course, because this is the US, not using the same patter as the others (Canada, Europe), but using spaced dots…<a href="#fnref2">↩</a></p></li>
</ol>
</div>Sun, 29 Jul 2018 20:25:07 -0400Build tool semantic aware build systems
http://www.joachim-breitner.de/blog/743-Build_tool_semantic_aware_build_systems
http://www.joachim-breitner.de/blog/743-Build_tool_semantic_aware_build_systemshttp://www.joachim-breitner.de/blog/743-Build_tool_semantic_aware_build_systems#commentsmail@joachim-breitner.de (Joachim Breitner)<p>I just had a lovely visit at Ben Gamari and Laura Dietz, and at the breakfast table we had an idea that I want to record here.</p>
<h3 id="the-problem">The problem</h3>
<p>Laura and Ben talked about the struggles they had using build systems like <code>make</code> or <a href="http://nixos.org/nix/">Nix</a> in data science applications. A build system like nix is designed around the idea that builds are relatively cheap, and that any change in a dependency ought to trigger a rebuild, just to be sure that all build outputs are up-to-date. This is a perfectly valid assumption when building software, where build times are usually minutes, or maybe hours. But when some of the data processing takes days, then you really really want to avoid any unnecessary builds.</p>
<p>One way of avoiding unnecessary rebuilds that is supported by build systems like <a href="https://shakebuild.com/"><code>shake</code></a> and (I presume, maybe with some extra work) Nix, is to do output hashing: If one build stage has its input changed and need to be re-run, but its <em>output</em> is actually unchanged, then later build stages do not have to be re-run. Great!</p>
<p>But even with this feature in place, there one common problem remains: Build tools! Your multi-gigabyte data is going to be processed by some code you write. What if the code changes? Clearly, if you change the algorithm, or fix a bug in your code, you want the output to be re-run. But if you just change some strings in the <code>--help</code> flag, or update some libraries, or do something else that does <em>not</em> change the program in a way that is significant for the task at hand, wouldn’t you prefer to not pay for that by futile multi-day data processing step?</p>
<h3 id="existing-approaches">Existing approaches</h3>
<p>There are various ways you can tackle this these days:</p>
<ul>
<li><p>You bite the bullet, add the build tool as a dependency of the processing step. You get the assurance that your data always reflects the output of the latest version of your tool, but you get lots of rebuilds.</p></li>
<li><p>You don’t track the tool as part of your build system. It is now completely up to you to decide when the tool has changed in significant ways. When you think it has, you throw away all build artifacts and start from scratch. Very crude, and easy to get wrong.</p></li>
<li><p>You keep track of a “build tool version”, e.g. a text file with a number, that you depend on in lieu of the build tool itself. When you make a change that you think is significant, you bump that version number. This is similar to the previous approach, but more precise: Only the build outputs that used this particular tools will be invalidated, and it also scales better to working in a team. But of course, you can still easily get it wrong.</p></li>
</ul>
<h3 id="build-tool-semantics">Build tool semantics</h3>
<p>Why are all these approaches so unsatisfying? Because none allow you to express the <em>intent</em>, which is to say “this build step depends on the <em>semantics</em> (i.e. behaviour) of the build tool”. If we could somehow specify that, then all would be great: Build tool changes, but its semantics is unaffected? no rebuild. Build tool changes, semantics change? rebuild.</p>
<p>This ideal is not reachable (blah blah halting problem blah blah) – but I believe we can approximate it. At least if good practices were used and the tool has a test suite!</p>
<p>Assume for now that the tool is a simple patch-processing tool, i.e. takes some input and produces some output. Assume further that there is a test suite with a small but representative set of example inputs, or maybe some randomly generated inputs (using a fixed seed). If the test suite is good, then <strong>the <em>(hash of)</em> the output on the test suite example is an approximation of the programs semantic</strong>.</p>
<p>And the build system can use this “semantics hash”. If the build tool changes, the build system can re-run the test suite and compare the output with the previous run. If they change, then the tools seems to have changed in significant ways, and it needs to re-run the data processing. But if the test suite outputs are unchanged, then it can assume that the behaviour of the tool has not changed, re-use the existing data outputs.</p>
<p>That is the core idea! A few additional thoughts, though:</p>
<ul>
<li>What if the test suite changes? If the above idea is implemented naively, then adding a test case to the test suite will change the semantics, and re-build everything. That would be horrible in terms of incentives! So instead, the build systems should keep the old version of the build tool around, re-calculate its semantics hash based on the new test suite, and then compare that. This way, extending the test suite does not cause recompilation.</li>
</ul>
<p>Hash-and-store-based build systems like Nix should have no problem keeping the previous version of the build tool around as long there is output that depends on it.</p>
<ul>
<li><p>A consequence of this approach is that if you find and fix a bug in your tool that is not covered by the existing test suite, then you absolutely have to add a test for that to your test suite, otherwise the bug fix will not actually make it to your data output. This might be the biggest downside of the approach, but at least it sets incentives right in that it makes you maintain a good regression test suite.</p></li>
<li><p>What if things go wrong, the test suite is incomplete and the build system re-uses build output because it wrongly assumes that two versions of the build tool have the same semantics?</p></li>
</ul>
<p>If done right, this can be detected and fixed: The build system needs to record which tool version (and not just which “semantics hash”) was used to produce a particular output. So once the test suite uncovers the difference, the build systems will no longer consider the two versions equivalent and – after the fact – invalidate the re-used of the previous build output, and re-build what needs to be rebuild</p>
<p>I am curious to hear if anybody has played with these or similar ideas before? How did it go? Would it be possible to implement this in Nix? In Shake? Other systems? Tell me your thoughts!</p>Sat, 28 Jul 2018 11:03:31 -0400WebGL, Fragment Shader, GHCJS and reflex-dom
http://www.joachim-breitner.de/blog/742-WebGL%2C_Fragment_Shader%2C_GHCJS_and_reflex-dom
http://www.joachim-breitner.de/blog/742-WebGL%2C_Fragment_Shader%2C_GHCJS_and_reflex-domhttp://www.joachim-breitner.de/blog/742-WebGL%2C_Fragment_Shader%2C_GHCJS_and_reflex-dom#commentsmail@joachim-breitner.de (Joachim Breitner)<p>What a potpourri of topics... too long to read? <a href="https://nomeata.github.io/reflex-dom-fragment-shader-canvas/">Click here!</a></p>
<p>On the side and very slowly I am working on a little game that involves breeding spherical patterns… more on that later (maybe). I want to implement it in Haskell, but have it run in the browser, so I reached for GHCJS, the Haskell-to-Javascript compiler.</p>
<h2 id="webgl-for-2d-images">WebGL for 2D images</h2>
<p>A crucial question was: How do I draw a generative pattern onto a HTML <code>canvas</code> element. My first attempt was to calculate the pixel data into a bit array and use <a href="https://developer.mozilla.org/en-US/docs/Web/API/CanvasRenderingContext2D/putImageData"><code>putImageData()</code></a> to push it onto the canvas, but it was prohibitively slow. I might have done something stupid along the way, and some optimization might have helped, but I figured that I should not myself calculate the colors of each pixel, but leave this to who is best at it: The browser and (ideally) the graphic card.</p>
<p>So I took this as an opportunity to learn about WebGL, in particular fragment shaders. The term shader is misleading, and should mentally be replaced with “program”, because it is no longer (just) about shading. WebGL is intended to do 3D graphics, and one sends a bunch of coordinates for triangles, a vertex shader and a fragment shader to the browser. The vertex shader can places the vertices, while the fragment shader colors each pixel on the visible triangles. This is a gross oversimplification, but that is fine: We only really care about the last step, and if our coordinates always just define a rectangle that fills the whole canvas, and the vertex shader does not do anything interesting, then what remains is a HTML canvas that takes a program (written in the GL shader language), which is run for each pixel and calculates the color to be shown at that pixel.</p>
<p>Perfect! Just what I need. Dynamically creating a program that renders the pattern I want to show is squarely within Haskell’s strengths.</p>
<h2 id="a-reflex-dom-widget">A <code>reflex-dom</code> widget</h2>
<p>As my game UI grows, I will at some point no longer want to deal with raw DOM access, events etc., and the abstraction that makes creating such user interfaces painless is Functional Reactive Programming (FRP). One of the main mature implementations is Ryan Trinkle's <a href="https://reflex-frp.org/"><code>reflex-dom</code></a>, and I want to use this project to get more hands-on experience with it.</p>
<p>Based on my description above, once I hide all the details of the WebGL canvas setup, what I really have is a widget that takes a text string (representing the fragment shader), and creates a DOM element for it. This would suggest a function with this type signature</p>
<pre><code>fragmentShaderCanvas ::
MonadWidget t m =>
Dynamic t Text ->
m ()</code></pre>
<p>where the input text is <em>dynamic</em>, meaning it can change over time (and the canvas will be updated) accordingly. In fact, I also want to specify attributes for the canvas (especially <code>width</code> and <code>height</code>), and if the supplied fragment shader source is invalid and does not compile, I want to get my hands on error messages, as provided by the browser. So I ended up with this:</p>
<pre><code>fragmentShaderCanvas ::
MonadWidget t m =>
Map Text Text ->
Dynamic t Text ->
m (Dynamic t (Maybe Text))</code></pre>
<p>which very pleasingly hides all the complexity of setting up the WebGL context from the user. This is abstraction at excellence!</p>
<p>I published this widget in the <a href="%60reflex-dom-fragment-shader-canvas%60">hackage.haskell.org/package/reflex-dom-fragment-shader-canvas</a> package on Hackage.</p>
<h2 id="a-demo">A Demo</h2>
<p>And because <code>reflex-dom</code> make it so nice, I created a little demo program; it is essentially a fragment shader playground!</p>
<p>On <a href="https://nomeata.github.io/reflex-dom-fragment-shader-canvas/" class="uri">https://nomeata.github.io/reflex-dom-fragment-shader-canvas/</a> you will find a text area where you can edit the fragment shader code. All your changes are immediately reflected in the canvas on the right, and in the list of warnings and errors below the text area. The <a href="https://github.com/nomeata/reflex-dom-fragment-shader-canvas/blob/6d64129c9bfb3b1171a86b9f7007467733e8009b/demo/Main.hs#L8">code for this demo</a> is pretty short.</p>
<p>A few things could be improved, of course: For example, the <code>canvas</code> element should have its resolution automatically adjusted to the actual size on screen, but it is somewhat tricky to find out when and if a DOM element has changed size. Also, the WebGL setup should be rewritten to be more defensively, and fail more gracefully if things go wrong.</p>
<p>BTW, if you need a proper shader playground, check out <a href="https://www.shadertoy.com/">Shadertoy</a>.</p>
<h2 id="development-and-automatic-deployment">Development and automatic deployment</h2>
<p>The <code>reflex</code> authors all use Nix as their development environment, and if you want to use <code>reflex-dom</code>, then using Nix is certainly the path of least resistance. But I would like to point out that it is not a necessity, and you can stay squarely in <code>cabal</code> land if you want:</p>
<ul>
<li><p>You don’t actually need <code>ghcjs</code> to <em>develop</em> your web application: <code>reflex-dom</code> builds on <code>jsaddle</code> which has a mode where you build your program using normal GHC, and it runs a web server that your browser connects to. It works better with Chrome <a href="https://github.com/ghcjs/jsaddle/issues/64">than with Firefox</a> at the moment, but is totally adequate to develop a program.</p></li>
<li><p>If you do want to install <code>ghcjs</code>, then it is actually relatively easily: The <a href="https://github.com/ghcjs/ghcjs/tree/ghc-8.2">README on the <code>ghc-8.2</code> branch of GHCJS</a> tells you how to build and install <code>GHCJS</code> with <code>cabal new-build</code>.</p></li>
<li><p><code>cabal</code> itself supports <code>ghcjs</code> just like <code>ghc</code>! Just pass <code>--ghcjs -w ghcjs</code> to it.</p></li>
<li><p>Because few people use <code>ghcjs</code> and <code>reflex</code> with <code>cabal</code> some important packages (<code>ghcjs-base</code>, <code>reflex</code>, <code>reflex-dom</code>) are not on Hackage, or only with old versions. You can point <code>cabal</code> to local checkouts using a <code>cabal.project</code> file or even directly to the git repositories. But it is simpler to just use <a href="https://hackage-ghcjs-overlay.nomeata.de/">a Hackage overlay</a> that I created with these three packages, until they are uploaded to Hackage.</p></li>
<li><p>If the application you create is a pure client-based program and could therefore be hosted on any static web host, wouldn’t it be nice if you could just have it appear somewhere in the internet whenever you push to your project? Even that is possible, as I describe in an <a href="https://github.com/nomeata/ghcjs2gh-pages/">example repository</a>!</p></li>
</ul>
<p>It uses Travis CI to build GHCJS and the dependencies, caches them, builds your program and – if successful – uploads the result to GitHub Pages. In fact, the demo linked above is produced using that. Just push, and 5 minutes later the changes available online!</p>
<p>I know about rumors that Herbert’s excellent <a href="https://github.com/haskell-CI/haskell-ci">multi-GHC PPA repository</a> might provide <code>.deb</code> packages with GHCJS prebuilt soon. Once that happens, and maybe <code>ghcjs-base</code> and <code>reflex</code> get uploaded to Hackage, then the power of reflex-based web development will be conveniently available to all Haskell developers (even those who shunned Nix so far), and I am looking forward to many cool projects coming out of that.</p>Sun, 22 Jul 2018 10:41:27 -0400The diameter of German+English
http://www.joachim-breitner.de/blog/741-The_diameter_of_German%2BEnglish
http://www.joachim-breitner.de/blog/741-The_diameter_of_German%2BEnglishhttp://www.joachim-breitner.de/blog/741-The_diameter_of_German%2BEnglish#commentsmail@joachim-breitner.de (Joachim Breitner)<p>Languages never map directly onto each other. The English word <strong>fresh</strong> can mean <strong>frisch</strong> or <strong>frech</strong>, but <strong>frish</strong> can also be <strong>cool</strong>. Jumping from one words to another like this yields entertaining sequences that take you to completely different things. Here is one I came up with:</p>
<blockquote>
<p><strong>frech</strong> – <strong>fresh</strong> – <strong>frish</strong> – <strong>cool</strong> – <strong>abweisend</strong> – <strong>dismissive</strong> – <strong>wegwerfend</strong> – <strong>trashing</strong> – <strong>verhauend</strong> – <strong>banging</strong> – <strong>Geklopfe</strong> – <strong>knocking</strong> – …</p>
</blockquote>
<p>And I could go on … but how far? So here is a little experiment I ran:</p>
<ol style="list-style-type: decimal">
<li><p>I obtained a German-English dictionary. Conveniently, after registration, you can get <a href="https://www1.dict.cc/translation_file_request.php">dict.cc’s translation file</a>, which is simply a text file with three columns: German, English, Word form.</p></li>
<li><p>I wrote a program that takes these words and first canonicalizes them a bit: Removing attributes like <code>[ugs.]</code> <code>[regional]</code>, <code>{f}</code>, the <code>to</code> in front of verbs and other embellishment.</p></li>
<li><p>I created the undirected, bipartite graph of all these words. This is a pretty big graph – ~750k words in each language, a million edges. A path in this graph is precisely a sequence like the one above.</p></li>
<li><p>In this graph, I tried to find a <em>diameter</em>. The diameter of a graph is the longest path between two nodes that you cannot connect with a shorter path.</p></li>
</ol>
<p>Because the graph is big (and my code maybe not fully optimized), it ran a few hours, but here it is: The English expression <strong>be annoyed by sb.</strong> and the German noun <strong>Icterus</strong> are related by 55 translations. Here is the full list:</p>
<ul>
<li>be annoyed by sb.</li>
<li>durch jdn. verärgert sein</li>
<li>be vexed with sb.</li>
<li>auf jdn. böse sein</li>
<li>be angry with sb.</li>
<li>jdm. böse sein</li>
<li>have a grudge against sb.</li>
<li>jdm. grollen</li>
<li>bear sb. a grudge</li>
<li>jdm. etw. nachtragen</li>
<li>hold sth. against sb.</li>
<li>jdm. etw. anlasten</li>
<li>charge sb. with sth.</li>
<li>jdn. mit etw. [Dat.] betrauen</li>
<li>entrust sb. with sth.</li>
<li>jdm. etw. anvertrauen</li>
<li>entrust sth. to sb.</li>
<li>jdm. etw. befehlen</li>
<li>tell sb. to do sth.</li>
<li>jdn. etw. heißen</li>
<li>call sb. names</li>
<li>jdn. beschimpfen</li>
<li>abuse sb.</li>
<li>jdn. traktieren</li>
<li>pester sb.</li>
<li>jdn. belästigen</li>
<li>accost sb.</li>
<li>jdn. ansprechen</li>
<li>address oneself to sb.</li>
<li>sich an jdn. wenden</li>
<li>approach</li>
<li>erreichen</li>
<li>hit</li>
<li>Treffer</li>
<li>direct hit</li>
<li>Volltreffer</li>
<li>bullseye</li>
<li>Hahnenfuß-ähnlicher Wassernabel</li>
<li>pennywort</li>
<li>Mauer-Zimbelkraut</li>
<li>Aaron's beard</li>
<li>Großkelchiges Johanniskraut</li>
<li>Jerusalem star</li>
<li>Austernpflanze</li>
<li>goatsbeard</li>
<li>Geißbart</li>
<li>goatee</li>
<li>Ziegenbart</li>
<li>buckhorn plantain</li>
<li>Breitwegerich / Breit-Wegerich</li>
<li>birdseed</li>
<li>Acker-Senf / Ackersenf</li>
<li>yellows</li>
<li>Gelbsucht</li>
<li>icterus</li>
<li>Icterus</li>
</ul>
<p>Pretty neat!</p>
<p>So what next?</p>
<p>I could try to obtain an even longer chain by forgetting whether a word is English or German (and lower-casing everything), thus allowing wild jumps like <strong>hat</strong> – <strong>hut</strong> – <strong>hütte</strong> – <strong>lodge</strong>.</p>
<p>Or write a tool where you can enter two arbitrary words and it finds such a path between them, if there exists one. Unfortunately, it seems that the terms of the dict.cc data dump would not allow me to create such a tool as a web site (but maybe I can ask).</p>
<p>Or I could throw in additional languages!</p>
<p>What would you do?</p>
<p><strong>Update (2018-06-17):</strong></p>
<p>I ran the code again, this time lower-casing all words, and allowing false-friends translations, as suggested above. The resulting graph has – surprisingly – precisely the same diamater (55), but with a partly different list:</p>
<ul>
<li>peyote</li>
<li>peyote</li>
<li>mescal</li>
<li>meskal</li>
<li>mezcal</li>
<li>blaue agave</li>
<li>maguey</li>
<li>amerikanische agave</li>
<li>american agave</li>
<li>jahrhundertpflanze</li>
<li>century plant</li>
<li>fächerlilie</li>
<li>tumbleweed</li>
<li>weißer fuchsschwanz</li>
<li>common tumbleweed</li>
<li>acker-fuchsschwanz / ackerfuchsschwanz</li>
<li>rough pigweed</li>
<li>grünähriger fuchsschwanz</li>
<li>love-lies-bleeding</li>
<li>stiefmütterchen</li>
<li>pansy</li>
<li>schwuchtel</li>
<li>fruit</li>
<li>ertrag</li>
<li>gain</li>
<li>vorgehen</li>
<li>approach</li>
<li>sich an jdn. wenden</li>
<li>address oneself to sb.</li>
<li>jdn. ansprechen</li>
<li>accost sb.</li>
<li>jdn. belästigen</li>
<li>pester sb.</li>
<li>jdn. traktieren</li>
<li>abuse sb.</li>
<li>jdn. beschimpfen</li>
<li>call sb. names</li>
<li>jdn. etw. heißen</li>
<li>tell sb. to do sth.</li>
<li>jdm. etw. befehlen</li>
<li>entrust sth. to sb.</li>
<li>jdm. etw. anvertrauen</li>
<li>entrust sb. with sth.</li>
<li>jdn. mit etw. [dat.] betrauen</li>
<li>charge sb. with sth.</li>
<li>jdm. etw. zur last legen</li>
<li>hold sth. against sb.</li>
<li>jdm. etw. nachtragen</li>
<li>bear sb. a grudge</li>
<li>jdm. grollen</li>
<li>have a grudge against sb.</li>
<li>jdm. böse sein</li>
<li>be angry with sb.</li>
<li>auf jdn. böse sein</li>
<li>be mad at sb.</li>
<li>auf jdn. einen (dicken) hals haben</li>
</ul>
<p>Note that there is not actually a false-friend in this list – it seems that adding the edges just changed the order of edges in the graph representation and my code just happened to find a different diamer.</p>Wed, 23 May 2018 08:35:24 +0200Proof reuse in Coq using existential variables
http://www.joachim-breitner.de/blog/740-Proof_reuse_in_Coq_using_existential_variables
http://www.joachim-breitner.de/blog/740-Proof_reuse_in_Coq_using_existential_variableshttp://www.joachim-breitner.de/blog/740-Proof_reuse_in_Coq_using_existential_variables#commentsmail@joachim-breitner.de (Joachim Breitner)<p>This is another technical post that is only of interest only to Coq users.</p>
<p>TL;DR: Using existential variable for hypotheses allows you to easily refactor a complicated proof into an induction schema and the actual proofs.</p>
<h3 id="setup">Setup</h3>
<p>As a running example, I will use a small theory of “bags”, which you can think of as lists represented as trees, to allow an <span class="math inline"><em>O</em>(1)</span> append operation:</p>
<pre><code>Require Import Coq.Arith.Arith.
Require Import Psatz.
Require FunInd.
(* The data type *)
Inductive Bag a : Type :=
| Empty : Bag a
| Unit : a -> Bag a
| Two : Bag a -> Bag a -> Bag a.
Arguments Empty {_}.
Arguments Unit {_}.
Arguments Two {_}.
Fixpoint length {a} (b : Bag a) : nat :=
match b with
| Empty => 0
| Unit _ => 1
| Two b1 b2 => length b1 + length b2
end.
(* A smart constructor that ensures that a [Two] never
has [Empty] as subtrees. *)
Definition two {a} (b1 b2 : Bag a) : Bag a := match b1 with
| Empty => b2
| _ => match b2 with | Empty => b1
| _ => Two b1 b2 end end.
Lemma length_two {a} (b1 b2 : Bag a) :
length (two b1 b2) = length b1 + length b2.
Proof. destruct b1, b2; simpl; lia. Qed.
(* A first non-trivial function *)
Function take {a : Type} (n : nat) (b : Bag a) : Bag a :=
if n =? 0
then Empty
else match b with
| Empty => b
| Unit x => b
| Two b1 b2 => two (take n b1) (take (n - length b1) b2)
end.</code></pre>
<h3 id="the-theorem">The theorem</h3>
<p>The theorem that I will be looking at in this proof describes how <code>length</code> and <code>take</code> interact:</p>
<pre><code>Theorem length_take''':
forall {a} n (b : Bag a),
length (take n b) = min n (length b).</code></pre>
<p>Before I dive into it, let me point out that this example itself is too simple to warrant the techniques that I will present in this post. I have to rely on your imagination to scale this up to appreciate the effect on significantly bigger proofs.</p>
<h3 id="naive-induction">Naive induction</h3>
<p>How would we go about proving this lemma? Surely, <a href="https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.induction"><code>induction</code></a> is the way to go! And indeed, this is provable using induction (on the <code>Bag</code>) just fine:</p>
<pre><code>Proof.
intros.
revert n.
induction b; intros n.
* simpl.
destruct (Nat.eqb_spec n 0).
+ subst. rewrite Nat.min_0_l. reflexivity.
+ rewrite Nat.min_0_r. reflexivity.
* simpl.
destruct (Nat.eqb_spec n 0).
+ subst. rewrite Nat.min_0_l. reflexivity.
+ simpl. lia.
* simpl.
destruct (Nat.eqb_spec n 0).
+ subst. rewrite Nat.min_0_l. reflexivity.
+ simpl. rewrite length_two, IHb1, IHb2. lia.
Qed.</code></pre>
<p>But there is a problem: A proof by induction on the <code>Bag</code> argument immediately creates three subgoals, one for each constructor. But that is not how <code>take</code> is defined, which <em>first</em> checks the value of <code>n</code>, independent of the constructor. This means that we have to do the case-split and the proof for the case <code>n = 0</code> three times, although they are identical. It’s a one-line proof here, but imagine something bigger...</p>
<h3 id="proof-by-fixpoint">Proof by fixpoint</h3>
<p>Can we refactor the proof to handle the case <code>n = 0</code> first? Yes, but not with a simple invocation of the <code>induction</code> tactic. We could do well-founded induction on the <code>length</code> of the argument, or we can do the proof using the more primitive <a href="https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.fix"><code>fix</code> tactic</a>. The latter is a bit hairy, you won’t know if your proof is accepted until you do <code>Qed</code> (or check with <a href="https://coq.inria.fr/refman/proof-engine/proof-handling.html#coq:cmd.guarded"><code>Guarded</code></a>), but when it works it can yield some nice proofs.</p>
<pre><code>Proof.
intros a.
fix IH 2.
intros.
rewrite take_equation.
destruct (Nat.eqb_spec n 0).
+ subst n. rewrite Nat.min_0_l. reflexivity.
+ destruct b.
* rewrite Nat.min_0_r. reflexivity.
* simpl. lia.
* simpl. rewrite length_two, !IH. lia.
Qed.</code></pre>
<p>Nice: we eliminated the duplication of proofs!</p>
<h3 id="a-functional-induction-lemma">A functional induction lemma</h3>
<p>Again, imagine that we jumped through more hoops here ... maybe some well-founded recursion with a tricky size measure and complex proofs that the measure decreases ... or maybe you need to carry around an invariant about your arguments and you have to work hard to satisfy the assumption of the induction hypothesis.</p>
<p>As long as you do only one proof about <code>take</code>, that is fine. As soon as you do a second proof, you will notice that you have to repeat all of that, and it can easily make up most of your proof...</p>
<p>Wouldn’t it be nice if you can do the common parts of the proofs only once, obtain a generic proof scheme that you can use for (most) proofs about <code>take</code>, and then just fill in the blanks?</p>
<p>Incidentally, the <a href="https://coq.inria.fr/refman/language/gallina-extensions.html#coq:cmd.function"><code>Function</code> command</a> provides precisely that:</p>
<pre><code>take_ind
: forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
(forall (n : nat) (b : Bag a), (n =? 0) = true -> P n b Empty) ->
(forall (n : nat) (b : Bag a), (n =? 0) = false -> b = Empty -> P n Empty b) ->
(forall (n : nat) (b : Bag a), (n =? 0) = false -> forall x : a, b = Unit x -> P n (Unit x) b) ->
(forall (n : nat) (b : Bag a),
(n =? 0) = false ->
forall b1 b2 : Bag a,
b = Two b1 b2 ->
P n b1 (take n b1) ->
P (n - length b1) b2 (take (n - length b1) b2) ->
P n (Two b1 b2) (two (take n b1) (take (n - length b1) b2))) ->
forall (n : nat) (b : Bag a), P n b (take n b)</code></pre>
<p>which is great if you can use <code>Function</code> (although not perfect – we’d rather see <code>n = 0</code> instead of <code>(n =? 0) = true</code>), but often <code>Function</code> is not powerful enough to define the function you care about.</p>
<h3 id="extracting-the-scheme-from-a-proof">Extracting the scheme from a proof</h3>
<p>We could define our own <code>take_ind'</code> by hand, but that is a lot of work, and we may not get it right easily, and when we change out functions, there is now this big proof statement to update.</p>
<p>Instead, let us use existentials, which are variables where Coq infers their type from how we use them, so we don’t have to declare them. Unfortunately, Coq does not support writing just</p>
<pre><code>Lemma take_ind':
forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
forall (IH1 : ?) (IH2 : ?) (IH3 : ?) (IH4 : ?),
forall n b, P n b (take n b).</code></pre>
<p>where we just leave out the type of the assumptions (Isabelle does...), but we can fake it using some generic technique.</p>
<p>We begin with stating an auxiliary lemma using a sigma type to say “there exist some assumption that are sufficient to show the conclusion”:</p>
<pre><code>Lemma take_ind_aux:
forall a (P : _ -> _ -> _ -> Prop),
{ Hs : Prop |
Hs -> forall n (b : Bag a), P n b (take n b)
}.</code></pre>
<p>We use the [<code>eexist</code> tactic])(https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacv.eexists) (existential <code>exists</code>) to construct the sigma type without committing to the type of <code>Hs</code> yet.</p>
<pre><code>Proof.
intros a P.
eexists.
intros Hs.</code></pre>
<p>This gives us an assumption <code>Hs : ?Hs</code> – note the existential type. We need four of those, which we can achieve by writing</p>
<pre><code> pose proof Hs as H1. eapply proj1 in H1. eapply proj2 in Hs.
pose proof Hs as H2. eapply proj1 in H2. eapply proj2 in Hs.
pose proof Hs as H3. eapply proj1 in H3. eapply proj2 in Hs.
rename Hs into H4.</code></pre>
<p>we now have this goal state:</p>
<pre><code>1 subgoal
a : Type
P : nat -> Bag a -> Bag a -> Prop
H4 : ?Goal2
H1 : ?Goal
H2 : ?Goal0
H3 : ?Goal1
______________________________________(1/1)
forall (n : nat) (b : Bag a), P n b (take n b)</code></pre>
<p>At this point, we start reproducing the proof of <code>length_take</code>: The same approach to induction, the same case splits:</p>
<pre><code> fix IH 2.
intros.
rewrite take_equation.
destruct (Nat.eqb_spec n 0).
+ subst n.
revert b.
refine H1.
+ rename n0 into Hnot_null.
destruct b.
* revert n Hnot_null.
refine H2.
* rename a0 into x.
revert x n Hnot_null.
refine H3.
* assert (IHb1 : P n b1 (take n b1)) by apply IH.
assert (IHb2 : P (n - length b1) b2 (take (n - length b1) b2)) by apply IH.
revert n b1 b2 Hnot_null IHb1 IHb2.
refine H4.
Defined. (* Important *)</code></pre>
<p>Inside each case, we move all relevant hypotheses into the goal using <a href="https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.revert"><code>revert</code></a> and <a href="https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.refine"><code>refine</code></a> with the corresponding assumption, thus instantiating it. In the recursive case (<code>Two</code>), we assert that <code>P</code> holds for the subterms, by induction.</p>
<p>It is important to end this proofs with <a href="https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#vernac-controlling-the-reduction-strategies"><code>Defined</code>, and not <code>Qed</code>,</a> as we will see later.</p>
<p>In a next step, we can remove the sigma type:</p>
<pre><code>Definition take_ind' a P := proj2_sig (take_ind_aux a P).</code></pre>
<p>The type of <code>take_ind'</code> is as follows:</p>
<pre><code>take_ind'
: forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
proj1_sig (take_ind_aux a P) ->
forall n b, P n b (take n b)</code></pre>
<p>This looks almost like an induction lemma. The assumptions of this lemma have the not very helpful type <code>proj1_sig (take_ind_aux a P)</code>, but we can already use this to prove <code>length_take</code>:</p>
<pre><code>Theorem length_take:
forall {a} n (b : Bag a),
length (take n b) = min n (length b).
Proof.
intros a.
intros.
apply take_ind' with (P := fun n b r => length r = min n (length b)).
repeat apply conj; intros.
* rewrite Nat.min_0_l. reflexivity.
* rewrite Nat.min_0_r. reflexivity.
* simpl. lia.
* simpl. rewrite length_two, IHb1, IHb2. lia.
Qed.</code></pre>
<p>In this case I have to explicitly state <code>P</code> where I invoke <code>take_ind'</code>, because Coq cannot figure out this instantiation on its own (it requires higher-order unification, which is undecidable and unpredictable). In other cases I had more luck.</p>
<p>After I <code>apply take_ind'</code>, I have this proof goal:</p>
<pre><code>______________________________________(1/1)
proj1_sig (take_ind_aux a (fun n b r => length r = min n (length b)))</code></pre>
<p>which is the type that Coq inferred for <code>Hs</code> above. We know that this is a conjunction of a bunch of assumptions, and we can split it as such, using <code>repeat apply conj</code>. At this point, Coq needs to look inside <code>take_ind_aux</code>; this would fail if we used <code>Qed</code> to conclude the proof of <code>take_ind_aux</code>.</p>
<p>This gives me four goals, one for each case of <code>take</code>, and the remaining proofs really only deals with the specifics of <code>length_take</code> – no more general dealing with worrying about getting the induction right and doing the case-splitting the right way.</p>
<p>Also note that, very conveniently, Coq uses the same name for the induction hypotheses <code>IHb1</code> and <code>IHb2</code> that we used in <code>take_ind_aux</code>!</p>
<h3 id="making-it-prettier">Making it prettier</h3>
<p>It may be a bit confusing to have this <code>proj1_sig</code> in the type, especially when working in a team where others will use your induction lemma without knowing its internals. But we can resolve that, and also turn the conjunctions into normal arrows, using a bit of tactic support. This is completely generic, so if you follow this procedure, you can just copy most of that:</p>
<pre><code>Lemma uncurry_and: forall {A B C}, (A /\ B -> C) -> (A -> B -> C).
Proof. intros. intuition. Qed.
Lemma under_imp: forall {A B C}, (B -> C) -> (A -> B) -> (A -> C).
Proof. intros. intuition. Qed.
Ltac iterate n f x := lazymatch n with
| 0 => x
| S ?n => iterate n f uconstr:(f x)
end.
Ltac uncurryN n x :=
let n' := eval compute in n in
lazymatch n' with
| 0 => x
| S ?n => let uc := iterate n uconstr:(under_imp) uconstr:(uncurry_and) in
let x' := uncurryN n x in
uconstr:(uc x')
end.</code></pre>
<p>With this in place, we can define our final proof scheme lemma:</p>
<pre><code>Definition take_ind'' a P
:= ltac:(let x := uncurryN 3 (proj2_sig (take_ind_aux a P)) in exact x).
Opaque take_ind''.</code></pre>
<p>The type of <code>take_ind''</code> is now exactly what we’d wish for: All assumptions spelled out, and the <code>n =? 0</code> already taken of (compare this to the <code>take_ind</code> provided by the <code>Function</code> command above):</p>
<pre><code>take_ind''
: forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
(forall b : Bag a, P 0 b Empty) ->
(forall n : nat, n <> 0 -> P n Empty Empty) ->
(forall (x : a) (n : nat), n <> 0 -> P n (Unit x) (Unit x)) ->
(forall (n : nat) (b1 b2 : Bag a),
n <> 0 ->
P n b1 (take n b1) ->
P (n - length b1) b2 (take (n - length b1) b2) ->
P n (Two b1 b2) (two (take n b1) (take (n - length b1) b2))) ->
forall (n : nat) (b : Bag a), P n b (take n b)</code></pre>
<p>At this point we can mark <code>take_ind''</code> as <code>Opaque</code>, to hide how we obtained this lemma.</p>
<p>Our proof does not change a lot; we merely no longer have to use <code>repeat apply conj</code>:</p>
<pre><code>Theorem length_take''':
forall {a} n (b : Bag a),
length (take n b) = min n (length b).
Proof.
intros a.
intros.
apply take_ind'' with (P := fun n b r => length r = min n (length b)); intros.
* rewrite Nat.min_0_l. reflexivity.
* rewrite Nat.min_0_r. reflexivity.
* simpl. lia.
* simpl. rewrite length_two, IHb1, IHb2. lia.
Qed.</code></pre>
<h3 id="is-it-worth-it">Is it worth it?</h3>
<p>It was in my case: <a href="https://github.com/antalsz/hs-to-coq/compare/de89fd0...b5b8ff7">Applying this trick</a> in our ongoing work of verifying parts of the Haskell compiler GHC separated a somewhat proof into a re-usable proof scheme (<code>go_ind</code>), making the actual proofs (<code>go_all_WellScopedFloats</code>, <code>go_res_WellScoped</code>) much neater and to the point. It saved “only” 60 lines (if I don’t count the 20 “generic” lines above), but the pay-off will increase as I do even more proofs about this function.</p>Fri, 18 May 2018 08:51:19 -0400Avoid the dilemma of the trailing comma
http://www.joachim-breitner.de/blog/739-Avoid_the_dilemma_of_the_trailing_comma
http://www.joachim-breitner.de/blog/739-Avoid_the_dilemma_of_the_trailing_commahttp://www.joachim-breitner.de/blog/739-Avoid_the_dilemma_of_the_trailing_comma#commentsmail@joachim-breitner.de (Joachim Breitner)<p>The Haskell syntax uses comma-separated lists in various places and does, in contrast to other programming language, not allow a trailing comma. If everything goes on one line you write</p>
<pre><code> (foo, bar, baz)</code></pre>
<p>and everything is nice.</p>
<h3 id="lining-up">Lining up</h3>
<p>But if you want to have one entry on each line, then the obvious plan</p>
<pre><code> (foo,
bar,
baz
)</code></pre>
<p>is aesthetically unpleasing and moreover, extending the list by <em>one</em> to</p>
<pre><code> (foo,
bar,
baz,
quux
)</code></pre>
<p>modifies <em>two</em> lines, which produces less pretty diffs.</p>
<p>Because it is much more common to append to lists rather than to prepend, Haskellers have developed the idiom of leading comma:</p>
<pre><code> ( foo
, bar
, baz
, quux
)</code></pre>
<p>which looks strange until you are used to it, but solves the problem of appending to a list. And we see this idiom in many places:</p>
<ul>
<li><p>In Cabal files:</p>
<pre><code> build-depends: base >= 4.3 && < 5
, array
, deepseq >= 1.2 && < 1.5</code></pre></li>
<li><p>In module headers:</p>
<pre><code>{-# LANGUAGE DefaultSignatures
, EmptyCase
, ExistentialQuantification
, FlexibleContexts
, FlexibleInstances
, GADTs
, InstanceSigs
, KindSignatures
, RankNTypes
, ScopedTypeVariables
, TemplateHaskell
, TypeFamilies
, TypeInType
, TypeOperators
, UndecidableInstances #-}</code></pre></li>
</ul>
<h3 id="think-outside-the-list">Think outside the list!</h3>
<p>I started to avoid this pattern where possible. And it is possible everywhere instead of having a declaration with a list, you can just have multiple declarations. I.e.:</p>
<ul>
<li><p>In Cabal files:</p>
<pre><code> build-depends: base >= 4.3 && < 5
build-depends: array
build-depends: deepseq >= 1.2 && < 1.5</code></pre></li>
<li><p>In module headers:</p>
<pre><code>{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}</code></pre></li>
</ul>
<p>It is a bit heavier, but it has a number of advantages:</p>
<ol style="list-style-type: decimal">
<li>Both appending and prepending works without touching other lines.</li>
<li>It is visually more homogeneous, making it – despite the extra words – easier to spot mistakes visually.</li>
<li>You can easily sort the declarations alphabetically with your editor.</li>
<li>Especially in <code>Cabal</code> files: If you have syntax error in your dependency specification (which I always have, writing <code><<</code> instead of <code><</code> due to my Debian background), <code>cabal</code> will actually give you a helpful error location – it always only tells you which <code>build-depends</code> stanza was wrong, so if you have only one, then <a href="https://stackoverflow.com/q/32751149/946226">that’s not helpful</a>.</li>
</ol>
<h3 id="what-when-it-does-not-work">What when it does not work?</h3>
<p>Unfortunately, not every list in Haskell can have that treatment, and that’s why <a href="https://github.com/ghc-proposals/ghc-proposals/pull/87">the recent GHC proposal on <code>ExtraCommas</code></a> wants to lift the restriction. In particular, it wants to allow trailing commas in subexport lists:</p>
<pre><code>module Foo
( Foo(
A,
B,
),
fromFoo,
)</code></pre>
<p>(Weirdly, export lists already allow trailing commas). An alternative here might be to write</p>
<pre><code>module Foo
( Foo(A),
Foo(B),
fromFoo,
)</code></pre>
<p>and teach the compiler to not warn about the duplicate export of the <code>Foo</code> type.</p>
<p>For plain lists, this idiom can be useful:</p>
<pre><code>list :: [Int]
list = let (>>) = (++) in do
[ 1 ]
[ 2 ]
[ 3 ]
[ 4 ]</code></pre>
<p>It requires <code>RebindableSyntax</code>, so I do not recommend it for regular code, but it can be useful in a module that is dedicated to hold some generated data or configuration. And of course it works with any binary operator, not just <code>(++)</code></p>Mon, 30 Apr 2018 22:19:47 -0400Verifying local definitions in Coq
http://www.joachim-breitner.de/blog/738-Verifying_local_definitions_in_Coq
http://www.joachim-breitner.de/blog/738-Verifying_local_definitions_in_Coqhttp://www.joachim-breitner.de/blog/738-Verifying_local_definitions_in_Coq#commentsmail@joachim-breitner.de (Joachim Breitner)<p>TL;DR: We can give top-level names to local definitions, so that we can state and prove stuff about them without having to rewrite the programs.</p>
<h3 id="when-a-haskeller-writes-coq">When a Haskeller writes Coq</h3>
<p>Imagine you teach Coq to a Haskell programmer, and give them the task of pairing each element in a list with its index. The Haskell programmer might have</p>
<pre><code>addIndex :: [a] -> [(Integer, a)]
addIndex xs = go 0 xs
where go n [] = []
go n (x:xs) = (n,x) : go (n+1) xs</code></pre>
<p>in mind and write this Gallina function (Gallina is the programming language of Coq):</p>
<pre><code>Require Import Coq.Lists.List.
Import ListNotations.
Definition addIndex {a} (xs : list a) : list (nat * a) :=
let fix go n xs := match xs with
| [] => []
| x::xs => (n, x) :: go (S n) xs
end
in go 0 xs.</code></pre>
<p>Alternatively, imagine you are using <a href="https://github.com/antalsz/hs-to-coq"><code>hs-to-coq</code></a> to mechanically convert the Haskell definition into Coq.</p>
<h3 id="when-a-coq-user-tries-to-verify-that">When a Coq user tries to verify that</h3>
<p>Now your task is to prove something about this function, for example</p>
<pre><code>Theorem addIndex_spec:
forall {a} n (xs : list a),
nth n (map fst (addIndex xs)) n = n.</code></pre>
<p>If you just have learned Coq, you will think “I can do this, this surely holds by induction on <code>xs</code>.” But if you have a bit more experience, you will already see a problem with this (if you do not see the problem yet, I encourage you to stop reading, copy the few lines above, and try to prove it).</p>
<p>The problem is that – as so often – you have to generalize the statement for the induction to go through. The theorem as stated says something about <code>addIndex</code> or, in other words, about <code>go 0</code>. But in the inductive case, you will need some information about <code>go 1</code>. In fact, you need a lemma like this:</p>
<pre><code>Lemma go_spec:
forall {a} n m k (xs : list a), k = n + m ->
nth n (map fst (go m xs)) k = k.</code></pre>
<p>But <code>go</code> is not a (top-level) function! How can we fix that?</p>
<ul>
<li>We can try to awkwardly work-around not having a name for <code>go</code> in our proofs, and essentially prove <code>go_spec</code> inside the proof of <code>addIndex_spec</code>. Might work in this small case, but does not scale up to larger proofs.</li>
<li>We can ask the programmer to avoid using local functions, and first define <code>go</code> as a top-level fixed point. But maybe we don’t want to bother them because of that. (Or, more likely, we are using <code>hs-to-coq</code> and that tool stubbornly tries to make the output as similar to the given Haskell code as possible.)</li>
<li>We can copy’n’paste the definition of <code>go</code> and make a separate, after-the-fact top-level definition. But this is not nice from a maintenance point of view: If the code changes, we have to update this copy.</li>
<li>Or we apply this one weird trick...</li>
</ul>
<h3 id="the-weird-trick">The weird trick</h3>
<p>We can define <code>go</code> after-the-fact, but instead of copy’n’pasting the definition, we can use Coq’s tactics to define it. Here it goes:</p>
<pre><code>Definition go {a} := ltac:(
let e := eval cbv beta delta [addIndex] in (@addIndex a []) in
(* idtac e; *)
lazymatch e with | let x := ?def in _ =>
exact def
end).</code></pre>
<p>Let us take it apart:</p>
<ol style="list-style-type: decimal">
<li>We define <code>go</code>, and give the parameters that <code>go</code> depends upon. Note that of the two parameters of <code>addIndex</code>, the definition of <code>go</code> only depends on (“captures”) <code>a</code>, but not <code>xs</code>.</li>
<li>We do <em>not</em> give a type to <code>go</code>. We could, but that would again just be copying information that is already there.</li>
<li>We define go via an <code>ltac</code> expression: Instead of a term we give a tactic that calculates the term.</li>
<li>This tactic first binds <code>e</code> to the body of <code>addIndex</code>. To do so, it needs to pass enough arguments to <code>addIndex</code>. The concrete value of the list argument does not matter, so we pass <code>[]</code>. The term <code>@addIndex a []</code> is now evaluated with the evaluation flags <code>eval cbv beta delta [addIndex]</code>, which says “unfold <code>addIndex</code> and do beta reduction, but nothing else”. In particularly, we do not do <code>zeta</code> reduction, which would reduce the <code>let go := …</code> definition. (The <a href="https://coq.inria.fr/refman/proof-engine/tactics.html#performing-computations">user manual</a> very briefly describes these flags.)</li>
<li>The <code>idtac e</code> line can be used to peek at <code>e</code>, for example when the next tactic fails. We can use this to check that <code>e</code> really is of the form <code>let fix go := … in …</code>.</li>
<li>The <code>lazymatch</code> line matches <code>e</code> against the pattern <code>let x := ?def in _</code>, and binds the definition of <code>go</code> to the name <code>def</code>.</li>
<li>And the <code>exact def</code> tactic tells Coq to use <code>def</code> as the definition of <code>go</code>.</li>
</ol>
<p>We now have defined <code>go</code>, of type <code>go : forall {a}, nat -> list a -> list (nat * a)</code>, and can state and prove the auxiliary lemma:</p>
<pre><code>Lemma go_spec:
forall {a} n m k (xs : list a), k = n + m ->
nth n (map fst (go m xs)) k = k.
Proof.
intros ?????.
revert n m k.
induction xs; intros; destruct n; subst; simpl.
1-3:reflexivity.
apply IHxs; lia.
Qed.</code></pre>
<p>When we come to the theorem about <code>addIndex</code>, we can play a little trick with <code>fold</code> to make the proof goal pretty:</p>
<pre><code>Theorem addIndex_spec:
forall {a} n (xs : list a),
nth n (map fst (addIndex xs)) n = n.
Proof.
intros.
unfold addIndex.
fold (@go a).
(* goal here: nth n (map fst (go 0 xs)) n = n *)
apply go_spec; lia.
Qed.</code></pre>
<h3 id="multiple-local-definitions">Multiple local definitions</h3>
<p>The trick extends to multiple local definitions, but needs some extra considerations to ensure that terms are closed. A bit contrived, but let us assume that we have this function definition:</p>
<pre><code>Definition addIndex' {a} (xs : list a) : list (nat * a) :=
let inc := length xs in
let fix go n xs := match xs with
| [] => []
| x::xs => (n, x) :: go (inc + n) xs
end in
go 0 xs.</code></pre>
<p>We now want to give names to <code>inc</code> <em>and</em> to <code>go</code>. I like to use a section to collect the common parameters, but that is not essential here. The trick above works flawlessly for `inc':</p>
<pre><code>Section addIndex'.
Context {a} (xs : list a).
Definition inc := ltac:(
let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
lazymatch e with | let x := ?def in _ =>
exact def
end).</code></pre>
<p>But if we try it for <code>go'</code>, like such:</p>
<pre><code>Definition go' := ltac:(
let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
lazymatch e with | let x := _ in let y := ?def in _ =>
exact def
end).</code></pre>
<p>we get “Ltac variable def depends on pattern variable name x which is not bound in current context”. To fix this, we use higher-order pattern matchin (<code>@?def</code>) to substitute “our” <code>inc</code> for the local <code>inc</code>:</p>
<pre><code>Definition go' := ltac:(
let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
lazymatch e with | let x := _ in let y := @?def x in _ =>
let def' := eval cbv beta in (def inc) in
exact def'
end).</code></pre>
<p>instead. We have now defined both <code>inc</code> and <code>go'</code> and can use them in proofs about <code>addIndex'</code>:</p>
<pre><code>Theorem addIndex_spec':
forall n, nth n (map fst (addIndex' xs)) n = n * length xs.
Proof.
intros.
unfold addIndex'.
fold inc go'. (* order matters! *)
(* goal here: nth n (map fst (go' 0 xs)) n = n * inc *)</code></pre>
<h3 id="reaching-into-a-match">Reaching into a match</h3>
<p>This trick also works when the local definition we care about is inside a match statement. Consider:</p>
<pre><code>Definition addIndex_weird {a} (oxs : option (list a))
:= match oxs with
| None => []
| Some xs =>
let fix go n xs := match xs with
| [] => []
| x::xs => (n, x) :: go (S n) xs
end in
go 0 xs
end.
Definition go_weird {a} := ltac:(
let e := eval cbv beta match delta [addIndex_weird]
in (@addIndex_weird a (Some [])) in
idtac e;
lazymatch e with | let x := ?def in _ =>
exact def
end).</code></pre>
<p>Note the addition of <code>match</code> to the list of evaluation flags passed to <code>cbv</code>.</p>
<h3 id="conclusion">Conclusion</h3>
<p>While local definitions are idiomatic in Haskell (in particular thanks to the <code>where</code> syntax), they are usually avoided in Coq, because they get in the way of verification. If, for some reason, one is stuck with such definitions, then this trick presents a reasonable way out.</p>Sun, 22 Apr 2018 17:47:24 -0400Reservoir sampling with few random bits
http://www.joachim-breitner.de/blog/737-Reservoir_sampling_with_few_random_bits
http://www.joachim-breitner.de/blog/737-Reservoir_sampling_with_few_random_bitshttp://www.joachim-breitner.de/blog/737-Reservoir_sampling_with_few_random_bits#commentsmail@joachim-breitner.de (Joachim Breitner)<p>Assume you are Nisus, the <a href="https://www.youtube.com/watch?v=8lN4TSslz-0">“one cross each” guy</a> in Monty Python’s “Life of Brian” movie. Condemned prisoners file past you one by one, on their way to crucifixion. Now it happens that this particular day, feel both both benevolent <em>and</em> very indecisive. Because you feel benevolent, you want to liberate one of the condemned. But because you feel indecisive, you don’t want to pick the lucky one yourself, so you have to leave it to chance. And you don’t want anybody to have grounds to to complain, so you want to give each prisoner exactly the same chance.</p>
<p>This would be a relatively simple task if you knew the number of prisoners, <span class="math inline"><em>n</em></span>, ahead of time: Pick a random number <span class="math inline"><em>k</em> ∈ {1, …, <em>n</em>}</span>, count while you hand our the crosses, and tell the <span class="math inline"><em>k</em></span>th prisoner to get lost.</p>
<p>But alas, the Romans judiciary system is big and effective, and you have no idea how many prisoners will emerge from the dungeons today. So you might plan to just let them all wait next to you while you count them (to figure out what <span class="math inline"><em>n</em></span> is), but that won’t work either: There is not enough space to have them waiting, and some might try to escape in the confusion before you are done counting. So in fact, you can only have one prisoner waiting at a time. As soon as the next one comes, you have to send one of them towards execution.</p>
<p>This is still a solvable problem, and the solution is <a href="https://en.wikipedia.org/wiki/Reservoir_sampling">Reservoir sampling</a>: You let the first prisoner wait. When the second one comes, you pick one of them with probability <span class="math inline">½</span>, and let him wait. When the third one comes, with probability <span class="math inline">⅔</span> you send him on, and with probability <span class="math inline">⅓</span> to let him wait. The fourth is sent forth with probability <span class="math inline">¼</span> and kept waiting with probability <span class="math inline">¼</span>. And so on. When finally the dungeon master tells you that all prisoners have emerged, whoever is waiting next to you is the lucky guy.</p>
<p>Before you do that, you should convince yourself that this is fair: The <span class="math inline"><em>k</em></span>th prisoner is the lucky one if you let him wait <em>and</em> from then on, all other prisoners are sent forth. The probability of this happening is <span class="math inline">¹ ⁄ <em>ₖ</em> ⋅ <em>ᵏ</em> ⁄ <em>ₖ</em>₊₁ ⋅ <em>ᵏ</em>⁺¹ ⁄ <em>ₖ</em>₊₂ ⋅ ⋯ ⋅ <em>ⁿ</em>⁻¹ ⁄ <em>ₙ</em></span> which, after a number of cancellations, resolves to <span class="math inline">¹ ⁄ <em>ₙ</em></span>. Because <span class="math inline"><em>k</em></span> does no longer show up in this calculation, the probability is the same for everybody, and hence fair.</p>
<h3 id="how-to-not-make-a-decision">How to not make a decision</h3>
<div class="figure">
<img src="https://upload.wikimedia.org/wikipedia/commons/c/c7/Roman_coin_commemorating_the_secret_ballot_law_of_137_BC.jpg" alt="A fair RNG"/>
<p class="caption">A fair RNG</p>
</div>
<p>So far so good. But the story misses an important point: Where do you get your randomness from? Just <a href="http://web.media.mit.edu/~guysatat/MindReader/index.html">picking randomly is hardly random</a>. Luckily, you just have been given your guerdon, and you have a Roman coin in your pocket. Let us assume the coin is perfectly fair: With probability <span class="math inline">½</span> it shows the head of Libertas, and with probability <span class="math inline">½</span> a bunch of horses. It is easy to use this coin to distinguish between the first and second prisoners, but when the third comes out, things get hairy.</p>
<p>You can try to throw the coin many times; say, 10 times. This has <span class="math inline">2<sup>10</sup> = 1024</span> outcomes, which we can interpret as a number between 1 and 1024. If you give the third prisoner his freedom when this number is between 1 and 341, and you give him a cross if the number is between 342 and 1024, then you made pretty fair call. Not yet fully satisfying, but let’s go with it for now.</p>
<p>There is, however, another problem with this: You have to throw the coin a lot of times: For each prisoner, you toss it 10 times! This is too slow, and the plebs will get impatient. And it clearly is wasteful. The great philosopher Shannonus taught you that throwing the coin ten times gives you 10 bits of entropy, but you actually need only <span class="math inline">−(⅓ ⋅ log(⅓)+⅔⋅log(⅔)) = 0.918…</span> bits to make this <span class="math inline">⅓</span>-<span class="math inline">⅔</span> decision. We should use those left-over 9.81 bits! How do we do that?</p>
<h3 id="unreal-real-randomness">Unreal real randomness</h3>
<p>To come up with a better (and maybe even optimal) plan, imagine for a moment that you had a source of randomness that gives you a real real number in the range <span class="math inline">(0, 1)</span>, uniformly. Clearly, that would solve your problem, because when prisoner <span class="math inline"><em>k</em></span> emerges, you can draw a random number <span class="math inline"><em>r</em></span> and let this prisoner wait if <span class="math inline"><em>r</em> < ¹ ⁄ <em>ₖ</em></span>.</p>
<p>But you don’t actually have to draw a random number more than once: It suffices to pick a single <span class="math inline"><em>r</em> ∈ (0, 1)</span> at the very beginning. You just have to be a bit cleverer when deciding whether to keep the <span class="math inline"><em>k</em></span>ths prisoner next to you. Let’s go through it step by step:</p>
<ul>
<li>When Augustus, the first prisoner, comes out, you simply keep him.</li>
<li>When Brutus, the second prisoner, comes out, you keep him with probability <span class="math inline">½</span>. You do that if <span class="math inline"><em>r</em> < ½</span>. You also start some bookkeeping, by remembering the range of <span class="math inline"><em>r</em></span> that has led to this outcome; in this case, the range is <span class="math inline">(0, ½)</span>. If you picked Augustus, the range is <span class="math inline">(½,1)</span>.</li>
<li><p>Now Claudius comes out, and you want to keep him with probability <span class="math inline">⅓</span>. If the range that you remembered is <span class="math inline">(0, ½)</span>, you keep him if <span class="math inline"><em>r</em> < ⅙</span>. Similarly, if the range is <span class="math inline">(½,1)</span> you keep him if <span class="math inline"><em>r</em> < ½ + ⅙ = ⁴ ⁄ ₆</span>.</p>
The currently remembered range is now <span class="math inline">(⁴⁄₆,1)</span> if Augustus is waiting, <span class="math inline">(⅙,½)</span> if Brutus is waiting and either <span class="math inline">(0, ⅙)</span> or <span class="math inline">(½,⁴⁄₆)</span> if Claudius is waiting. Notice that the ranges are not all of the same size, but if you add the lengths of each prisoner’s range, you have <span class="math inline">⅓</span>, which means that every prisoner has the same chance to be waiting so far.</li>
<li><p>Finally, Decimus shows up. You repeat this procedure: Look at the current interval; if <span class="math inline"><em>r</em></span> is in the left quarter of it, Decimus stays, otherwise he leaves.</p></li>
</ul>
<p>I tried to visualize this, and came up with this. Pick <span class="math inline"><em>r</em></span>, locate the right spot on the <span class="math inline"><em>x</em></span> axis, and you can read off, by going down, who is waiting next you.</p>
<div class="figure">
<img src="//www.joachim-breitner.de/various/nisus-coins.svg" alt="A table for Nisus"/>
<p class="caption">A table for Nisus</p>
</div>
<h3 id="back-to-using-coins">Back to using coins</h3>
<p>With this strategy in mind, we can go back to using a coin. Now, a single coin flip does not give us <span class="math inline"><em>r</em></span>. 1000 coin flips don’t either. If we could flip the coin an infinite number of times, yes, then we could get <span class="math inline"><em>r</em></span> out of this: The first coin flip decides the first bit after the <del>decimal</del> binary point: Head is 0, horses are 1. The second the second bit. And so on.</p>
<p>But note that you don’t need to know precisely <span class="math inline"><em>r</em></span>. To decide whether Augustus or Brutus stay, you only need to know if <span class="math inline"><em>r</em></span> is in the left or the right half -- and you know that after the first coin flip. You can also tell whether Claudius stays as soon as you threw the coin often enough to determine if <span class="math inline"><em>r</em> < ⅙</span>. This might already be the case after a single coin throw (if it shows horses), or after a few more. The likelihood that you can’t decide with certainty whether <span class="math inline"><em>r</em> < ⅓</span> goes down exponentially, so with probability <span class="math inline">1</span>, you will come to a conclusion eventually.</p>
<p>And the good thing is: If you were unlucky and had to throw the coin very often, then you learned a lot about <span class="math inline"><em>r</em></span>, and you can decide the next few prisoners without throwing a coin at all! In this sense, we managed to use “left-over entropy”.</p>
<p>And the other good thing is: There are no rounding errors any more. Every prisoner has the same chance to be freed.</p>
<h3 id="a-visualization">A visualization</h3>
<p>I tried to visualize the whole story, using <a href="https://code.world/">CodeWorld</a>. In <a href="https://code.world/run.html?mode=haskell&dhash=DlHROcVzrb6vCozi0UCqM6A">this not very pretty animation</a>, you see the prisoners (so far just simple numbers) coming from the left. Nisus (not shown) either lets them wait in the slot in the top, or sends them to the right. Sometimes he needs to toss a coin. Below you can see, in numbers and in a bar, what ranges of <span class="math inline"><em>r</em></span> are interesting: In green, the range which indicates that the current prisoner can stay, in red the range where he has to go, and in blue the range that <span class="math inline"><em>r</em></span> is known so far.</p>
<div class="figure">
<img src="//www.joachim-breitner.de/various/nisus-coins-animation.png" alt="Nisus (not shown) at work"/>
<p class="caption">Nisus (not shown) at work</p>
</div>
<p>Probably, by the time you have read this until now, the animation is not at the beginning any more. Move the mouse over it, and you will see controls in the lower left corner; the first button resets the animation. You can also check out the <a href="https://code.world/haskell#P47oXtz3j5Ar4Sc8Bm8NTnA">source code</a>.</p>
<h3 id="open-questions">Open questions</h3>
<p>So Nisus is happy, because with few coin tosses, he can fairly pick a random prisoner to free. I am not fully satisfied yet, because of two option questions:</p>
<ul>
<li>Is this algorithm optimal? (And what does it mean to be optimal?)</li>
<li>What is the expected number of coin throws for <span class="math inline"><em>n</em></span> prisoners? Does this number converge to <span class="math inline">log(<em>n</em>)</span>, which is the entropy of the result?</li>
</ul>
<p>If you know the anwers, let me know!</p>
<h3 id="related-ideas">Related ideas</h3>
<p>Brent Yorgey pointed me to a <a href="https://patternsinfp.wordpress.com/2017/12/05/arithmetic-coding/">sequence of blog posts</a> by Jeremy Gibbons, on “Arithmetic Coding”, which use a similar structure of dividing the unit intervals.</p>Sun, 25 Mar 2018 16:31:57 -0400Interleaving normalizing reduction strategies
http://www.joachim-breitner.de/blog/736-Interleaving_normalizing_reduction_strategies
http://www.joachim-breitner.de/blog/736-Interleaving_normalizing_reduction_strategieshttp://www.joachim-breitner.de/blog/736-Interleaving_normalizing_reduction_strategies#commentsmail@joachim-breitner.de (Joachim Breitner)<p>A little, not very significant, observation about <a href="https://en.wikipedia.org/wiki/Lambda_calculus">lambda calculus</a> and reduction strategies.</p>
<p>A <a href="https://en.wikipedia.org/wiki/Reduction_strategy_(lambda_calculus)">reduction strategy</a> determines, for every lambda term with redexes left, which redex to reduce next. A reduction strategy is normalizing if this procedure terminates for every lambda term that has a normal form.</p>
<p>A fun fact is: If you have two normalizing reduction strategies <span class="math inline"><em>s</em><sub>1</sub></span> and <span class="math inline"><em>s</em><sub>2</sub></span>, consulting them alternately may not yield a normalizing strategy.</p>
<p>Here is an example. Consider the lambda-term <span class="math inline"><em>o</em> = (<em>λ</em><em>x</em>.<em>x</em><em>x</em><em>x</em>)</span>, and note that <span class="math inline"><em>o</em><em>o</em> → <em>o</em><em>o</em><em>o</em> → <em>o</em><em>o</em><em>o</em><em>o</em> → …</span>. Let <span class="math inline"><em>M</em><sub><em>i</em></sub> = (<em>λ</em><em>x</em>.(<em>λ</em><em>x</em>.<em>x</em>))(<em>o</em><em>o</em><em>o</em>…<em>o</em>)</span> (with <span class="math inline"><em>i</em></span> ocurrences of <span class="math inline"><em>o</em></span>). <span class="math inline"><em>M</em><sub><em>i</em></sub></span> has two redexes, and reduces to either <span class="math inline">(<em>λ</em><em>x</em>.<em>x</em>)</span> or <span class="math inline"><em>M</em><sub><em>i</em> + 1</sub></span>. In particular, <span class="math inline"><em>M</em><sub><em>i</em></sub></span> has a normal form.</p>
<p>The two reduction strategies are:</p>
<ul>
<li><span class="math inline"><em>s</em><sub>1</sub></span>, which picks the second redex if given <span class="math inline"><em>M</em><sub><em>i</em></sub></span> for an <em>even</em> <span class="math inline"><em>i</em></span>, and the first (left-most) redex otherwise.</li>
<li><span class="math inline"><em>s</em><sub>2</sub></span>, which picks the second redex if given <span class="math inline"><em>M</em><sub><em>i</em></sub></span> for an <em>odd</em> <span class="math inline"><em>i</em></span>, and the first (left-most) redex otherwise.</li>
</ul>
<p>Both stratgies are normalizing: If during a reduction we come across <span class="math inline"><em>M</em><sub><em>i</em></sub></span>, then the reduction terminates in one or two steps; otherwise we are just doing left-most reduction, which is known to be normalizing.</p>
<p>But if we alternatingly consult <span class="math inline"><em>s</em><sub>1</sub></span> and <span class="math inline"><em>s</em><sub>2</sub></span> while trying to reduce <span class="math inline"><em>M</em><sub>2</sub></span>, we get the sequence</p>
<p><br/><span class="math display"><em>M</em><sub>2</sub> → <em>M</em><sub>3</sub> → <em>M</em><sub>4</sub> → …</span><br/></p>
<p>which shows that this strategy is not normalizing.</p>
<p><strong>Afterthought:</strong> The interleaved strategy is not actually a reduction strategy in the usual definition, as it not a pure (stateless) function from lambda term to redex.</p>Thu, 15 Feb 2018 14:17:58 -0500The magic “Just do it” type class
http://www.joachim-breitner.de/blog/735-The_magic_%E2%80%9CJust_do_it%E2%80%9D_type_class
http://www.joachim-breitner.de/blog/735-The_magic_%E2%80%9CJust_do_it%E2%80%9D_type_classhttp://www.joachim-breitner.de/blog/735-The_magic_%E2%80%9CJust_do_it%E2%80%9D_type_class#commentsmail@joachim-breitner.de (Joachim Breitner)<p>One of the great strengths of strongly typed functional programming is that it allows <em>type driven development</em>. When I have some non-trivial function to write, I first write its type signature, and then the writing the implementation often very obvious.</p>
<h3 id="once-more-i-am-feeling-silly">Once more, I am feeling silly</h3>
<p>In fact, it often is completely mechanical. Consider the following function:</p>
<div class="sourceCode"><pre class="sourceCode hs"><code class="sourceCode haskell"><span class="ot">foo ::</span> (r <span class="ot">-></span> <span class="dt">Either</span> e a) <span class="ot">-></span> (a <span class="ot">-></span> (r <span class="ot">-></span> <span class="dt">Either</span> e b)) <span class="ot">-></span> (r <span class="ot">-></span> <span class="dt">Either</span> e (a,b))</code></pre></div>
<p>This is somewhat like the bind for a combination of the error monad and the reader monad, and remembers the intermediate result, but that doesn’t really matter now. What matters is that once I wrote that type signature, I feel silly having to also write the code, because there isn’t really anything interesting about that.</p>
<p>Instead, I’d like to tell the compiler to just do it for me! I want to be able to write</p>
<div class="sourceCode"><pre class="sourceCode hs"><code class="sourceCode haskell"><span class="ot">foo ::</span> (r <span class="ot">-></span> <span class="dt">Either</span> e a) <span class="ot">-></span> (a <span class="ot">-></span> (r <span class="ot">-></span> <span class="dt">Either</span> e b)) <span class="ot">-></span> (r <span class="ot">-></span> <span class="dt">Either</span> e (a,b))
foo <span class="fu">=</span> justDoIt</code></pre></div>
<p>And now I can! Assuming I am using GHC HEAD (or eventually GHC 8.6), I can run <a href="https://hackage.haskell.org/package/ghc-justdoit"><code>cabal install ghc-justdoit</code></a>, and then the following code actually works:</p>
<div class="sourceCode"><pre class="sourceCode hs"><code class="sourceCode haskell"><span class="ot">{-# OPTIONS_GHC -fplugin=GHC.JustDoIt.Plugin #-}</span>
<span class="kw">import </span><span class="dt">GHC.JustDoIt</span>
<span class="ot">foo ::</span> (r <span class="ot">-></span> <span class="dt">Either</span> e a) <span class="ot">-></span> (a <span class="ot">-></span> (r <span class="ot">-></span> <span class="dt">Either</span> e b)) <span class="ot">-></span> (r <span class="ot">-></span> <span class="dt">Either</span> e (a,b))
foo <span class="fu">=</span> justDoIt</code></pre></div>
<h3 id="what-is-this-justdoit">What is this <code>justDoIt</code>?</h3>
<pre><code>*GHC.LJT GHC.JustDoIt> :browse GHC.JustDoIt
class JustDoIt a
justDoIt :: JustDoIt a => a
(…) :: JustDoIt a => a</code></pre>
<p>Note that there are no instances for the <code>JustDoIt</code> class -- they are created, on the fly, by the GHC plugin <code>GHC.JustDoIt.Plugin</code>. During type-checking, it looks as these <code>JustDoIt t</code> constraints and tries to construct a term of type <code>t</code>. It is based on <a href="https://rd.host.cs.st-andrews.ac.uk/publications/jsl57.pdf">Dyckhoff’s LJT proof search</a> in intuitionistic propositional calculus, which I have <a href="https://github.com/nomeata/ghc-justdoit/blob/master/GHC/LJT.hs">implemented to work directly on GHC’s types and terms</a> (and I find it pretty slick). Those who like Unicode can write <code>(…)</code> instead.</p>
<h3 id="what-is-supported-right-now">What is supported right now?</h3>
<p>Because I am working directly in GHC’s representation, it is pretty easy to support user-defined data types and newtypes. So it works just as well for</p>
<div class="sourceCode"><pre class="sourceCode hs"><code class="sourceCode haskell"><span class="kw">data</span> <span class="dt">Result</span> a b <span class="fu">=</span> <span class="dt">Failure</span> a <span class="fu">|</span> <span class="dt">Success</span> b
<span class="kw">newtype</span> <span class="dt">ErrRead</span> r e a <span class="fu">=</span> <span class="dt">ErrRead</span> {<span class="ot"> unErrRead ::</span> r <span class="ot">-></span> <span class="dt">Result</span> e a }
<span class="ot">foo2 ::</span> <span class="dt">ErrRead</span> r e a <span class="ot">-></span> (a <span class="ot">-></span> <span class="dt">ErrRead</span> r e b) <span class="ot">-></span> <span class="dt">ErrRead</span> r e (a,b)
foo2 <span class="fu">=</span> (…)</code></pre></div>
<p>It doesn’t infer coercions or type arguments or any of that fancy stuff, and carefully steps around anything that looks like it might be recursive.</p>
<h3 id="how-do-i-know-that-it-creates-a-sensible-implementation">How do I know that it creates a sensible implementation?</h3>
<p>You can check the generated Core using <code>-ddump-simpl</code> of course. But it is much more convenient to use <a href="https://github.com/nomeata/inspection-testing"><code>inspection-testing</code></a> to test such things, as I am doing in the <a href="https://github.com/nomeata/ghc-justdoit/blob/master/examples/Demo.hs">Demo file</a>, which you can skim to see a few more examples of <code>justDoIt</code> in action. I very much enjoyed reaping the benefits of the work I put into <code>inspection-testing</code>, as this is so much more convenient than manually checking the output.</p>
<h3 id="is-this-for-real-should-i-use-it">Is this for real? Should I use it?</h3>
<p>Of course you are welcome to play around with it, and it will not launch any missiles, but at the moment, I consider this a prototype that I created for two purposes:</p>
<ul>
<li><p>To demonstrates that you can use type checker plugins for program synthesis. Depending on what you need, this might allow you to provide a smoother user experience than the alternatives, which are:</p>
<ul>
<li>Preprocessors</li>
<li>Template Haskell</li>
<li>Generic programming together with type-level computation (e.g. <a href="http://hackage.haskell.org/package/generic-lens">generic-lens</a>)</li>
<li>GHC Core-to-Core plugins</li>
</ul>
<p>In order to make this viable, I <a href="http://git.haskell.org/ghc.git/commit/0e022e56b130ab9d277965b794e70d8d3fb29533">slightly changed the API</a> for type checker plugins, which are now free to produce arbitrary Core terms as they solve constraints.</p></li>
<li><p>To advertise the idea of taking type-driven computation to its logical conclusion and free users from having to implement functions that they have already specified sufficiently precisely by their type.</p></li>
</ul>
<h3 id="what-needs-to-happen-for-this-to-become-real">What needs to happen for this to become real?</h3>
<p>A bunch of things:</p>
<ul>
<li>The LJT implementation is somewhat neat, but I probably did not implement backtracking properly, and there might be more bugs.</li>
<li>The implementation is very much unoptimized.</li>
<li>For this to be practically useful, the user needs to be able to use it with confidence. In particular, the user should be able to predict what code comes out. If there a multiple possible implementations, i.e. a clear specification which implementations are more desirable than others, and it should probably fail if there is ambiguity.</li>
<li>It ignores any recursive type, so it cannot do anything with lists. It would be much more useful if it could do some best-effort thing here as well.</li>
</ul>
<p>If someone wants to pick it up from here, that’d be great!</p>
<h3 id="i-have-seen-this-before">I have seen this before…</h3>
<p>Indeed, the idea is not new.</p>
<p>Most famously in the Haskell work is certainly Lennart Augustssons’s <a href="http://hackage.haskell.org/package/djinn">Djinn</a> tool that creates Haskell source expression based on types. Alejandro Serrano has connected that to GHC in the library <a href="http://hackage.haskell.org/package/djinn-ghc">djinn-ghc</a>, but I coudn’t use this because it was still outputting Haskell source terms (and it is easier to re-implement LJT rather than to implement type inference).</p>
<p>Lennart Spitzner’s <a href="http://hackage.haskell.org/package/exference">exference</a> is a much more sophisticated tool that also takes library API functions into account.</p>
<p>In the Scala world, Sergei Winitzki very recently presented the pretty neat <a href="https://github.com/Chymyst/curryhoward">curryhoward</a> library that uses for Scala macros. He seems to have some good ideas about ordering solutions by likely desirability.</p>
<p>And in Idris, Joomy Korkut has created <a href="https://github.com/joom/hezarfen">hezarfen</a>.</p>Fri, 02 Feb 2018 14:01:11 -0500Finding bugs in Haskell code by proving it
http://www.joachim-breitner.de/blog/734-Finding_bugs_in_Haskell_code_by_proving_it
http://www.joachim-breitner.de/blog/734-Finding_bugs_in_Haskell_code_by_proving_ithttp://www.joachim-breitner.de/blog/734-Finding_bugs_in_Haskell_code_by_proving_it#commentsmail@joachim-breitner.de (Joachim Breitner)<p>Last week, I wrote a small nifty tool called <a href="https://github.com/nomeata/bisect-binary"><code>bisect-binary</code></a>, which semi-automates answering the question “To what extent can I fill this file up with zeroes and still have it working”. I wrote it it in Haskell, and part of the Haskell code, in the <a href="https://github.com/nomeata/bisect-binary/blob/48f9b9f05509a8b0c15c654f790fefd4e0c22676/src/Intervals.hs">Intervals.hs</a> module, is a data structure for “subsets of a file” represented as a sorted list of intervals:</p>
<pre><code>data Interval = I { from :: Offset, to :: Offset }
newtype Intervals = Intervals [Interval]</code></pre>
<p>The code is the kind of Haskell code that I like to write: A small local recursive function, a few guards to case analysis, and I am done:</p>
<pre><code>intersect :: Intervals -> Intervals -> Intervals
intersect (Intervals is1) (Intervals is2) = Intervals $ go is1 is2
where
go _ [] = []
go [] _ = []
go (i1:is1) (i2:is2)
-- reorder for symmetry
| to i1 < to i2 = go (i2:is2) (i1:is1)
-- disjoint
| from i1 >= to i2 = go (i1:is1) is2
-- subset
| to i1 == to i2 = I f' (to i2) : go is1 is2
-- overlapping
| otherwise = I f' (to i2) : go (i1 { from = to i2} : is1) is2
where f' = max (from i1) (from i2)</code></pre>
<p>But clearly, the code is already complicated enough so that it is easy to make a mistake. I could have put in some QuickCheck properties to test the code, I was in proving mood...</p>
<h3 id="now-available-formal-verification-for-haskell">Now available: Formal Verification for Haskell</h3>
<p>Ten months ago I complained that there was <a href="http://www.joachim-breitner.de/blog/717-Why_prove_programs_equivalent_when_your_compiler_can_do_that_for_you_">no good way to verify Haskell code</a> (and created the nifty hack <a href="https://github.com/nomeata/ghc-proofs"><code>ghc-proofs</code></a>). But things have changed since then, as a group at UPenn (mostly Antal Spector-Zabusky, Stephanie Weirich and myself) has created <a href="https://github.com/antalsz/hs-to-coq"><code>hs-to-coq</code></a>: a translator from Haskell to the theorem prover Coq.</p>
<p>We have used <code>hs-to-coq</code> on various examples, as described in our <a href="https://arxiv.org/abs/1711.09286">CPP'18 paper</a>, but it is high-time to use it for real. The easiest way to use <code>hs-to-coq</code> at the moment is to clone the repository, copy one of the example directories (e.g. <code>examples/successors</code>), place the Haskell file to be verified there and put the right module name into the <code>Makefile</code>. I also commented out parts of the Haskell file that would drag in non-base dependencies.</p>
<h3 id="massaging-the-translation">Massaging the translation</h3>
<p>Often, <code>hs-to-coq</code> translates Haskell code without a hitch, but sometimes, a bit of help is needed. In this case, I had to specify <a href="https://github.com/antalsz/hs-to-coq/blob/8f84d61093b7be36190142c795d6cd4496ef5aed/examples/intervals/edits">three so-called <em>edits</em></a>:</p>
<ul>
<li><p>The Haskell code uses <code>Intervals</code> both as a name for a type and for a value (the constructor). This is fine in Haskell, which has separate value and type namespaces, but not for Coq. The line</p>
<pre><code>rename value Intervals.Intervals = ival</code></pre>
<p>changes the constructor name to <code>ival</code>.</p></li>
<li><p>I use the <code>Int64</code> type in the Haskell code. The Coq version of Haskell’s base library that comes with <code>hs-to-coq</code> does not support that yet, so I change that via</p>
<pre><code>rename type GHC.Int.Int64 = GHC.Num.Int</code></pre>
<p>to the normal <code>Int</code> type, which itself is mapped to <a href="https://coq.inria.fr/library/Coq.Numbers.BinNums.html">Coq’s <code>Z</code> type</a>. This is not a perfect fit, and my verification would not catch problems that arise due to the boundedness of <code>Int64</code>. Since none of my code does arithmetic, only comparisons, I am fine with that.</p></li>
<li><p>The biggest hurdle is the recursion of the local <code>go</code> functions. Coq requires all recursive functions to be obviously (i.e. structurally) terminating, and the <code>go</code> above is not. For example, in the first case, the arguments to <code>go</code> are simply swapped. It is very much not obvious why this is not an infinite loop.</p>
<p>I can specify a termination measure, i.e. a function that takes the arguments <code>xs</code> and <code>ys</code> and returns a “size” of type <code>nat</code> that decreases in every call: Add the lengths of <code>xs</code> and <code>ys</code>, multiply by two and add one if the the first interval in <code>xs</code> ends before the first interval in <code>ys</code>.</p>
<p>If the problematic function were a top-level function I could tell <code>hs-to-coq</code> about this termination measure and it would use this information to define the function using <code>Program Fixpoint</code>.</p>
<p>Unfortunately, <code>go</code> is a local function, so this mechanism is not available to us. If I care more about the verification than about preserving the exact Haskell code, I could easily change the Haskell code to make <code>go</code> a top-level function, but in this case I did not want to change the Haskell code.</p>
<p>Another way out offered by <code>hs-to-coq</code> is to translate the recursive function using an axiom <code>unsafeFix : forall a, (a -> a) -> a</code>. This looks scary, but as I explain in the previous blog post, <a href="http://www.joachim-breitner.de/blog/733-Existence_and_Termination">this axiom can be used in a safe way</a>.</p>
<p>I should point out it is my dissenting opinion to consider this a valid verification approach. The official stand of the <code>hs-to-coq</code> author team is that using <code>unsafeFix</code> in the verification can only be a temporary state, and eventually you’d be expected to fix (heh) this, for example by moving the functions to the top-level and using <code>hs-to-coq</code>’s the support for <code>Program Fixpoint</code>.</p></li>
</ul>
<p>With these edits in place, <code>hs-to-coq</code> splits out a faithful Coq copy of my Haskell code.</p>
<h3 id="time-to-prove-things">Time to prove things</h3>
<p>The rest of the work is mostly straight-forward use of Coq. I define the invariant I expect to hold for these lists of intervals, namely that they are sorted, non-empty, disjoint and non-adjacent:</p>
<pre><code>Fixpoint goodLIs (is : list Interval) (lb : Z) : Prop :=
match is with
| [] => True
| (I f t :: is) => (lb <= f)%Z /\ (f < t)%Z /\ goodLIs is t
end.
Definition good is := match is with
ival is => exists n, goodLIs is n end.</code></pre>
<p>and I give them meaning as Coq type for sets, <a href="https://coq.inria.fr/library/Coq.Sets.Ensembles.html"><code>Ensemble</code></a>:</p>
<pre><code>Definition range (f t : Z) : Ensemble Z :=
(fun z => (f <= z)%Z /\ (z < t)%Z).
Definition semI (i : Interval) : Ensemble Z :=
match i with I f t => range f t end.
Fixpoint semLIs (is : list Interval) : Ensemble Z :=
match is with
| [] => Empty_set Z
| (i :: is) => Union Z (semI i) (semLIs is)
end.
Definition sem is := match is with
ival is => semLIs is end.</code></pre>
<p>Now I prove for every function that it preserves the invariant and that it corresponds to the, well, corresponding function, e.g.:</p>
<pre><code>Lemma intersect_good : forall (is1 is2 : Intervals),
good is1 -> good is2 -> good (intersect is1 is2).
Proof. … Qed.
Lemma intersection_spec : forall (is1 is2 : Intervals),
good is1 -> good is2 ->
sem (intersect is1 is2) = Intersection Z (sem is1) (sem is2).
Proof. … Qed.</code></pre>
<p>Even though I punted on the question of termination while defining the functions, I do not get around that while verifying this, so I formalize the termination argument above</p>
<pre><code>Definition needs_reorder (is1 is2 : list Interval) : bool :=
match is1, is2 with
| (I f1 t1 :: _), (I f2 t2 :: _) => (t1 <? t2)%Z
| _, _ => false
end.
Definition size2 (is1 is2 : list Interval) : nat :=
(if needs_reorder is1 is2 then 1 else 0) + 2 * length is1 + 2 * length is2.</code></pre>
<p>and use it in my inductive proofs.</p>
<p>As I intend this to be a write-once proof, I happily copy’n’pasted proof scripts and did not do any cleanup. Thus, the <a href="https://github.com/antalsz/hs-to-coq/blob/8f84d61093b7be36190142c795d6cd4496ef5aed/examples/intervals/Proofs.v">resulting Proof file</a> is big, ugly and repetitive. I am confident that judicious use of Coq tactics could greatly condense this proof.</p>
<h3 id="using-program-fixpoint-after-the-fact">Using Program Fixpoint after the fact?</h3>
<p>This proofs are also an experiment of how I can actually do induction over a locally defined recursive function without too ugly proof goals (hence the line <code>match goal with [ |- context [unsafeFix ?f _ _] ] => set (u := f) end.</code>). One could improve upon this approach by following these steps:</p>
<ol style="list-style-type: decimal">
<li><p>Define copies (say, <code>intersect_go_witness</code>) of the local <code>go</code> using <code>Program Fixpoint</code> with the above termination measure. The termination argument needs to be made only once, here.</p></li>
<li><p>Use this function to prove that the argument <code>f</code> in <code>go = unsafeFix f</code> actually has a fixed point:</p>
<pre><code>Lemma intersect_go_sound:</code></pre>
<p>f intersect_go_witness = intersect_go_witness</p>
<p>(This requires functional extensionality). This lemma indicates that my use of the axioms <code>unsafeFix</code> and <code>unsafeFix_eq</code> are actually sound, as discussed in the previous blog post.</p></li>
<li><p>Still prove the desired properties for the <code>go</code> that uses <code>unsafeFix</code>, as before, but using the <a href="https://coq.inria.fr/refman/schemes.html#sec655">functional induction scheme</a> for <code>intersect_go</code>! This way, the actual proofs are free from any noisy termination arguments.</p>
<p>(The trick to define a recursive function just to throw away the function and only use its induction rule is one I learned in Isabelle, and is very useful to separate the meat from the red tape in complex proofs. Note that the induction rule for a function does not actually mention the function!)</p></li>
</ol>
<p>Maybe I will get to this later.</p>
<p><strong>Update:</strong> I experimented a bit in that direction, and it does not quite work as expected. In step 2 I am stuck because <code>Program Fixpoint</code> does not create a fixpoint-unrolling lemma, and in step 3 I do not get the induction scheme that I was hoping for. Both problems <a href="https://stackoverflow.com/a/46995609/946226">would not exist if I use the <code>Function</code> command</a>, although that needs some tickery to support a termination measure on multiple arguments. The induction lemma is not quite as polished as I was hoping for, so <a href="https://github.com/antalsz/hs-to-coq/blob/b7efc7a8dbacca384596fc0caf65e62e87ef2768/examples/intervals/Proofs_Function.v">he resulting proof</a> is still somewhat ugly, and it requires copying code, which does not scale well.</p>
<h3 id="efforts-and-gains">Efforts and gains</h3>
<p>I spent exactly 7 hours working on these proofs, according to <a href="http://arbtt.nomeata.de/"><code>arbtt</code></a>. I am sure that writing these functions took me much less time, but I cannot calculate that easily, as they were originally in the <code>Main.hs</code> file of <code>bisect-binary</code>.</p>
<p>I did <a href="https://github.com/nomeata/bisect-binary/commit/48f9b9f05509a8b0c15c654f790fefd4e0c22676#diff-38999f20f11fe6a93fa194587e8ad507">find and fix three bugs</a>:</p>
<ul>
<li>The <code>intersect</code> function would not always retain the invariant that the intervals would be non-empty.</li>
<li>The <code>subtract</code> function would prematurely advance through the list intervals in the second argument, which can lead to a genuinely wrong result. (This occurred twice.)</li>
</ul>
<p><strong>Conclusion:</strong> Verification of Haskell code using Coq is now practically possible!</p>
<p><strong>Final rant:</strong> Why is the Coq standard library so incomplete (compared to, say, Isabelle’s) and requires me to prove <a href="https://github.com/antalsz/hs-to-coq/blob/8f84d61093b7be36190142c795d6cd4496ef5aed/examples/intervals/Ensemble_facts.v">so many lemmas about basic functions on <code>Ensembles</code></a>?</p>Tue, 05 Dec 2017 09:17:43 -0500Existence and Termination
http://www.joachim-breitner.de/blog/733-Existence_and_Termination
http://www.joachim-breitner.de/blog/733-Existence_and_Terminationhttp://www.joachim-breitner.de/blog/733-Existence_and_Termination#commentsmail@joachim-breitner.de (Joachim Breitner)<p>I recently had some intense discussions that revolved around issues of existence and termination of functions in Coq, about axioms and what certain proofs actually mean. We came across some interesting questions and thoughts that I’ll share with those of my blog readers with an interest in proofs and interactive theorem proving.</p>
<h3 id="tldr">tl;dr</h3>
<ul>
<li>It can be meaningful to assume the <em>existence</em> of a function in Coq, and under that assumption prove its <em>termination</em> and other properties.</li>
<li>Axioms and assumptions are logically equivalent.</li>
<li>Unsound axioms do not necessary invalidate a theory development, when additional meta-rules govern their use.</li>
</ul>
<h3 id="preparation">Preparation</h3>
<p>Our main running example is the infamous Collatz series. Starting at any natural number, the next is calculated as follow:</p>
<pre><code>Require Import Coq.Arith.Arith.
Definition next (n : nat) :nat :=
if Nat.even n then n / 2 else 3*n + 1.</code></pre>
<p>If you start with some positive number, you are going to end up reaching 1 eventually. Or are you? So far nobody has found a number where that does not happen, but we also do not have a proof that it never happens. It is one of the <a href="https://en.wikipedia.org/wiki/Collatz_conjecture">great mysteries of Mathematics</a>, and if you can solve it, you’ll be famous.</p>
<h3 id="a-failed-definition">A failed definition</h3>
<p>But assume we had an idea on how to prove that we are always going to reach 1, and tried to formalize this in Coq. One attempt might be to write</p>
<pre><code>Fixpoint good (n : nat) : bool :=
if n <=? 1
then true
else good (next n).
Theorem collatz: forall n, good n = true.
Proof. (* Insert genius idea here.*) Qed.</code></pre>
<p>Unfortunately, this does not work: Coq rejects this recursive definition of the function <code>good</code>, because it does not see how that is a terminating function, and Coq requires all such recursive function definitions to be obviously terminating – without this check there would be a risk of Coq’s type checking becoming incomplete or its logic being unsound.</p>
<p>The idiomatic way to avoid this problem is to state <code>good</code> as an inductive predicate... but let me explore another idea here.</p>
<h3 id="working-with-assumptions">Working with assumptions</h3>
<p>What happens if we just assume that the function <code>good</code>, described above, exists, and then perform our proof:</p>
<pre><code>Theorem collatz
(good : nat -> bool)
(good_eq : forall n,
good n = if n <=? 1 then true else good (next n))
: forall n, good n = true.
Proof. (* Insert genius idea here.*) Qed.</code></pre>
<p>Would we accept this as a proof of Collatz’ conjecture? Or did we just assume what we want to prove, in which case the theorem is vacuously true, but we just performed useless circular reasoning?</p>
<p>Upon close inspection, we find that the assumptions of the theorem (<code>good</code> and <code>good_eq</code>) are certainly satisfiable:</p>
<pre><code>Definition trivial (n: nat) : bool := true.
Lemma trivial_eq: forall n,
trivial n = if n <=? 1 then true else trivial (next n).
Proof. intro; case (n <=? 1); reflexivity. Qed.
Lemma collatz_trivial: forall n, trivial n = true.
Proof.
apply (collatz trivial trivial_eq).
Qed.</code></pre>
<p>So clearly there exists a function of type <code>nat -> bool</code> that satisfies the assumed equation. This is good, because it means that the <code>collatz</code> theorem is not simply assuming <code>False</code>!</p>
<p>Some (including me) might already be happy with this theorem and proof, as it clearly states: “Every function that follows the Collatz series eventually reaches 1”.</p>
<p>Others might still not be at ease with such a proof. Above we have seen that we cannot define the real collatz series in Coq. How can the <code>collatz</code> theorem say something that is not definable?</p>
<h3 id="classical-reasoning">Classical reasoning</h3>
<p>One possible way of getting some assurance it to define <code>good</code> as a classical function. The logic of Coq can be extended with the law of the excluded middle without making it inconsistent, and with that axiom, we can define a version of <code>good</code> that is pretty convincing (sorry for the slightly messy proof):</p>
<pre><code>Require Import Coq.Logic.ClassicalDescription.
Require Import Omega.
Definition classical_good (n:nat) : bool :=
if excluded_middle_informative (exists m, Nat.iter m next n <= 1)
then true else false.
Lemma iter_shift:
forall a f x (y:a), Nat.iter x f (f y) = f (Nat.iter x f y).
Proof.
intros. induction x. reflexivity. simpl. rewrite IHx. reflexivity. Qed.
Lemma classical_good_eq: forall n,
classical_good n = if n <=? 1 then true else classical_good (next n).
Proof.
intros.
unfold classical_good at 1.
destruct (Nat.leb_spec n 1).
* destruct (excluded_middle_informative _); try auto.
contradict n0. exists 0. simpl. assumption.
* unfold classical_good.
destruct (Nat.eqb_spec (next n) 0); try auto.
destruct (excluded_middle_informative _), (excluded_middle_informative _); auto.
- contradict n0.
destruct e0.
destruct x; simpl in *. omega.
exists x. rewrite iter_shift. assumption.
- contradict n0.
destruct e0.
exists (S x). simpl. rewrite iter_shift in H0. assumption.
Qed.
Lemma collatz_classical: forall n, classical_good n = true.
Proof. apply (collatz classical_good classical_good_eq). Qed.</code></pre>
<p>The point of this is not so much to use this particular definition of <code>good</code>, but merely to convince ourselves that the assumptions of the <code>collatz</code> theorem above encompass “the” Collatz series, and thus constitutes a proof of the Collatz conjecture.</p>
<p>The main take-away so far is that <strong>existence and termination of a function</strong> are two separate issues, and it is possible to assume the former, prove the latter, and not have done a vacuous proof.</p>
<h3 id="the-ice-gets-thinner">The ice gets thinner</h3>
<h4 id="sections">Sections</h4>
<p>Starting with the above <code>Theorem collatz</code>, there is another train of thought I invite to to follow along.</p>
<p>Probably the “genius idea” proof will be more than a few lines long, and we probably to be able to declare helper lemmas and other things along the way. Doing all that in the body of the <code>collatz</code> proof is not very convenient, so instead of using assumptions, we might write</p>
<pre><code>Section collatz:
Variable good : nat -> bool.
Variable good_eq : forall n,
good n = if n <=? 1 then true else good (next n)
Theorem collatz2 : forall n, good n = true.
Proof. (* Insert genius idea here.*) Qed.
End collatz.</code></pre>
<p>So far so good: Clearly, I just refactored my code a bit, but did not make any significant change. The theorems <code>collatz2</code> and <code>collatz</code> are equivalent.</p>
<h4 id="sound-axioms">Sound axioms</h4>
<p>But note that we do not really intend to instantiate <code>collatz2</code>. We know that the assumptions are satisfiable (e.g. since we can define <code>trivial</code> or <code>classical_good</code>). So maybe, we would rather avoid the <code>Section</code> mechanism and simply write</p>
<pre><code>Axiom good : nat -> bool.
Axiom good_eq : forall n,
good n = if n <=? 1 then true else good (next n)
Theorem collatz3 : forall n, good n = true.
Proof. (* Insert genius idea here.*) Qed.</code></pre>
<p>I assume this will make a few of my readers’ eyebrows go up: How can I dare to start with such Axioms? Do they not invalidate my whole development?</p>
<p>On the other hand, all that a Coq axiom is doing is saying “the following theorems are under the assumption that the axiom holds”. In that sense, <code>collatz3</code> and <code>collatz2</code> are essentially equivalent.</p>
<h4 id="unsound-axioms">Unsound axioms</h4>
<p>Let me take it one step further, and change that to:</p>
<pre><code>Axiom unsafeFix : forall a, (a -> a) -> a.
Axiom unsafeFix_eq : forall f, unsafeFix f = f (unsafeFix f).
Definition good : nat -> bool :=
unsafeFix (fun good n => if n <=? 1 then true else good (next n)).
Theorem collatz4 : forall n, good n = true.
Proof. (* Insert genius idea here.*) Qed.</code></pre>
<p>At this point, the majority of my readers <em>will</em> cringe. The axiom <code>unsafeFix</code> is so blatantly unsound (in Coq), how do I even dare to think of using it. But bear with me for a moment: I did not change the proof. So maybe the <code>collatz4</code> theorem is still worth something?</p>
<p>I want to argue that it is: Both <code>unsafeFix</code> and <code>unsafeFix_eq</code> are unsound in their full generality. But as long as I instantiate them only with functions <code>f</code> which have a fixpoint, then I cannot prove <code>False</code> this way. So while “Coq + <code>unsafeFix</code>” is unsound, “Coq + <code>unsafeFix</code> + <code>unsafeFix_eq</code> + metarule that these axioms are only called with permissible <code>f</code>” is not.</p>
<p>In that light, my <code>collatz4</code> proof carries the same meaning as the <code>collatz3</code> proof, it is just less convenient to check: If I were to check the validity of <code>collatz3</code>, I have to maybe look for uses of <code>admit</code>, or some misleading use of syntax or other tricks, or other smells. When I have to check the validity of <code>collatz4</code>, I also have to additionally check the meta-rule -- tedious, but certainly possible (e.g. by inspecting the proof term).</p>
<h3 id="beyond-collatz">Beyond Collatz</h3>
<p>The questions discussed here did not come up in the context of the Collatz series (for which I unfortunately do not have a proof), but rather the verification of Haskell code in Coq using <a href="https://github.com/antalsz/hs-to-coq"><code>hs-to-coq</code></a>. I started with the idiomatic Haskell definition of “Quicksort”:</p>
<div class="sourceCode"><pre class="sourceCode hs"><code class="sourceCode haskell"><span class="ot">quicksort ::</span> <span class="dt">Ord</span> a <span class="ot">=></span> [a] <span class="ot">-></span> [a]
quicksort [] <span class="fu">=</span> []
quicksort (p<span class="fu">:</span>xs) <span class="fu">=</span> quicksort lesser <span class="fu">++</span> [p] <span class="fu">++</span> quicksort greater
<span class="kw">where</span> (lesser, greater) <span class="fu">=</span> partition (<span class="fu"><</span>p) xs</code></pre></div>
<p>This function is not terminating in a way that is obvious to the Coq type checker. Conveniently, <code>hs-to-coq</code> can optionally create the Coq code using the <code>unsafeFix</code> axiom above, producing (roughly):</p>
<pre><code>Definition quicksort {a} `{Ord a} : list a -> list a :=
unsafeFix (fun quicksort xs =>
match xs with
| nil => nil
| p :: xs => match partition (fun x => x <? p) xs with
| (lesser, greater) => quicksort lesser ++ [p] ++ quicksort greater
end
end).</code></pre>
<p>I <a href="https://github.com/antalsz/hs-to-coq/tree/a8cfb747cee2dbe7ce77b3a118958af99c090768/examples/ghc-base/quicksort">then proved</a> (roughly)</p>
<pre><code>Theorem quicksort_sorted:
forall a `(Ord a) (xs : list a), StronglySorted (quicksort xs).</code></pre>
<p>and</p>
<pre><code>Theorem quicksort_permutation:
forall a `(Ord a) (xs : list a), Permutation (quicksort xs) xs.</code></pre>
<p>These proofs proceed by well-founded induction on the length of the argument <code>xs</code>, and hence encompass a termination proof of <code>quicksort</code>. Note that with a only <em>partially</em> correct but non-terminating definition of <code>quicksort</code> (e.g. <code>quicksort := unsafeFix (fun quicksort xs => quicksort xs)</code>) I would not be able to conclude these proofs.</p>
<p>My (not undisputed) claim about the meaning of these theorems is therefore</p>
<blockquote>
<p>If the Haskell equations for <code>quicksort</code> actually have a fixed point, then the use of <code>unsafeFix</code> in its definition does not introduce any inconsistency. Under this assumption, we showed that <code>quicksort</code> always terminates and produces a sorted version of the input list.</p>
</blockquote>
<p>Do you agree?</p>Sat, 25 Nov 2017 15:54:57 -0500Isabelle functions: Always total, sometimes undefined
http://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined
http://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefinedhttp://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined#commentsmail@joachim-breitner.de (Joachim Breitner)<p>Often, when I mention how things work in the interactive theorem prover [Isabelle/HOL] (in the following just “Isabelle”<a href="#fn1" class="footnoteRef" id="fnref1"><sup>1</sup></a>) to people with a strong background in functional programming (whether that means Haskell or Coq or something else), I cause confusion, especially around the issue of <em>what is a function</em>, are function <em>total</em> and what is the business with <em>undefined</em>. In this blog post, I want to explain some these issues, aimed at functional programmers or type theoreticians.</p>
<p>Note that this is not meant to be a tutorial; I will not explain how to do these things, and will focus on what they mean.</p>
<h3 id="hol-is-a-logic-of-total-functions">HOL is a logic of total functions</h3>
<p>If I have a Isabelle function <code>f :: a ⇒ b</code> between two types <code>a</code> and <code>b</code> (the function arrow in Isabelle is <code>⇒</code>, not <code>→</code>), then – by definition of what it means to be a function in HOL – whenever I have a value <code>x :: a</code>, then the expression <code>f x</code> (i.e. <code>f</code> applied to <code>x</code>) <em>is</em> a value of type <code>b</code>. Therefore, and without exception, <em>every Isabelle function is total</em>.</p>
<p>In particular, it cannot be that <code>f x</code> does not exist for some <code>x :: a</code>. This is a first difference from Haskell, which does have partial functions like</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">spin ::</span> <span class="dt">Maybe</span> <span class="dt">Integer</span> <span class="ot">-></span> <span class="dt">Bool</span>
spin (<span class="dt">Just</span> n) <span class="fu">=</span> spin (<span class="dt">Just</span> (n<span class="fu">+</span><span class="dv">1</span>))</code></pre></div>
<p>Here, neither the expression <code>spin Nothing</code> nor the expression <code>spin (Just 42)</code> produce a value of type <code>Bool</code>: The former raises an exception (“incomplete pattern match”), the latter does not terminate. Confusingly, though, both expressions have type <code>Bool</code>.</p>
<p>Because every function is total, this confusion cannot arise in Isabelle: If an expression <code>e</code> has type <code>t</code>, then it <em>is</em> a value of type <code>t</code>. This trait is shared with other total systems, including Coq.</p>
<p>Did you notice the emphasis I put on the word “is” here, and how I deliberately did not write “evaluates to” or “returns”? This is because of another big source for confusion:</p>
<h3 id="isabelle-functions-do-not-compute">Isabelle functions do not compute</h3>
<p>We (i.e., functional programmers) stole the word “function” from mathematics and repurposed it<a href="#fn2" class="footnoteRef" id="fnref2"><sup>2</sup></a>. But the word “function”, in the context of Isabelle, refers to the mathematical concept of a function, and it helps to keep that in mind.</p>
<p>What is the difference?</p>
<ul>
<li>A function <code>a → b</code> in functional programming is an algorithm that, given a value of type <code>a</code>, calculates (returns, evaluates to) a value of type <code>b</code>.</li>
<li>A function <code>a ⇒ b</code> in math (or Isabelle) associates with each value of type <code>a</code> a value of type <code>b</code>.</li>
</ul>
<p>For example, the following is a perfectly valid function definition in math (and HOL), but could not be a function in the programming sense:</p>
<pre class="isabelle"><code>definition foo :: "(nat ⇒ real) ⇒ real" where
"foo seq = (if convergent seq then lim seq else 0)"</code></pre>
<p>This assigns a real number to every sequence, but it does not <em>compute</em> it in any useful sense.</p>
<p>From this it follows that</p>
<h3 id="isabelle-functions-are-specified-not-defined">Isabelle functions are specified, not defined</h3>
<p>Consider this function definition:</p>
<pre class="isabelle"><code>fun plus :: "nat ⇒ nat ⇒ nat" where
"plus 0 m = m"
| "plus (Suc n) m = Suc (plus n m)"</code></pre>
<p>To a functional programmer, this reads</p>
<blockquote>
<p><code>plus</code> is a function that analyses its first argument. If that is <code>0</code>, then it returns the second argument. Otherwise, it calls itself with the predecessor of the first argument and increases the result by one.</p>
</blockquote>
<p>which is clearly a description of a computation.</p>
<p>But to Isabelle, the above reads</p>
<blockquote>
<p><code>plus</code> is a binary function on natural numbers, and it satisfies the following two equations: …</p>
</blockquote>
<p>And in fact, it is not so much Isabelle that reads it this way, but rather the <code>fun</code> command, which is external to the Isabelle logic. The <code>fun</code> command analyses the given equations, constructs a non-recursive definition of <code>plus</code> under the hood, passes <em>that</em> to Isabelle and then proves that the given equations hold for <code>plus</code>.</p>
<p>One interesting consequence of this is that different specifications can lead to the same functions. In fact, if we would define <code>plus'</code> by recursing on the second argument, we’d obtain the the same function (i.e. <code>plus = plus'</code> is a theorem, and there would be no way of telling the two apart).</p>
<h3 id="termination-is-a-property-of-specifications-not-functions">Termination is a property of specifications, not functions</h3>
<p>Because a function does not evaluate, it does not make sense to ask if it terminates. The question of termination arises <em>before</em> the function is defined: The <code>fun</code> command can only construct <code>plus</code> in a way that the equations hold if it passes a termination check – very much like <code>Fixpoint</code> in Coq.</p>
<p>But while the termination check of <code>Fixpoint</code> in Coq is a deep part of the basic logic, in Isabelle it is simply something that this particular command requires for its internal machinery to go through. At no point does a “termination proof of the function” exist as a theorem inside the logic. And other commands may have other means of defining a function that do not even require such a termination argument!</p>
<p>For example, a function specification that is tail-recursive can be turned in to a function, even without a termination proof: The following definition describes a higher-order function that iterates its first argument <code>f</code> on the second argument <code>x</code> until it finds a fixpoint. It is completely polymorphic (the single quote in <code>'a</code> indicates that this is a type variable):</p>
<pre class="isabelle"><code>partial_function (tailrec)
fixpoint :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a"
where
"fixpoint f x = (if f x = x then x else fixpoint f (f x))"</code></pre>
<p>We can work with this definition just fine. For example, if we instantiate <code>f</code> with <code>(λx. x-1)</code>, we can prove that it will always return 0:</p>
<pre class="isabelle"><code>lemma "fixpoint (λ n . n - 1) (n::nat) = 0"
by (induction n) (auto simp add: fixpoint.simps)</code></pre>
<p>Similarly, if we have a function that works within the option monad (i.e. |Maybe| in Haskell), its specification can always be turned into a function without an explicit termination proof – here one that calculates the Collatz sequence:</p>
<pre class="isabelle"><code>partial_function (option) collatz :: "nat ⇒ nat list option"
where "collatz n =
(if n = 1 then Some [n]
else if even n
then do { ns <- collatz (n div 2); Some (n # ns) }
else do { ns <- collatz (3 * n + 1); Some (n # ns)})"</code></pre>
<p>Note that lists in Isabelle are finite (like in Coq, unlike in Haskell), so this function “returns” a list only if the collatz sequence eventually reaches 1.</p>
<p>I expect these definitions to make a Coq user very uneasy. How can <code>fixpoint</code> be a total function? What is <code>fixpoint (λn. n+1)</code>? What if we run <code>collatz n</code> for a <code>n</code> where the <a href="https://en.wikipedia.org/wiki/Collatz_conjecture">Collatz sequence</a> does <em>not</em> reach 1?<a href="#fn3" class="footnoteRef" id="fnref3"><sup>3</sup></a> We will come back to that question after a little detour…</p>
<h3 id="hol-is-a-logic-of-non-empty-types">HOL is a logic of non-empty types</h3>
<p>Another big difference between Isabelle and Coq is that in Isabelle, <em>every type is inhabited</em>. Just like the totality of functions, this is a very fundamental fact about what HOL defines to be a type.</p>
<p>Isabelle gets away with that design because in Isabelle, we do not use types for propositions (like we do in Coq), so we do not need empty types to denote false propositions.</p>
<p>This design has an important consequence: It allows the existence of a polymorphic expression that inhabits any type, namely</p>
<pre class="isabelle"><code>undefined :: 'a</code></pre>
<p>The naming of this term alone has caused a great deal of confusion for Isabelle beginners, or in communication with users of different systems, so I implore you to not read too much into the name. In fact, you will have a better time if you think of it as <code>arbitrary</code> or, even better, <code>unknown</code>.</p>
<p>Since <code>undefined</code> can be instantiated at any type, we can instantiate it for example at <code>bool</code>, and we can observe an important fact: <code>undefined</code> is not an <em>extra</em> value besides the “usual ones”. It is simply <em>some</em> value of that type, which is demonstrated in the following lemma:</p>
<pre class="isabelle"><code>lemma "undefined = True ∨ undefined = False" by auto</code></pre>
<p>In fact, if the type has only one value (such as the unit type), then we know the value of <code>undefined</code> for sure:</p>
<pre class="isabelle"><code>lemma "undefined = ()" by auto</code></pre>
<p>It is very handy to be able to produce an expression of any type, as we will see as follows</p>
<h3 id="partial-functions-are-just-underspecified-functions">Partial functions are just underspecified functions</h3>
<p>For example, it allows us to translate incomplete function specifications. Consider this definition, Isabelle’s equivalent of Haskell’s partial <code>fromJust</code> function:</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell">fun<span class="ot"> fromSome ::</span> <span class="st">"'a option ⇒ 'a"</span> <span class="kw">where</span>
<span class="st">"fromSome (Some x) = x"</span></code></pre></div>
<p>This definition is accepted by <code>fun</code> (albeit with a warning), and the generated function <code>fromSome</code> behaves exactly as specified: when applied to <code>Some x</code>, it is <code>x</code>. The term <code>fromSome None</code> is also a value of type <code>'a</code>, we just do not know which one it is, as the specification does not address that.</p>
<p>So <code>fromSome None</code> behaves just like <code>undefined</code> above, i.e. we can prove</p>
<pre class="isabelle"><code>lemma "fromSome None = False ∨ fromSome None = True" by auto</code></pre>
<p>Here is a small exercise for you: Can you come up with an explanation for the following lemma:</p>
<pre class="isabelle"><code>fun constOrId :: "bool ⇒ bool" where
"constOrId True = True"
lemma "constOrId = (λ_.True) ∨ constOrId = (λx. x)"
by (metis (full_types) constOrId.simps)</code></pre>
<p>Overall, this behavior makes sense if we remember that function “definitions” in Isabelle are not really definitions, but rather specifications. And a partial function “definition” is simply a underspecification. The resulting function is simply any function hat fulfills the specification, and the two lemmas above underline that observation.</p>
<h3 id="nonterminating-functions-are-also-just-underspecified">Nonterminating functions are also just underspecified</h3>
<p>Let us return to the puzzle posed by <code>fixpoint</code> above. Clearly, the function – seen as a functional program – is not total: When passed the argument <code>(λn. n + 1)</code> or <code>(λb. ¬b)</code> it will loop forever trying to find a fixed point.</p>
<p>But Isabelle functions are not functional programs, and the definitions are just specifications. What does the specification say about the case when <code>f</code> has no fixed-point? It states that the equation <code>fixpoint f x = fixpoint f (f x)</code> holds. And this equation has a solution, for example <code>fixpoint f _ = undefined</code>.</p>
<p>Or more concretely: The specification of the <code>fixpoint</code> function states that <code>fixpoint (λb. ¬b) True = fixpoint (λb. ¬b) False</code> has to hold, but it does not specify which particular value (<code>True</code> or <code>False</code>) it should denote – any is fine.</p>
<h3 id="not-all-function-specifications-are-ok">Not all function specifications are ok</h3>
<p>At this point you might wonder: Can I just specify any equations for a function <code>f</code> and get a function out of that? But rest assured: That is not the case. For example, no Isabelle command allows you define a function <code>bogus :: () ⇒ nat</code> with the equation <code>bogus () = Suc (bogus ())</code>, because this equation does not have a solution.</p>
<p>We can actually prove that such a function cannot exist:</p>
<pre class="isabelle"><code>lemma no_bogus: "∄ bogus. bogus () = Suc (bogus ())" by simp</code></pre>
<p>(Of course, <code>not_bogus () = not_bogus ()</code> is just fine…)</p>
<h3 id="you-cannot-reason-about-partiality-in-isabelle">You cannot reason about partiality in Isabelle</h3>
<p>We have seen that there are many ways to define functions that one might consider “partial”. Given a function, can we prove that it is not “partial” in that sense?</p>
<p>Unfortunately, but unavoidably, no: Since <code>undefined</code> is not a separate, recognizable value, but rather simply an unknown one, there is no way of stating that “A function result is not specified”.</p>
<p>Here is an example that demonstrates this: Two “partial” functions (one with not all cases specified, the other one with a self-referential specification) are indistinguishable from the total variant:</p>
<pre class="isabelle"><code>fun partial1 :: "bool ⇒ unit" where
"partial1 True = ()"
partial_function (tailrec) partial2 :: "bool ⇒ unit" where
"partial2 b = partial2 b"
fun total :: "bool ⇒ unit" where
"total True = ()"
| "total False = ()"
lemma "partial1 = total ∧ partial2 = total" by auto</code></pre>
<p>If you really <em>do</em> want to reason about partiality of functional programs in Isabelle, you should consider implementing them not as plain HOL functions, but rather use <a href="http://isabelle.in.tum.de/dist/library/HOL/HOLCF/README.html">HOLCF</a>, where you can give equational specifications of functional programs and obtain <em>continuous functions</em> between <em>domains</em>. In that setting, <code>⊥ ≠ ()</code> and <code>partial2 = ⊥ ≠ total</code>. We have done that <a href="https://arxiv.org/abs/1306.1340">to verify some of HLint’s equations</a>.</p>
<h3 id="you-can-still-compute-with-isabelle-functions">You can still compute with Isabelle functions</h3>
<p>I hope by this point, I have not scared away anyone who wants to use Isabelle for functional programming, and in fact, you can use it for that. If the equations that you pass to `fun are a reasonable definition for a function (in the programming sense), then these equations, used as rewriting rules, will allow you to “compute” that function quite like you would in Coq or Haskell.</p>
<p>Moreover, Isabelle supports code extraction: You can take the equations of your Isabelle functions and have them expored into Ocaml, Haskell, Scala or Standard ML. See <a href="http://www21.in.tum.de/~popescua/rs3/CoCon.html">Concon</a> for a conference management system with confidentially verified in Isabelle.</p>
<p>While these usually are the equations you defined the function with, they don't have to: You can declare other proved equations to be used for code extraction, e.g. to refine your elegant definitions to performant ones.</p>
<p>Like with code extraction from Coq to, say, Haskell, the adequacy of the translations rests on a <a href="http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html">“moral reasoning” foundation</a>. Unlike extraction from Coq, where you have an (unformalized) guarantee that the resulting Haskell code is terminating, you do not get that guarantee from Isabelle. Conversely, this allows you do reason about and extract non-terminating programs, like <code>fixpoint</code>, which is not possible in Coq.</p>
<p>There is <a href="https://www21.in.tum.de/~hupel/pub/isabelle-cakeml.pdf">currently ongoing work</a> about verified code generation, where the code equations are reflected into a deep embedding of HOL in Isabelle that would allow explicit termination proofs.</p>
<h3 id="conclusion">Conclusion</h3>
<p>We have seen how in Isabelle, <em>every function is total</em>. Function declarations have equations, but these do not <em>define</em> the function in an computational sense, but rather <em>specify</em> them. Because in HOL, there are no empty types, many specifications that appear partial (incomplete patterns, non-terminating recursion) have solutions in the space of total functions. Partiality in the specification is no longer visible in the final product.</p>
<h3 id="ps-axiom-undefined-in-coq">PS: Axiom <code>undefined</code> in Coq</h3>
<p><em>This section is speculative, and an invitation for discussion.</em></p>
<p>Coq already distinguishes between types used in programs (<code>Set</code>) and types used in proofs <code>Prop</code>.</p>
<p>Could Coq ensure that every <code>t : Set</code> is non-empty? I imagine this would require additional checks in the <code>Inductive</code> command, similar to the checks that the Isabelle command <code>datatype</code> has to perform<a href="#fn4" class="footnoteRef" id="fnref4"><sup>4</sup></a>, and it would disallow <a href="https://coq.inria.fr/library/Coq.Init.Datatypes.html"><code>Empty_set</code></a>.</p>
<p>If so, then it would be sound to add the following axiom</p>
<pre class="coq"><code>Axiom undefined : forall (a : Set), a.</code></pre>
<p>wouldn't it? This axiom does not have any computational meaning, but that seems to be ok for optional Coq axioms, like classical reasoning or function extensionality.</p>
<p>With this in place, how much of what I describe above about function definitions in Isabelle could now be done soundly in Coq. Certainly pattern matches would not have to be complete and could sport an implicit case <code>_ ⇒ undefined</code>. Would it “help” with non-obviously terminating functions? Would it allow a Coq command <code>Tailrecursive</code> that accepts any tailrecursive function without a termination check?</p>
<div class="footnotes">
<hr/>
<ol>
<li id="fn1"><p>Isabelle is a metalogical framework, and other logics, e.g. Isabelle/ZF, behave differently. For the purpose of this blog post, I always mean Isabelle/HOL.<a href="#fnref1">↩</a></p></li>
<li id="fn2"><p>Isabelle is a metalogical framework, and other logics, e.g. Isabelle/ZF, behave differently. For the purpose of this blog post, I always mean Isabelle/HOL.<a href="#fnref2">↩</a></p></li>
<li id="fn3"><p>Let me know if you find such an <span class="math inline"><em>n</em></span>. Besides <span class="math inline"><em>n</em> = 0</span>.<a href="#fnref3">↩</a></p></li>
<li id="fn4"><p>Like <code>fun</code>, the constructions by <code>datatype</code> are not part of the logic, but create a type definition from more primitive notions that is isomorphic to the specified data type.<a href="#fnref4">↩</a></p></li>
</ol>
</div>Thu, 12 Oct 2017 13:54:20 -0400