Unary arithmetics is even slower than you'd expect

My coworker Encsé posted a challange use the 9-digit number problem to demonstrate interesting programming techniques. So I sat down and wrote my first practical program using dependant types, in Agda. I've been playing around with Agda previously, but this seemed like a good opportunity to try to write an actual, self-contained, provably correct program with it.

I'm not going to get into details now about the resulting Agda code, because I'm planning to present it in detail in a later post. In its current form, my program is formally proven to produce only good nine-digit numbers; the only property that still needs proving is that it finds all of them.

But the sad surprise came when I tried to actually run it. It was unbearably slow to just get to all possible combinations for the first three digits. I'm talking about 12 minutes just to list them from 123 to 423 (at which point I killed the process). For comparison, the following Haskell program, which is an implementation of the same naïve algorithm, finds the (unique) solution in 4 milliseconds:

import Control.Monad.List

fromDigits = foldr shift 0
    where shift d s = 10 * s + d

p `divides` q = q `mod` p == 0

encse :: [Int]
encse = map fromDigits $ encse' 0 []
    where encse' 9 ds = return ds
          encse' n ds = do d <- [1..9]
                           let ds' = d:ds
                               n' = n + 1
                           guard $ not (d `elem` ds)
                           guard $ n' `divides` fromDigits ds'
                           encse' n' ds'
      

So where's that slowdown coming from?

The first intuition would be that the code generated by Agda is slow because in parallel to the actual computation, it is also evaluating all kinds of proofs. But the proofs exist only in the world of types, so they shouldn't matter once the program is compiled.

The real answer is that calculating in unary representation is slow. Very, very slow. Even slower than you'd imagine.

The B Method for Programmers (Part 2)

In my previous post, I introduced the B method and showed the steps of writing a simple program for finding the n^th element of a sequence satisfying a given predicate p. While you may think the resulting program is correct, we can't just say so and be done with it. The whole point of the B method is that the resulting program can be formally proven correct.

The B software generates 69 so-called proof obligations for the code from the first part. These are assertions about the program actually behaving as specified. For example, let's look at PO69 which asserts that ll is correctly set. Recall first the relevant portion of the specification:

And the invariant of the implementation:

So what we have to prove is that given the preconditions, by the time the loop in the implementation terminates, the invariant makes sure ll is equal to its specified value. This is what's described (somewhat more verbosely) by the actual proof obligation below.

The B Method for Programmers (Part 1)

Last month, I had to use Atelier B, an implementation of the B method, for a university assignment. But what is the B method, and what does programming with B look like in practice?

I'm going to introduce B from the perspective of a traditional programmer. You can find documentation on the web, but most of it is from the viewpoint of designing complex state machines. However, B is also a Pascal-like language than can be used for imperative programming. The big added value of using B is that the resulting program can be proven to be correct. In fact, I first encountered B a year ago while working on my B.Sc. thesis, which was about deriving new correct programs from existing ones.

As for its theoretical backgrounds, B is based on the Hoare-Dijkstra model of imperative programming. I'm not going to delve into it; instead, let's look at a concrete example, and I'll guide you through the process of first writing a formal specification, then creating the implementation (this part), and then proving its correctness (in the next part).

Programozás visszavezetéssel

Hát akkor nézzük, mivel is tervezek foglalkozni Fóthi Ákossal a hétfőn kezdődő félév során, progmatos nagyprogramom keretében.

Az alapötlet az, hogy gépi segítséggel bizonyítsunk programozási tételeket , visszavezetés segítségével, és az "ötleteket", az invenciózus lépéseket a felhasználó, ne pedig valamilyen hilbertiánus, féseggű MI-engine találja ki. Tehát a papírt-ceruzát váltanánk csak ki, a hibázás lehetőségét akarjuk csökkenteni és az eredmények menedzselhetőségét növelni.

A "Hello World" szintet például az jelenti majd, ha abból a tételből, hogy ismerjük tetszőleges f:ℤ→ℤ illetve β:ℤ→𝕃 függvények esetén az alábbi feladat (Hoare/Dijkstra/Fóthi értelemben) megoldását...

(egyrészt vegyük észre, hogy természetesen a feltételes maximumkeresésről van szó, másrészt gondolkodjunk el azon, milyen fun lehetett ezt egyenként, Unicode táblázatokat böngészve beírnom)

... be tudjuk látni, hogy akkor meg tudjuk oldani bármilyen, mondjuk g:ℤ→ℤ függvényre az egyszerű minimumkeresést is, vagyis az alábbi feladatot:

Erre egyébként van már annyi szanaszét heverő Lisp kódrészletem, amennyiből valószínűleg össze lehetne kalapálni valamit, ami ennyit már épp majdnem tudna is. Stay tuned.