Cracked the proof...
May. 24th, 2004 02:29 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
compilerbitch10 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.
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.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
(no subject)
Date: 2004-05-23 10:49 pm (UTC)(no subject)
Date: 2004-05-24 03:38 am (UTC)Bouncing around the room at 2am wasn't enough, so I had to post to LJ!
(no subject)
Date: 2004-05-24 05:29 am (UTC)i just hadn't a clue what your on about
I'll get you to explain it to me sometime
(no subject)
Date: 2004-05-24 12:18 am (UTC)(no subject)
Date: 2004-05-24 03:39 am (UTC)(no subject)
Date: 2004-05-24 02:33 pm (UTC)I've been having trouble enough with the easier logic problems today though, so I have admiration. :)
(no subject)
Date: 2004-05-24 02:35 pm (UTC)Your own is always more endearing than someone else's. But it still screams its lungs out and throws up all over you at every available opportunity.