weight-based electrical measurement and other fun stuff

From a paper On the security economics of electricity metering by Ross Anderson and Shailendra Fuloria (via Bruce Schneier's blog), a few of quotes that amused me.

Edison invented a meter consisting of a jar holding two zinc plates: each month the electrodes were weighed and the customer billed according to the change in their weight.

and

For example, customers in Soweto noticed that their meters would set themselves to maximum credit in a brown-out (a voltage reduction to 160-180V) because they had not been tested adequately for African conditions; this only came to light when customers started throwing chains over the 11kV feeders in order to credit their meters.

and (about california):

generators had enough market power to boost peak prices by shutting down some of their plants for “maintenance reasons”. They had learned this trick in 1998 when the replacement reserve price of electricity peaked at $9,999.99/MW in July as against the average of $10/MW for the first three months of the year

A bit later they talk about contract languages, which reminds me very much of recent talk of expressing stock market contracts in Python:

This analysis suggests a technical research project: to design a command language for meters that enables an energy company to specify complex tariffs in a piece of signed downloaded code that would implement a particular contract between the supplier and the customer. The sort of tariff we have in mind is: “Your basic rate is 5p from midnight to 0600, 15p for the peak from 1730 to 2100 and 10p the rest of the time; however the 15p basic peak rate applies only provided you restrict demand to two kilowatts else it becomes 50p. Furthermore we may at any time request you to limit consumption to 1kW and if you don’t then any half-hour segment during which you draw more than 1kW at any time will be charged at 50p”. The code would have to export to the energy company enough data for it to bill the customer correctly, and enough to the distibution company for it to operate the system efficiently. This problem is nontrivial but we believe it is solvable.

branching on the left vs branching on the right (agda bubble sort part 3)

I gave a definition of onepass, the inner loop of my Agda bubblesort implementation, in an earlier post.

That wasn't the first implementation that I tried.

Instead, first I wrote it like this, in a way that uses with expressions. The difference is that the version I wrote uses an if construct that is manually defined. Agda seems to prefer doing case analysis / branching using with, which makes it seem as if you're getting a new parameter to pattern match on - in the below example, the results of y ≤? y which is either yes _ or no _.

onepass : {n : ℕ}→ Vec ℕ n → Vec ℕ n
  onepass {zero} [] = []
  onepass {suc zero} (y :: []) = y :: []
  onepass {suc (suc n)} (y :: (y' :: y0)) with y ≤? y'
  ... | yes _ = y :: (onepass {suc n} (y' :: y0))
  ... | no _ = y' :: (onepass {suc n} (y :: y0))

For comparison, here's the definition in my first post:

onepass {suc (suc n)} (y :: (y' :: y0)) = if y ≤? y' then        
                                        y :: (onepass {suc n} (y' :: y0))     
                                   else y' :: (onepass {suc n} (y :: y0))  

The two implementations do the same thing at runtime - they swap the first two elements of the list and recurse. But their compile-time behaviour is different.

The with-based version doesn't pass the termination checker. The if-based one does.

The with-based version with with the proofs that I gave in part 2. The if based version doesn't.

So I pretty much am forced to choose: I can use the with-based definition, and turn off the termination checker in the Agda compiler. Or not. Either way seems pretty lame. In order to proof all this stuff, I have to turn off the termination checker which is a key part of checking the proofs that I'm writing.

I don't really understand what is going on inside Agda to make the first version not work. But that's what I actually use in practice (with termination checking turned off) - perhaps I can investigate a bit more later. But for now, I want to continue working on a proof (albeit not termination checked) that bubblesort actually sorts...

permutations (bubble sort in agda, pt 2)

(following from part 1)

I implemented bubblesort in Agda, and it looks bug-free. But I want to prove that it is correct. First I want to prove that the output is a permutation of the input. I'm not going to try proving anything about the ordering yet, but I want to know that at least I'm getting back the same list, rearranged.

This is where Agda starts getting really hard for me, and becomes more like stuff I did in my maths degree courses than stuff I've done with hobby computer hacking. Except you can't write "clearly, .... is true" in your Agda programs like you could in your maths homework, so you don't get to bluff your way through proofs quite so easily.

The previous post showed how you could augment the datatypes of the functions in your program to carry more information about how those functions behave. That's one way of using dependent types. In this post, I'm going to use a different style to prove that the output of bubblesort is a permutation.

The Curry-Howard isomorphism which (for the purposes of this post) says (for the purposes of this post) that you can regard propositions as types, and proofs of those propositions as values in those types.

So you define a type to represent whatever proposition it is you want to prove, and then you write a function that creates a value of that type - that value is then a proof of the proposition. When you use values normally, you care what that value is. When you use proofs though, you don't care so much what the proof is. You just care that the proof exists.

First I need to make a definition of what I mean by permutation. There are a few different ways I could have done this. I ended up settling on this one:

data SwapBasedPermutation {A : Set} : {n : ℕ} -> (Vec A n) -> (Vec A n) -> Set where

    reflexivity : {n : ℕ} -> (i : Vec A n) -> SwapBasedPermutation i i

    transitivity : {n : ℕ} -> {a : Vec A n} -> {b : Vec A n} -> {c : Vec A n} -> (SwapBasedPermutation a b) -> (SwapBasedPermutation b c) -> SwapBasedPermutation a c

    prepend : {pn : ℕ} -> {l r : Vec A pn } -> (e : A) -> (SwapBasedPermutation l r) -> SwapBasedPermutation (e :: l) (e :: r)

    swapheads : {pn : ℕ} -> {first second : A} -> {rest : Vec A pn} -> SwapBasedPermutation ( first :: second :: rest ) ( second :: first :: rest)

My permutations are swap-based. Given a list, you can swap the first two elements (using the swapheads constructor, and you get a proof that the first list (but only the first two elements, not some arbitrary pair of elements) is a permutation of the second; and given two lists that are permutations of each other, you can add the same element onto the front of both, and you get a proof that those two new lists will be permutations of each other (using the prepend constructor).

I also declare that permutations are reflexive and transitivitive by definition (although I think I could build those up from more fundamental parts, but I'm more interested in looking at the higher level behaviour of bubblesort).

Those are proofs-by-definition and so they are trivially true (at least as far as the type-checker is concerned).

Now given this SwapBasedPermutation type, I can write a theorem that the top level sortlist function (defined in my previous post) outputs a permutation of its input.

The theorem is a type signature for a function, and body of the function needs to generate a proof of that theorem:

The type signature for my theorem looks like this:

sortlist-permutes : {n : ℕ} -> (l : Vec ℕ n) -> SwapBasedPermutation l (sortlist l)

It says: for all ℕumbers n: for all Vectors l of length n: l is a permutation of sortlist l.

If we can write a definition for this function that typechecks correctly, then this theorem holds. We never actually need to invoke the function at runtime - it is enough to know that we could. (That's another thing thats a bit weird in Agda- you're writing functions that will never be called at runtime but they're still useful. I guess its like writing javadocs...)

Here its important that Agda functions are total - we need to know that our proof generating function really will return a value and not loop forever or error out. Otherwise, our theorem could typecheck but not really be proved.

Now that we've stated the theorem (as a type), we need to build the body (the proof).

To get there, we can define lemmas, in the same way that you can define helper functions to help implement your main function.

First, invoking onepass on a list permutes that list. onepass is the code in my implementation that actually re-orders the list, so the proof of this lemma makes use of the swaphead definition. It also recursively calls itself on a smaller list - that means we're using proof by induction. This definition roughly follows the shape of the definition of onepass itself.

lemma-onepass-permutes : {n : ℕ} -> (l : Vec ℕ n) -> SwapBasedPermutation l (onepass l)
  lemma-onepass-permutes [] = reflexivity []
  lemma-onepass-permutes (e :: []) = reflexivity (e :: [])
  lemma-onepass-permutes (y :: y' :: rest) with  y ≤? y'
  ... | yes _ = prepend y (lemma-onepass-permutes (y' :: rest))
  ... | no _ = let                      
       p1 = lemma-onepass-permutes (y :: rest)                              
       p2 = prepend y' p1
       p3 = swapheads -- magically the list that we're swapping the             
                      -- heads for is inferred (from use in p4)                 
       p4 = transitivity p3 p2
    in p4

Another lemma, this time about the behaviour of innersort:

lemma-innersort-permutes : {vn : ℕ } -> (sn : ℕ) -> (l : Vec ℕ vn) -> SwapBasedPermutation l (innersort sn l)
  lemma-innersort-permutes zero l = reflexivity l
  lemma-innersort-permutes (suc sm) l = let
             a = lemma-onepass-permutes l
                  -- this shows l is a permutation of onepass l                                  
             b = lemma-innersort-permutes sm (onepass l)
                  -- this shows that (onepass l) is a permutation of (innersort sm (onepass l))               
          in transitivity a b

and finally we can give our definition for our theorem, sortlist-permutes, using these lemmas:

sortlist-permutes {n} l = lemma-innersort-permutes  n l

And now, because sortlist-permutes typechecks correctly at compile time, I know that I can generate a proof that sortlist really does permute a list, no matter what list I give it.

Tada!

Except this doesn't actually typecheck in Agda due to a problem with my definition of onepass... see the next post.

bubblesort in agda (part 1)

I've been playing with Agda, a dependently typed programming language (where types of expressions can depend on earlier values).

Dependent types let you make quite rich compile-time assertions about the behaviour of your program. These assertions are written and checked using the type system.

One of the examples for Agda seems to be quicksort. So, I thought I'd experiment with bubblesort - similar but different.

First I want an implementation of bubblesort in Agda. Then I want to use dependent types to express something interesting that I cannot express in another language: that bubblesort really sorts.

Agda looks syntactically quite like Haskell, so I first made a Haskell implementation. This doesn't look like a procedural normal bubblesort implementation, as I wanted to keep a functional style.

bubblesort t = applyLoop t

applyLoop t = if isSorted t then t else applyLoop (onePass t)

onePass [e] = [e]
onePass t =
  let a:b:rest = t
      (as,bs) = if a < b then (a,b) else (b,a)
      newlist = as:bs:rest  -- list with head two elements in order
      bsrest = onePass (bs:rest)
      endlist = as:bsrest
    in endlist

Next I wanted to convert the above Haskell code into Agda. Syntactically, this translates quite easily.

My only major stumbling block comes with termination.

Functions in Agda must be total.

That means they must always terminate with a value. They can't fail with an error, and they can't run forever (which means that Agda is not a turing-complete language, I think!)

Agda contains a termination checker that gives a compile error if it can't prove that your functions terminate.

Bubblesort does always terminate. But the Agda compiler can't see that from the above definition. The proof looks something like: every iteration of applyLoop makes the list more sorted, and once you've called it enough times (as many as there are elements in the list) then the list will be sorted.

So I changed my implementation to run the outer loop a fixed number of times, rather than until the list is sorted. That makes the termination provable. But it makes it less obvious that the final result is actually sorted: now we end after a certain number of runs, rather than when the isSorted test is true...

Here's the Agda code:

onepass : {n : ℕ}→ Vec ℕ n → Vec ℕ n
  onepass {zero} [] = []
  onepass {suc zero} (y :: []) = y :: []
  onepass {suc (suc n)} (y :: (y' :: y0)) = if y ≤? y' then                   
                                        y :: (onepass {suc n} (y' :: y0))     
                                   else y' :: (onepass {suc n} (y :: y0)) 

  innersort : {n : ℕ} -> ℕ -> Vec ℕ n -> Vec ℕ n
  innersort zero list = list
  innersort (suc i) sorted = innersort i (onepass sorted)

  sortlist : {n : ℕ} -> Vec ℕ n -> Vec ℕ n
  sortlist {n} l = innersort n l

(I actually started with a different definition of onepass - I'll come back to that in a different post).

Now, that's enough (given wrappers for main, etc) to successfully sort a list:

$ ./run
2 :: 3 :: 5 :: 8 :: 11 :: 12 :: 14 :: []

So what's different from doing this in Haskell?

Well, on the downside, it is not as obvious that this sort actually returns a sorted list, as mentioned above.

On the upside: we know that this program won't loop forever (although it might loop for a very long time) - because of the termination checker.

And the types of the functions, which I haven't mentioned yet, tell us something that relates the inputs and the outputs. sortlist has a type that tells us that its output will be the same length as its input. This is not a full definition of sortedness but its more than is offered by Haskell lists.

The type signature looks like this:

sortlist : {n : ℕ} -> Vec ℕ n -> Vec ℕ n

which says something like: sortlist is defined for every natural number n, and takes as input a Vector (of ℕumbers) of length n and returns as output a Vector (of ℕumbers) of that same length n.

The type checker checks that this is true at compile time, so the inner functions must have the length similarly encoded in their types.

At compile time, when we call n, we don't know what the n will be for every invocation (this is not Pascal statically-sized arrays) - but we do know that the output will be the same size as the input.

Compare that to type of the Haskell implementation:

bubblesort :: [Int] -> [Int]

which says that bubblesort takes a list of numbers and returns a list of numbers. Typewise, a perfectly valid implementation of quicksort here could return the empty list [] for every input. This can't happen here.

So in subsequent posts, I want to try to make compile-time assertions richer. I want to prove that bubblesort really sorts, by which I mean (I think):the output is a permutation of the input; and the output is in order.

(note 1) actually the Haskell type is: bubblesort :: (Ord t) => [t] -> [t] meaning Lists of anything that can be ordered, rather than lists of integers. That same abstraction is mostly achievable in Agda, but not quite - it doesn't have typeclasses in the same way that Haskell does.

Read part 2...

autoconf and portable programs: the joke

This is not my rant, but I like it:

I have a simple request for you: each time you run into software that does
this idiotic kind of test, please interact with the idiots upstream for
whom all the world is linux, and try to get them to replace their "joke"
of an autoconf macro with actual genuine tests that actually CHECK FOR THE
FUCKING FEATURE.

http://marc.info/?l=openbsd-ports&m=126805847322995&w=2

chess rankings for photos

I have a lot of photos - around 50000. I want to have some kind of scoring system for them.

The obvious one is something like a 5-star scale: when presented with a photo, you can award it from 0 to 5 stars, with 5 being best and 0 being worst.

But thats not very granular, and it is not clear to me that clearly defined standards for the 6 different scores will emerge.

I preferred something that says "this is better than that, so this should have a higher score than that".

But I don't want to have to manually make a strict linear order of all photos (despite the fact that a numerical score would do so), and I want the system to tolerate inconsistencies (eg. A>B, B>C, C>A) somehow.

Eventually I read about chess ranking, where each player is assigned a numerical score indicating their "goodness" and the scores are adjusted by pairwise comparisons between players - chess matches.

I adapted this for scoring my photographs. I started with the glicko system and modified it some.

The way this works is:

Photos compete against each other, as chess players compete against each other. The equivalent of a chess match is a presentation of two photos alongside each other in a web browser, with the user clicking on the photo they prefer. So, users do not assign an absolute score to a photo. Nor do they pick how much better one photo is than the other. They pick have a simple choice: "a>b" or "b>a".

Each photo is assumed to have a single numeric score, such that the difference in the score reflects the probability that one photo will win over the other photo. (this is affine: 900 vs 1000 is the same probability as 4000 vs 4100)

It is assumed that the score cannot be known exactly, but is approximated by a normal distribution (so there is a mean, and a standard deviation).

Adding a comparison between two photos gives information about the distributions for both photos causing the mean and standard deviation to be changed to more accurately reflect the score, as described in the glicko paper.

For my 50000 photos from the past 5 years, I have about 20% voted on at least once.

For a recent trip to rome, where I took about 1000 photos, it took a few hours to include each photo in at least one vote, where each comparison was an unvoted photo vs a random photo (which may or may not have been previously voted). This does not give a huge amount of information per photo.
Once that was done, I spent some hours making other votes: sometimes random vs random, sometimes random vs the photo with the closest mean. This caused rankings to become somewhat refined (sometimes causing surprisingly large changes in mean score)

So here are the top 3 photos from that trip:



and here are the bottom 3:



It seems to work reasonably well, though I think I need many more votes to get more accuracy. But that will come over time: as new photos are added, they'll get their scores by being compared against old photos, which will give more information about the old photos too.