peteg's blog - hacking

The h-tree example, another infinite image.

You can download the standalone file here. Unfortunately I can't seem to get the gzip compression to work, so that file is a little bit huge for what it is. Here's the code:

l :: Picture
l = Canvas 1 1 [Line (0.5, 0.5) (0.5, 1)]
;
h :: Picture
h = Overlay l (Beside 1 1 (Flip s) s)
;
s :: Picture
s = Rotate h
;
htree :: Picture
htree = h
;
main = htree

Here is a friend of the fish cycle: the "fish limit".

Again, if you look at the free standing SVG file, you should be able to exercise the scaling feature of your SVG implementation.

Although the SVG rendering consists of only a finite set of lines, the original FLAN source code describes an infinite set; the interpreter decides to stop generating that set once the lines get too small.

polyline :: [(Num, Num)] -> [Shape]
polyline pts =
  match pts with
      []   -> []
    | p:ps ->
        let mkP :: (Num, Num) -> [(Num, Num)] -> [Shape]
            mkP prev qqs =
              match qqs with
                  []   -> [] -- Don't close the polygon.
                | q:qs -> (Line prev q) : (mkP q qs)
              end ;
         in mkP p ps
  end
;

leftFish :: Picture
leftFish =
    Canvas 1 1
      ((Line (1/8, 3/5) (1, 4/5))
       : (polyline [ (1, 1), (1/8, 3/5), (1, 1/8), (3/4, 0), (1, 0)]))
;

rightFish :: Picture
rightFish = Flip leftFish
;

fish :: Picture
fish = Beside 1 1 leftFish rightFish
;
sideFish :: Picture
sideFish = Rotate fish
;

foodChain :: Picture
foodChain =
  let p :: Picture
      p = Beside 1 1 foodChain sideFish ;
  in Above 1 1 p p
;

main = foodChain

In a previous life I implemented GLog, a declarative graphics engine based on some very old ideas. In this one I've been implementing Peter Henderson's even older Functional Geometry as part of an assignment for JAS. If your browser can render SVG and HCoop's webserver is behaving itself, you should see the dear old "fish cycle" from the paper Logic programming graphics and infinite terms by P. R. Eggert and K. P. Chow.

If you look at the free standing SVG file, you should be able to exercise the scaling feature of the SVG implementation in your browser. The FLAN source code is this:

polyline :: [(Num, Num)] -> [Shape]
polyline pts =
  match pts with
      []   -> []
    | p:ps ->
        let mkP :: (Num, Num) -> [(Num, Num)] -> [Shape]
            mkP prev qqs =
              match qqs with
                  []   -> [] -- Don't close the polygon.
                | q:qs -> (Line prev q) : (mkP q qs)
              end ;
         in mkP p ps
  end
;

leftFish :: Picture
leftFish =
    Canvas 1 1
      ((Line (1/8, 3/5) (1, 4/5))
       : (polyline [ (1, 1), (1/8, 3/5), (1, 1/8)
                   , (3/4, 0), (1, 0)]))
;

rightFish :: Picture
rightFish = Flip leftFish
;

fish :: Picture
fish = Beside 1 1 leftFish rightFish
;

sideFish :: Picture
sideFish = Rotate fish
;

matrix :: [[Picture]] -> Picture
matrix = col
;

col :: [[Picture]] -> Picture
col pps =
  let mkP :: [[Picture]] -> (Picture, Num)
      mkP pps = match pps with
                    []   -> (Empty, 0)
                  | p:ps -> match mkP ps with (pic, n) ->
                              (Above 1 n (row p) pic, n + 1)
                            end
                end ;
  in match mkP pps with (p, n) -> p end
;

row :: [Picture] -> Picture
row pps =
  let mkP :: [Picture] -> (Picture, Num)
      mkP pps = match pps with
                    []   -> (Empty, 0)
                  | p:ps -> match mkP ps with (pic, n) ->
                              (Beside 1 n p pic, n + 1)
                            end
                end ;
  in match mkP pps with (p, n) -> p end
;

main =
  let u :: Picture
      u = fish ;
      l :: Picture
      l = sideFish ;
      d :: Picture
      d = Rotate l ;
      r :: Picture
      r = Rotate d ;
  in matrix [[d, l,     l],
             [d, Empty, u],
             [r, r,     u]]

There is an implementation available in LISP.

I abandoned this attempt at mechanising a proof of the "approx lemma" about eighteen months ago, for what now seem like spurious reasons; what I had was quite close to what was needed. I was initially interested in the "take lemma" made famous by Richard Bird & Philip Wadler, and how it took the magic step from assertions about finite lists to ones about possibly infinite objects. Well, I definitely feel some awareness of vacuity now.

You can read it here.

The magic is how the continuity underpinning the semantics of functions is reflected into the term language. As such it's unbelievably cute. The proof of correctness is not particularly interesting though, except perhaps as an exercise in fiddling with fixpoints and continuity.

It's about time I pushed this out the door. Their proofs went through fine for the most part, except for the need to do some induction when rewriting the recursive calls. It is unclear to me how to prove the lemma that justifies this step in general, though for each instance the induction is quite straightfoward, and the key lemmas for the inductive steps are given in the paper. In effect we need induction just to convince HOLCF, not an optimisation phase, but it would be nice if their fusion rule handled this for me. (My proposed, unproven variant can be found in worker_wrapper.thy.)

I believe there was a small strictness bug in their streams / memoisation example. Score one to HOLCF.

I also tried to mechanise Andy Gill's nub example, which mostly went OK, modulo proving some auxiliary lemmas. Specifically, as above one needs to use induction to rewrite the recursive call, and coming out with the right statements is made difficult by HOLCF's admissibility requirements. A work in progress. Again, I can feel Larry Paulson laughing at me for wasting my time.

You can look at it here, or utter:

darcs get http://peteg.org/isabelle/worker_wrapper/

Note some proofs are quite rough, though most of the important stuff is as clear as Isar. The Nat theory may end up being interesting, though with too much more monadic machinery one may as well use HOL... and I have begun to realise that proof-reuse for even something as simple as lists is quite difficult. There are at least two mainstream types (fully lazy and fully strict), as well as some in-betweens that might be convenient (e.g. head-strict and tail-strict). The code here just begins down the mainstream-Haskell path; I figure the Standard ML people are wise enough to be using HOL or Coq or whatever in the first place.

Tim pointed this almost-book out to me. It's sorely disappointing that whoever-it-was who should've cranked the operational semantics half did not do so; what is there is top-notch, especially the chapters on Information Systems. Whereas Glyn Winskel's text does a great job of presenting the mathematics of these "concretised" domains, this book also delves into the philosophical concerns and hence makes the mathematics that much easier to follow.

It's linked from near the top of his publications page.

It's been a while between drinks with HOLCF, and it didn't take me long to realise why; it's a massive time-sink and all one gets at the end is a proof unreadable by the mainstream and an awareness of vacuity. Here are some random observations that I will try to expand on later:

• Brian Huffman gave me some help with treating unpointed domains, so I've begun cranking out a theory of a few ways to think about Nat. We'll see if that ever gets polished.
• I was mucking about with those while trying to mechanise Andy Gill and Graham Hutton's worker/wrapper pre-paper. That went OK, modulo HOLCF's general unfriendliness towards numbers. I'll post the development when it's a bit more polished.
• John Launchbury and Simon Peyton-Jones's Unboxed values as first class citizens is the most awesome concrete application of domain theory I've seen yet. Perhaps I should dig deeper into the abstract interpretation literature.
• I was curious about Larry Paulson's mechanised verification of the unification algorithm in LCF, from the early 80s. Partial predicates? WTF is this? Larry's inimitable way of politely grinding his teeth made me realise just how much HOL brought to the table.
• I managed to crank out a proof in HOLCF that "parallel or" and its friend "tell me if this function ever says yes" are continuous. So, err, just what is this domain theory modelling anyway? Those proofs were much harder yakka than I expected. Next step: Gordon Plotkin's notes on domains lists some cute sequentiality definitions that I'd like to understand.
• In HOLCF we have (λx. ⊥) = ⊥, and one has to wonder just what that entails, coming from Haskell where it does not obtain.
• Apparently some people are translating Haskell to HOLCF, and I have to wonder what the point is. There's a bit of a semantic gap, so many arbitrary modelling decisions to take, not much of a standard library, ... so there's lots of tedious stuff to do before you can prove your program is incorrect.

I guess I'll have to get back to real (economic) work one of these days.

There are several proofs of this fact, such as this one from 2006. So, why would IBM's DeveloperWorks publish an an article that apparently says otherwise [*]?

Finally, XSLT is the familiar technique that, in a sense, best matches the structure of XML. Perhaps reflecting this match, XSL documents are themselves XML document instances. XSLT is a special-purpose functional programming language that allows you to specify transformations of XML documents into other things (especially, but not only, into other XML documents). Aside from the somewhat annoying verboseness of XSLT, it is limited in its expressiveness — the things you can say are expressed rather clearly (and functionally, not procedurally), but you quickly bump up against all the things that you simply cannot say in XSLT.

OK, so there is an appeal to a Turing tarpit argument, but how about that last phrase, the worrying ... all the things that you simply cannot say in XSLT? Let's keep reading:

The problem comes as soon as you want to filter or compute something for the output — something that is not included in the few comparisons available to XSLT. For example, maybe you want (in a numerological spirit) to display only the even-numbered hexagrams, or only the prime ones. With XSLT, you are out of luck for something this simple.

So, what we have here is something like control completeness — it has enough in the way of control flow constructs — but data-incompleteness — you can't munge your data in all the ways you'd like to. This has always bothered me: how do you prove that you have provided enough operations for your datatype? I'm sure there are people studying algebraic data types and algebraic specification who have some answers for that.

[*] As this article should make clear, the claim of Turing Completeness is weaker and slipperier than most people seem to think.

That's a first, a Mac OS X update that screwed things up so badly the MacBook ceased to function. Oh well, I now know where an Apple store is in Hồ Chí Minh City; I went to:

Thuan My Co. Ltd - Apple Authorised Reseller
98 Nguyễn Công Trứ, District 1, Hồ Chí Minh City.
Tel: 84 8 8218936, 8218937
Fax: 84 8 8218937
Email: thuanmy-sales@hcm.fpt.vn

and tried to buy a copy, nay a licence, of Leopard. I'll spare you that story. The "update" function failed to work any magic (or didn't like the cafés I went to), but the "archive and install" thing did the trick. I get the impression that some database in my old 10.4 installation got trashed.

Here are some fix-ups for Leopard from around the net (sorry for the lack of attribution). Let's fix the Dock (make it look more like Tiger's):

defaults write com.apple.dock no-glass -boolean YES
killall Dock

and the transparent menubar (cut and paste this line, then — eek! — reboot):

sudo defaults write /System/Library/LaunchDaemons/com.apple.WindowServer 'EnvironmentVariables' -dict 'CI_NO_BACKGROUND_IMAGE' 0.63

Time machine claims to have done something but I haven't tried to use it yet. Spaces is clunkier than I'd expect; using an app that sprays windows around like Finder and expecting some kind of mid-90s "raise" functionality is apparently asking too much. The wifi widget on the menubar finally works like what every user of open networks wants it to. Worth the money? Probably not, but heh, anything to get the MacBook back on its feet. That's the last time I travel without a Mac OS X DVD.

I don't know why people hate PayPal; perhaps they were evil in the past. (Actually, reading that website makes me wish Visa et al. got properly into this game.) Anyway, as Vietnam doesn't seem to use phone cards, I wanted to put some cash into Skype so I could call my parents. The payment options are specific to the country where they guess your IP is, and in Vietnam one cannot use PayPal to pay Skype, though PayPal is happy for you to manipulate it from within Vietnam. The only option usable to me — Moneybookers — asks for a mobile phone number in Australia, which may or may not actually need to be valid.

What to do? Well, fortunately the Skype website is accessible, and the server hosting peteg.org is in Australia, so I just used links to punt some cash over. This setup is so stupid — how many ex-pats want to do the same thing? — though I can understand that Skype figures it's better to be safe than useful.

(Thanks André, thanks Adelaide.)

This whole Unicode fiasco has finally killed X11 as a viable option for me. I wouldn't have thought it was so very hard to provide a complete set of easily-usable Unicode fonts, but there it is.

So, on André's advice, I've switched to:

• Aquamacs, GNU Emacs with a shiny-happy Mac OS X face. Apart from a lot of minor irritations that come with losing about a decade's worth of XEmacs configuration, it seems quite slick. I tried Carbon XEmacs but it doesn't support Unicode out of the box, and I refuse to spend (more) hours fiddling with it.

• Terminator, an xterm-alike written in Java, is possibly the best thing ever to run on the JVM.

• A new bash from MacPorts that speaks Unicode better than the crusty old one that comes with Mac OS X 10.4.x.

Of course I'll still need X11 for sundry old-school things like Isabelle, but there the pain is much less.

So, why Aquamacs rather than a fancy closed-source editor? Well, TextMate crashed on me after about twenty minutes of use — I tried to open a file while saving-as another one, and was madly switching programs trying to navigate the directory tree — and so I recall the cardinal rule of editors: anything less than twenty years old hasn't been tested enough. Whether the (relatively shallow) differences that Aquamacs has to GNU Emacs matter is something I will soon discover.

This thing is magic: one can readily write a little script to (in my case) copy images from iPhoto into a Blosxom-friendly location, and output the requisite tags.

The storm this morning brought two things: mrak's much-talked-about postcards, one from Qatar, the other from Vietnam, both posted in the last week of his travels; and a man from TNT Express Worldwide bearing a MacBook.

Apple has a strange way of managing expectations; the Apple Store website told me it was late in shipping, but then the shipping itself took one day instead of two or more. Anyway, they managed to suck me into buying an iPod with a two hundred dollar discount so I guess they've earnt the right to laugh at me.

I spent most of the day trying to reinstall everything, after I asked Migration Assistant to ship all the crap in my home directory over. Surprisingly Isabelle installed with little hassle, and Apple's new(er) X11 works pretty well. I was shocked to find how easy it was to install Debian these days, even under (a trial version of) Parallels.

In short: it's bigger, heavier and much, much faster than the old iBook, and the fan comes on pretty much as soon as you do anything serious. The glossy screen seems to be OK; it's all about getting the angle right, like MySpace. The keyboard is actually quite fine too, despite appearances. No regrets so far.

This application is just plain broken. It wants to be an operating system: from the look of Version 8 Adobe has tried to shoehorn most of the Mac OS X desktop into their proprietary web-browser-of-sorts. Hmm... perhaps this is what the Windows people have been dealing with all these years. unnecessary, unwanted feature-creep and integration.

The updater is broken. Just download the latest version. Oh wait, you need to get the "Download Manager" to download it for you. Grrr. And you sure do a lot of waiting on all these bloody programs... and then it tries to do the update thing anyway! Screw it, too much trouble.

Now, down to business: the instant-gratification eBook I rashly bought yesterday only lets me print 20 pages of it per month, which seems to me to be a strange compromise between the real world (fair use?) and what's possible with electronic authoritarianism. I found this mechanism is indeed easy to defeat.

A moment's reflection tells you that it is common (UNIX) courtesy for an application to only fiddle with stuff in your home directory, which you (of course) have free access to. (It could do nasty things if it's SUID or using OS DRM services, and that's surely in the post.) The hope is that by swapping some files we can reset the print counter, and that is indeed the case. On Mac OS X, simply, if inconveniently:

1. Kill Adobe Reader. I assume you haven't used any of your print quota.
2. Copy your ~/Library/Acrobat User Data somewhere safe. It seems to be a bit sensitive to a few things, so I suggest:

   cd ~/Library
   tar cfv ~/AUD.tar Acrobat\ User\ Data/
   

3. Fire up Adobe reader, print as much as you're allowed to.
4. Kill Adobe Reader, save the new state and extract the old:

   cd ~/Library
   mv Acrobat\ User\ Data/ /tmp/AUD.old
   tar xfv ~/AUD.tar
   

5. Go back to step 3.

If things screw up you can move your saved state back into place and things should work as they did before. The standard disclaimer applies to all of this: it worked for me, I hope it works for you, don't sue me if it doesn't.

I see I'm not the first to think of this.

• Unplugging the headphones makes it pause. Perhaps all iPods do this, but my iRiver didn't.
• The control is much better designed than my old iRiver.

• Some audible warning that it's out of juice. The little all-purpose LED glows red, I think, and that's that.
• A way to delete songs on the player itself, so I can fill it up with random crap and on-the-spot nuke the annoying stuff, rather than having to tediously go through it afterwards in iTunes at home.

• The dinky dock. My old iRiver had a standard mini-USB port, which happened to be the same as my Canon PowerShot A75. One cable was all I needed. Moreover I have no way to recharge it without having the iBook plugged in and running — there's no juice on the USB bus when it's suspended.

I trudged all over Sydney CBD today looking for a new pair of Docs and something that would let me recharge the iBook from the car. It seems the old Docs shop on Pitt St Mall has folded, and the joint down George St that for years proudly advertised cut-price Docs has gone for the factory- (China-) direct brand instead. I'd forgotten what a hassle it is shopping on the street.

Anyway, to cut a long ramble short, I ended up buying a "Powertech Plus Cat. MP-3463 3.5 Amp Universal Step-up DC/DC Converter for Notebook Computer" from Jaycar on York St for $40. The sealed-in cardboard says it was made in China and is distributed by Electus Distribution, and I can guarantee you that the cardboard was printed there too. I can't find it in either of their catalogues. There is also a 6 Amp version for those who have something hefty.

It works, with one small wrinkle: the iBook-sized plug adaptor is wired backwards! Fortunately the iBook is up to that game, simply ignoring a reverse-polarity 24 volts. The solution is to wedge the plug adaptor onto the cable backwards. For the curious these Italians have the details, or you can try to figure out what Apple is on about.