![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Feeling ucky
Oct. 12th, 2003 05:49 pmSore throat, feel hot, tired, fuzzy head, memory not working, sniffly. Bleurgh.
Having nice sleepy day with![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
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.
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.