/usr/share/doc/libghc-sbv-doc/html/Data-SBV-Examples-Uninterpreted-Shannon.html is in libghc-sbv-doc 5.14-1build3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 | <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Data.SBV.Examples.Uninterpreted.Shannon</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script src="file:///usr/share/javascript/mathjax/MathJax.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Data-SBV-Examples-Uninterpreted-Shannon.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">sbv-5.14: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.</p></div><div id="content"><div id="module-header"><table class="info"><tr><th valign="top">Copyright</th><td>(c) Levent Erkok</td></tr><tr><th>License</th><td>BSD3</td></tr><tr><th>Maintainer</th><td>erkokl@gmail.com</td></tr><tr><th>Stability</th><td>experimental</td></tr><tr><th>Safe Haskell</th><td>None</td></tr><tr><th>Language</th><td>Haskell2010</td></tr></table><p class="caption">Data.SBV.Examples.Uninterpreted.Shannon</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Boolean functions</a></li><li><a href="#g:2">Shannon cofactors</a></li><li><a href="#g:3">Shannon expansion theorem</a></li><li><a href="#g:4">Derivatives</a></li><li><a href="#g:5">Universal quantification</a></li><li><a href="#g:6">Existential quantification</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Proves (instances of) Shannon's expansion theorem and other relevant
facts. See: <a href="http://en.wikipedia.org/wiki/Shannon's_expansion">http://en.wikipedia.org/wiki/Shannon's_expansion</a></p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">type</span> <a href="#t:Ternary">Ternary</a> = <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Binary">Binary</a> = <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a></li><li class="src short"><a href="#v:pos">pos</a> :: (<a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> a) -> a</li><li class="src short"><a href="#v:neg">neg</a> :: (<a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> a) -> a</li><li class="src short"><a href="#v:shannon">shannon</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a></li><li class="src short"><a href="#v:shannon2">shannon2</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a></li><li class="src short"><a href="#v:derivative">derivative</a> :: <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Ternary">Ternary</a> -> <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Binary">Binary</a></li><li class="src short"><a href="#v:noWiggle">noWiggle</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a></li><li class="src short"><a href="#v:universal">universal</a> :: <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Ternary">Ternary</a> -> <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Binary">Binary</a></li><li class="src short"><a href="#v:univOK">univOK</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a></li><li class="src short"><a href="#v:existential">existential</a> :: <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Ternary">Ternary</a> -> <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Binary">Binary</a></li><li class="src short"><a href="#v:existsOK">existsOK</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a></li></ul></div><div id="interface"><h1 id="g:1">Boolean functions</h1><div class="top"><p class="src"><span class="keyword">type</span> <a id="t:Ternary" class="def">Ternary</a> = <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#Ternary" class="link">Source</a> <a href="#t:Ternary" class="selflink">#</a></p><div class="doc"><p>A ternary boolean function</p></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a id="t:Binary" class="def">Binary</a> = <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> <a href="Data-SBV-Internals.html#t:SBool">SBool</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#Binary" class="link">Source</a> <a href="#t:Binary" class="selflink">#</a></p><div class="doc"><p>A binary boolean function</p></div></div><h1 id="g:2">Shannon cofactors</h1><div class="top"><p class="src"><a id="v:pos" class="def">pos</a> :: (<a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> a) -> a <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#pos" class="link">Source</a> <a href="#v:pos" class="selflink">#</a></p><div class="doc"><p>Positive Shannon cofactor of a boolean function, with
respect to its first argument</p></div></div><div class="top"><p class="src"><a id="v:neg" class="def">neg</a> :: (<a href="Data-SBV-Internals.html#t:SBool">SBool</a> -> a) -> a <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#neg" class="link">Source</a> <a href="#v:neg" class="selflink">#</a></p><div class="doc"><p>Negative Shannon cofactor of a boolean function, with
respect to its first argument</p></div></div><h1 id="g:3">Shannon expansion theorem</h1><div class="top"><p class="src"><a id="v:shannon" class="def">shannon</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#shannon" class="link">Source</a> <a href="#v:shannon" class="selflink">#</a></p><div class="doc"><p>Shannon's expansion over the first argument of a function. We have:</p><pre class="screen"><code class="prompt">>>> </code><strong class="userinput"><code>shannon
</code></strong>Q.E.D.
</pre></div></div><div class="top"><p class="src"><a id="v:shannon2" class="def">shannon2</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#shannon2" class="link">Source</a> <a href="#v:shannon2" class="selflink">#</a></p><div class="doc"><p>Alternative form of Shannon's expansion over the first argument of a function. We have:</p><pre class="screen"><code class="prompt">>>> </code><strong class="userinput"><code>shannon2
</code></strong>Q.E.D.
</pre></div></div><h1 id="g:4">Derivatives</h1><div class="top"><p class="src"><a id="v:derivative" class="def">derivative</a> :: <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Ternary">Ternary</a> -> <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Binary">Binary</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#derivative" class="link">Source</a> <a href="#v:derivative" class="selflink">#</a></p><div class="doc"><p>Computing the derivative of a boolean function (boolean difference).
Defined as exclusive-or of Shannon cofactors with respect to that
variable.</p></div></div><div class="top"><p class="src"><a id="v:noWiggle" class="def">noWiggle</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#noWiggle" class="link">Source</a> <a href="#v:noWiggle" class="selflink">#</a></p><div class="doc"><p>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:</p><pre class="screen"><code class="prompt">>>> </code><strong class="userinput"><code>noWiggle
</code></strong>Q.E.D.
</pre></div></div><h1 id="g:5">Universal quantification</h1><div class="top"><p class="src"><a id="v:universal" class="def">universal</a> :: <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Ternary">Ternary</a> -> <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Binary">Binary</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#universal" class="link">Source</a> <a href="#v:universal" class="selflink">#</a></p><div class="doc"><p>Universal quantification of a boolean function with respect to a variable.
Simply defined as the conjunction of the Shannon cofactors.</p></div></div><div class="top"><p class="src"><a id="v:univOK" class="def">univOK</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#univOK" class="link">Source</a> <a href="#v:univOK" class="selflink">#</a></p><div class="doc"><p>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:</p><pre class="screen"><code class="prompt">>>> </code><strong class="userinput"><code>univOK
</code></strong>Q.E.D.
</pre></div></div><h1 id="g:6">Existential quantification</h1><div class="top"><p class="src"><a id="v:existential" class="def">existential</a> :: <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Ternary">Ternary</a> -> <a href="Data-SBV-Examples-Uninterpreted-Shannon.html#t:Binary">Binary</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#existential" class="link">Source</a> <a href="#v:existential" class="selflink">#</a></p><div class="doc"><p>Existential quantification of a boolean function with respect to a variable.
Simply defined as the conjunction of the Shannon cofactors.</p></div></div><div class="top"><p class="src"><a id="v:existsOK" class="def">existsOK</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a> <a href="src/Data-SBV-Examples-Uninterpreted-Shannon.html#existsOK" class="link">Source</a> <a href="#v:existsOK" class="selflink">#</a></p><div class="doc"><p>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:</p><pre class="screen"><code class="prompt">>>> </code><strong class="userinput"><code>existsOK
</code></strong>Q.E.D.
</pre></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.17.3</p></div></body></html>
|