Some notes about the 5-value logic idea

[compilerbitch]

... are here, in the unlikely event that anyone's interested. It's still at-best quarter-baked, I still need to figure out how to handle feedback properly. But it does get the idea across anyway.

Comments

[doseybat.livejournal.com]

i think ill open it at school tomorrow and pretend to be engrossed in it when the head of department goes past *evyl grin*

its a scary thing to have done in an afternoon, i shudder to imagine the size of your thesis!! *trembles slightly* *warmhugs*

[grimgrim.livejournal.com]

Makes sense to me. Do you have cause to use the temporal logic operators? I have only dimly-remembered knowledge of them; geometric-looking affairs for 'assert X at some future time,' 'assert X at all times' and all that.

[compilerbitch.livejournal.com]

Now you're dredging up the old memories! I did a little ccs back during my master's degree, in 1990 I think.

The 5-value logic isn't really a temporal logic. That's why I called it a 'transitional' logic. It kind-of deals with time, but in a sanitised, munged down kind of way. It says things like, well, if this particular signal goes from true to false at some point, then this other signal will change state, again at some unspecified point. It might be interesting trying to unify the two approaches, but I don't intend to hold my breath over managing to make it work! ;-)

I've been playing around on paper with the idea that it should be possible to add an extra construct (I'm calling it a mu-expression for vaguely remembered historical reasons) that syntactically looks a bit like a lambda expression, e.g.: (please forgive the LaTeX!)

\mu x . \neg (r \vee \neg (s \vee x))

which is actually a way of defining an SR latch in the transitional logic. I've also been able to define all the other major classes of latch, including arbiters and Muller C elements, so it does seem to be powerful enough. The idea is to figure out what the algebraic laws for mu expressions should be -- clearly there are going to be some that can be relied upon. It should keep me busy for a while, if nothing else, but the handy thing is that if this approach works, it makes it possible to formalise the semantics of mixed asynchronous/synchronous logic in such a way as to allow a safe axiom of replacement to be defined, which in turn will allow various kinds of optimisation strategy (including of course PE, which is my main motivation for doing this) to be proved correct (or otherwise!).