There are several important semirings in CS, which miss out on being rings simply because there is no negation. Some examples include the theory of combinatorial species (which describes datastructures), the Kleene Algebra describing regular expressions aka regular grammars aka finite state machines, and both Boolean and Heyting lattices. The last two have a lot of applications- obviously Boolean algebra is important in CS. Heyting lattices are a generalization of Boolean lattices which have some implication structure not necessarily satisfying the usual a -> b = -a\/b. Negation in this context is defined as -a = a -> _|_, so "not a" is the same as "a implies bottom". These are important in denotational semantics and Domain theory.
Negation is also interesting in constructive mathematics, where there is no double negation elimination. Double negation is something like "potentially false" apparently.
The translation of statements from classical logic into intuisionistic logic by double negation corresponds to a translation into CPS (continuation passing style) which is pretty amazing. This only occurs when the _|_ type is replaced with some other type, giving the type of continuations (a -> r) -> r, which is related to the Yoneda Lemma in a way that I am having trouble understanding.
Double negation also has something to say about the concept of proof irrelevance. A term of a type is a proof of the proposition that its type corresponds to. On the other hand, which the actual term is important from a computational perceptive (as it is an algorithm) it is irrelevant from a proof perspective because we are interested in the existence of a proof, not its particulars. The double negation actually removes the computational content from a proof in a very interesting way. In (a -> _|_) -> _|_, if "a" is inhabited then (a -> _|_) is not, as there is no function from an inhabited set to an empty one. If (a -> _|_) is equal to _|_ then (_|_ -> _|_) is inhabited, as there is one function from the empty set to the empty set. This means that the type (a -> _|_) -> _|_, proves a if true, but has lost the particular term that proves a, losing the computational context. I wonder if this is related to the difference between Prop and Set in Coq when doing program extraction to other languages..
There is probably more to say, but for now thats all I can think of.
No comments:
Post a Comment