Cracked the proof...

10 past 2 in the morning. After a long day fighting with troublesome maths, I now have what looks like a solid proof that my Galois connection really is a Galois connection. The proof is in two halves -- the first bit was actually quite easy, just very simple symbol pushing. The second part was harder, but I managed to nail it eventually.

The basic idea is that if f is an abstraction function and g is a concretisation function, f(g(x)) = x, but g(f(x)) may be a superset of x. (I'm using a slightly stricter definition of Galois connection than normal, but that's not a problem). To prove you have a for-real Galois connection, you have to prove that those relations hold. I did the first bit, following an example Alan showed me, just with symbol pushing and the raw definitions of f and g. The second bit was harder. Simple symol pushing wasn't enough, so I ended up messing about with equivalence classes in the concrete domain, which let me rewrite the definitions a bit, making it possible to complete the second half of the proof.

(If this doesn't sound that tricky, I should probably point out that the concrete domain is nondeterministic functions from real (dense, infinite) time to the Booleans, and the abstract domain is a trace semantics generated by collapsing out time.)

I have to prove soundness for functions on both domains next. This bit may be harder.

Sorry for not making it to the V&A meet-up today. I really *did* have to do the maths, and I now feel *so* much happier now that the main proof is sorted out.

I'm giving a seminar on Friday...

Subject: Hardware Partial Evaluation - CPRG meeting
Speaker: Sarah Thompson (CPRG)
Title: Bit-Level Partial Evaluation of Synchronous Circuits

Date: Fri 28 May
Time: 3-4pm
Place: FC22, WGB

Abstract:

Partial evaluation has been known for some time to be very effective when applied to software; in this paper we demonstrate that it is also of significant benefit when applied to hardware.

We present a bit-level algorithm that supports the partial evaluation of synchronous digital circuits. Full PE of combinational logic is noted to be equivalent to Boolean minimisation. A loop unrolling technique, supporting both partial and full unrolling, is described. Experimental results are given, showing that partial evaluation of a simple microprocessor against a ROM image is equivalent to compiling the ROM program directly into low level hardware.


Any cam-types with a vague interest of seeing me bounce up and down in front of a whiteboard are cordially invited...

Filmgoing...

I want to go and see a film in Cam one night this week. Any takers? I'm open to suggestions about choice of film and venue.