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.
Andy Gill & Graham Hutton's Worker/Wrapper in HOLCF, finally.Mon, Jul 27, 2009./hacking/isabelle | Link
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.
Incidentally I stumbled upon VeriFun, which looks like it might be interesting, albeit inert. I wonder what their underlying logic is.
Some of Jeremy Gibbons & Graham Hutton's Proof Methods for Corecursive Programs in HOLCF.Mon, Mar 03, 2008./hacking/isabelle | Link
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.
Andy Gill & Graham Hutton's Worker/Wrapper in HOLCF, partially.Sun, Mar 02, 2008./hacking/isabelle | Link
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
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.