Feeling ucky

[compilerbitch]

Sore throat, feel hot, tired, fuzzy head, memory not working, sniffly. Bleurgh.

Having nice sleepy day with doseybat here in Cam. First pool practice is in three hours. I really suck at pool these days. Maybe I should go to the SF soc squash instead -- at least I won't have to face being dropped from the 'being geeky and talking about books' team...

doseybat informs me that I am settling in well. People seem to like me on the whole, and I am now pretty much all sorted out as regards the details of getting moving with the PhD. My lingering self-esteem lack tends to make me assume I do the socialising thing worse than people tell me I do. I think I just need injections of self-worth, once-weekly.

I have mostly got a handle on the shape of the maths that is going into the hardware abstract interpretation paper. I'm going to give it all a few more days to sink into my brain, then start writing in about a week, which should still give plenty of time before the abstract deadline. I am going to try to get a first draft of a paper well on the way, if not complete, so I can be pretty sure that abstract makes sense.

For those of you who care about such things, my supervisor suggested using Cousot & Cousot style abstract interpretation as a means of 'selling' the 5-value logic idea. It turns out to have been a really useful insight -- not only does this work, it also makes it possible to define a lattice of similar arithmetics (I'm not using the L-word, because the logicians will whinge incomprehensibly about it). At one extreme, there is a (useless) 1-value logic, then a 3-value arithmetic that resembles intuitionistic logic, then the 5-value arithmetic I mentioned previously. Introducing a nondeterministic choice operator between the 5 values allows a rather neat 16-value version to be defined that can cope with things like F|FT, i.e. a signal that might either stay false forever, or that might at some unspecified point cleanly transition to true. There are only 16 possible values - this follows from a|a = a. This version might be really cool for safe optimisation of asynchronous logic -- it can deal with, for example, the difference between an input that is wired to 1 or 0 for all time, one that switches but that is guaranteed never to glitch (e.g. a clock) and a signal that is genuinely unpredictable, and can potentially be used to help optimise these cases differently. Beyond that, I've been looking at a notation inspired by traces in Hoare's CSP, which generalises all of this very nicely, along with a couple of extensions that can handle synchronisation and both abstract and concrete ideas of time. Alan thinks we can add a further model which is basically just analogue electronics, but I'm not quite sure how to do that yet. I have some ideas, but it will probably fall out from defining the other arithmetics.

Comments

[compilerbitch.livejournal.com]

Intuitionistic logic was an attempt at getting away from the false implies anything = true property of classical Boolean logic. A third 'don't know' state usually written '*' was introduced, so 0 => x = *.

I only touched on it a few years ago, so forgive me for not being able to reel off the references from memory. I'll inevitably have to do some reading on this, so wath this space! There is a turnstile notation based proof system for it that (unsurprisingly!) is rather harder to prove things in than its classical equivalent, but the idea is that you shouldn't be able to accidentally create 'if the moon is made of green cheese, then all fish need bicycles' style invalid proofs.

My 5 value logic adds two extra values to this that capture the idea of clean transitions between states -- the idea was partly inspired by intuitionistic logic.

[trurl.livejournal.com]

Actually I was curious because I know quite a bit about Intuitionistic logic, and didn't know of what you were saying :-)






Intuitionistic logic was an attempt at getting away from the false implies anything = true property of classical Boolean logic.





Actually Intuitionistic logic does allow one to prove anything given false. What it cannot do is prove the excluded middle (A v ~A) or reductio ad absurbdum (~~A => A). This is because it requires a
stronger notion of truth than classical logic. If you have a proof
in Intuitionistic logic, you also have an explicit witness that some statement is true. Consequently, in order to prove A v ~A you would first need to provide some witness for either A being true or ~A being true. Intuitionistic logic has the very appealing property that a proof of a statement is actually isomorphic to a program in the λ-calculus, and formulas are isomorphic to types.





I highly recommend reading http://www-2.cs.cmu.edu/~fp/courses/logic/handouts.html





So I'm still not sure how closely the three value logic you describe relates to my understanding of Intuitionistic logic, but if you can point me to some references I'd certainly be interested in knowing more.

[compilerbitch.livejournal.com]

Hmm... I am possibly misremembering something from a dicrete maths course about 13 years ago. I must admit that the details are a bit hazy now -- it's possible that the 3-value logic might have been something homegrown used as a means of explaining the ideas behind intuitionistic logic, and I may have picked up on that rather than the proof system (which definitely did have the properties you mentioned).

Anyway, if you forgive my previous incorrect use of terminology, the 3-value logic idea goes like this:


/\ 0 1 *
---+---+---+---
0 | 0 | 0 | 0
1 | 0 | 1 | *
* | 0 | * | *

\/ 0 1 *
---+---+---+---
0 | 0 | 1 | *
1 | 1 | 1 | 1
* | * | 1 | *

!
---+---
0 | 1
1 | 0
* | *


which allows 'don't know' or 'unknown' states to be handled easily. This is used quite a lot in the EE world -- most logic synthesis systems can use these * states to generate less logic than would otherwise be required. That's the good news -- the bad news is that logic minimisation based on this logic (or classical logic, for that matter) is only really safe for pure synchronous circuits. Minimisation strategies for more general classes of circuit need to take switching behaviour into account, which is where the 5 and 16 value 'logics' become useful.

Mea culpa.