----------------------------------------------------------------------------- -- | -- Module : Documentation.SBV.Examples.Uninterpreted.Shannon -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- Proves (instances of) Shannon's expansion theorem and other relevant -- facts. See: ----------------------------------------------------------------------------- module Documentation.SBV.Examples.Uninterpreted.Shannon where import Data.SBV ----------------------------------------------------------------------------- -- * Boolean functions ----------------------------------------------------------------------------- -- | A ternary boolean function type Ternary = SBool -> SBool -> SBool -> SBool -- | A binary boolean function type Binary = SBool -> SBool-> SBool ----------------------------------------------------------------------------- -- * Shannon cofactors ----------------------------------------------------------------------------- -- | Positive Shannon cofactor of a boolean function, with -- respect to its first argument pos :: (SBool -> a) -> a pos f = f sTrue -- | Negative Shannon cofactor of a boolean function, with -- respect to its first argument neg :: (SBool -> a) -> a neg f = f sFalse ----------------------------------------------------------------------------- -- * Shannon expansion theorem ----------------------------------------------------------------------------- -- | Shannon's expansion over the first argument of a function. We have: -- -- >>> shannon -- Q.E.D. shannon :: IO ThmResult shannon = prove \$ \x y z -> f x y z .== (x .&& pos f y z .|| sNot x .&& neg f y z) where f :: Ternary f = uninterpret "f" -- | Alternative form of Shannon's expansion over the first argument of a function. We have: -- -- >>> shannon2 -- Q.E.D. shannon2 :: IO ThmResult shannon2 = prove \$ \x y z -> f x y z .== ((x .|| neg f y z) .&& (sNot x .|| pos f y z)) where f :: Ternary f = uninterpret "f" ----------------------------------------------------------------------------- -- * Derivatives ----------------------------------------------------------------------------- -- | Computing the derivative of a boolean function (boolean difference). -- Defined as exclusive-or of Shannon cofactors with respect to that -- variable. derivative :: Ternary -> Binary derivative f y z = pos f y z .<+> neg f y z -- | The no-wiggle theorem: If the derivative of a function with respect to -- a variable is constant False, then that variable does not "wiggle" the -- function; i.e., any changes to it won't affect the result of the function. -- In fact, we have an equivalence: The variable only changes the -- result of the function iff the derivative with respect to it is not False: -- -- >>> noWiggle -- Q.E.D. noWiggle :: IO ThmResult noWiggle = prove \$ \y z -> sNot (f' y z) .<=> pos f y z .== neg f y z where f :: Ternary f = uninterpret "f" f' = derivative f ----------------------------------------------------------------------------- -- * Universal quantification ----------------------------------------------------------------------------- -- | Universal quantification of a boolean function with respect to a variable. -- Simply defined as the conjunction of the Shannon cofactors. universal :: Ternary -> Binary universal f y z = pos f y z .&& neg f y z -- | Show that universal quantification is really meaningful: That is, if the universal -- quantification with respect to a variable is True, then both cofactors are true for -- those arguments. Of course, this is a trivial theorem if you think about it for a -- moment, or you can just let SBV prove it for you: -- -- >>> univOK -- Q.E.D. univOK :: IO ThmResult univOK = prove \$ \y z -> f' y z .=> pos f y z .&& neg f y z where f :: Ternary f = uninterpret "f" f' = universal f ----------------------------------------------------------------------------- -- * Existential quantification ----------------------------------------------------------------------------- -- | Existential quantification of a boolean function with respect to a variable. -- Simply defined as the conjunction of the Shannon cofactors. existential :: Ternary -> Binary existential f y z = pos f y z .|| neg f y z -- | Show that existential quantification is really meaningful: That is, if the existential -- quantification with respect to a variable is True, then one of the cofactors must be true for -- those arguments. Again, this is a trivial theorem if you think about it for a moment, but -- we will just let SBV prove it: -- -- >>> existsOK -- Q.E.D. existsOK :: IO ThmResult existsOK = prove \$ \y z -> f' y z .=> pos f y z .|| neg f y z where f :: Ternary f = uninterpret "f" f' = existential f