Logicomix

Talán egy hónapja hallottam először a Logicomix című képregényről, aztán most valahogy megint előjött Redditen, úgyhogy elolvastam. Szerintem négy dologról szól:

1. Az őrültség (konkrét, orvosi, pszichotikus-skizofrén/neurotikus értelemben) és a formális logika, mint érdeklődési kör korrelációja. A könyv saját magáról állítja, hogy ez a központi kérdése, de szerintem ez a vonal pont nincs annyira nagyon kidolgozva.
2. Bertrand Russel életrajza: ez a "direkt" szint, a könyv alapszerkezetét az adja, hogy Russel maga '39-ben egy előadáson elmeséli életét kisgyerekkorától.
3. Hilbert programja a századfordulóból a matematika axiomatikus megalapozásáról, és annak bukása — bár a könyv nem tudja, vagy nem meri eldönteni, hogy bukásnak értékelje-e a végeredményt. Konkrétan a regény írója és a matematikus szakértő ebben a kérdésben nem jut közös álláspontra — ugyanis a könyv készítői, természetesen, mind-mind szereplői is a képregénynek; milyen is lenne egy könyv Russelről önhivatkozás nélkül...
4. A matematika, a formális logika összeegyeztethetőségének kérdése az emberi lét élményével és tágabban a humanizmussal. Itt először Whitehead/Russel és Wittgenstein van beállítva a két pólusként, de a lezárásra a II. világháború küszöbén tartott előadásában Russel egy frappáns párhuzamot húz Gödel eredményei és az emberiség problémáinak logikai megoldhatósága között.

Egyetlen bánatom a könyvvel, hogy laikusoknak készült, ezért a matematikai tartalma nagyon light-os, és sok helyet elvesz olyan koncepciók vagy akár konkrét tételek elmagyarázása, amiket szerintem a tényleges olvasóközönség úgyis ismer. Viszont az életrajzi adatok, a ki-mikor-kivel-min dolgozott része nagyon érdekes, és nekem a fent negyediknek felsorolt témában érdekes kérdéseket tudott felvetni.

Amiről eddig nem beszéltem, az a könvy vizuális aspektusa. A fekete vonalakkal körberajzolt formákból, halvány színekből álló stílus a klasszikus képregényekre jellemző, a kamera-beállítások és a nagyon jól kidolgozott árnyékolás viszont inkább filmszerűvé teszi a képi világát. Vizuálisan a legerősebbnek az első világháború frontvonalán játszódó Wittgenstein-etűdöt mondanám.

Összességében nyugodt szívvel tudom ajánlani ezt a képregényt a blogom olvasóinak — maga az alapötlet, meglátni a XX. század intellektusainak küzdelmét a matematika és a formális logika látszólag száraz formalizálási törekvései mögött, olyan, ami talán sok unalmas matematika-óra káros hatását tudja kijavítani.

Efficient type-level division for Haskell

Another approach I wanted to explore to Encsé's 9-digit problem was creating a type-level solution in Haskell. First I'll describe what that would entail, and then present a solution to one of its sub-problems: testing special cases of divisibility in a more efficient way than the naïve implementation of repeating subtractions.

Type-level programming

Basically, a type-level Haskell program is to regular Haskell programs what C++ template metaprograms are to C++ proper. Conrad Parker wrote a great introduction to type-level programming using functional dependencies in issue 6 of The Monad.Reader journal, titled Type-Level Instant Insanity. You encode values as types, and then construct an expression whose type, as inferred by the Haskell compiler, encodes the output of your computation. To actually implement the equivalent of a function, typeclasses are used.

For example, take the following (value-level) Haskell definition of length: (deliberately not using any builtin types, and using unary representation for simplicity):

module ValueLength where
        
data Nat = Z | S Nat      
data List a = Nil | a ::: (List a)
infixr 6 :::

length :: List a -> Nat
length Nil = Z
length (x ::: xs) = S (length xs)

(note that due to technical limitations, both : and :: are reserved names in Haskell, and so we have to use ::: for our cons)

To lift this definition to the level of types, we first need a way to represent actual numbers and lists as types. This is pretty straightforward using algebraic datatypes. Since we are ultimately only going to be interested in the type of expressions and not their value, no constructors are defined.

{-# LANGUAGE EmptyDataDecls, TypeOperators,
             FunctionalDependencies,
             MultiParamTypeClasses, UndecidableInstances #-}
module TypeLength where

data Z
data S n

data Nil
data x ::: xs
infixr 6 :::

– Continued below

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).