peteg's blog - hacking - isabelle

At last I have completed the submission process for my worker/wrapper corrigendum-ish thing: the JFP emailed me the printing proofs and I have sent them back, all four and a half pages of it. I am told it will be online sometime soon, and in print at some later time.

Finally completed this bit of work, started sometime around December 2007. The Isabelle proofs available here remain a bit rough, but I did manage to find a bug in the original presentation by Andy Gill and Graham Hutton — unwrap must be strict for fusion to be correct. From there it is a short step to a fusion rule that provably works. I've submitted a corrigendum-ish paper to the JFP and we'll see what happens now.

I never post about anything technical I do any more, so instead I'll talk about someone else's stuff. Brian Huffman, HOLCF's last man standing, has a brand new entry in the Archive of Formal Proofs about verifying stream fusion. From a cursory read I thought he had opted for the "correct but GHC can't optimise it" variant floated in the original paper, but it turns out he has modelled the actual implementation. As always his proofs are mystifying in their clarity and succinctness.

Sweet, someone has ported the library to Standard ML.

Incidentally I stumbled upon VeriFun, which looks like it might be interesting, albeit inert. I wonder what their underlying logic is.

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.

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

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.