sauerlandAlts.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Implementing Sauerland's algorithm using the pointed-set monad"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Syntax\n",
    "\n",
    "In this system, we won't be treating exhaustification as a unary logical operator, but ultimately as a the reflex of a special interpretation rule. As such, the syntax for propositional logic is rather standard, the only difference being the presence of the binary connectives `L` and `R` (following Sauerland 2004)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "newtype Var = Var Char\n",
    "    deriving (Eq, Ord)\n",
    "    \n",
    "data Expr = Variable Var\n",
    "          | Negation Expr\n",
    "          | Conjunction Expr Expr\n",
    "          | Disjunction Expr Expr\n",
    "          | L Expr Expr\n",
    "          | R Expr Expr\n",
    "          deriving Eq\n",
    "          \n",
    "mkVar :: Char -> Expr\n",
    "mkVar = Variable . Var"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here, we define some functions in order to print formulas of propositional logic in a readable fashion."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "instance Show Var where\n",
    "    show (Var v) = [v]\n",
    "\n",
    "showBinaryConnective :: (Expr -> String) -> String -> Expr -> Expr -> String\n",
    "showBinaryConnective show_ symbol exp1 exp2 =\n",
    "  '(' : show_ exp1 ++ \" \" ++ symbol ++ \" \" ++ show_ exp2 ++ \")\"\n",
    "\n",
    "showBC :: String -> Expr -> Expr -> String\n",
    "showBC = showBinaryConnective show\n",
    "          \n",
    "instance Show Expr where\n",
    "  show (Variable      name)      = show name\n",
    "  show (Negation      expr)      = '~' : show expr\n",
    "  show (Conjunction   exp1 exp2) = showBC \"&&\" exp1 exp2\n",
    "  show (Disjunction   exp1 exp2) = showBC \"||\" exp1 exp2\n",
    "  show (L   exp1 exp2) = showBC \"L\" exp1 exp2\n",
    "  show (R   exp1 exp2) = showBC \"R\" exp1 exp2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Computing structural alternatives"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here, we use Chung-chieh Shan's *pointed-set monad* in order to compute structural alternatives in a compositional fashion (definitions taken from [this blog post](http://conway.rutgers.edu/~ccshan/wiki/blog/posts/Pointed_set)). The pointed-set monad is used to model a monadic computation that keeps track of both $a$s and indeterminate $a$s (in this instance, the set of alternatives)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "import Control.Monad (liftM,replicateM,ap)\n",
    "\n",
    "data Pointed a = Pointed a [a]\n",
    "  deriving (Eq, Ord, Show, Read)\n",
    "\n",
    "toList (Pointed x xs) = x:xs\n",
    "\n",
    "instance Functor Pointed where\n",
    "  fmap = liftM\n",
    "\n",
    "instance Applicative Pointed where\n",
    "  pure = return\n",
    "  (<*>) = ap\n",
    "  \n",
    "instance Monad Pointed where\n",
    "  return x = Pointed x []\n",
    "  Pointed x xs >>= k = Pointed y (ys ++ (xs >>= toList.k))\n",
    "    where Pointed y ys = k x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [],
   "source": [
    "binaryConnectives :: [Expr -> Expr -> Expr]\n",
    "binaryConnectives = [Conjunction, Disjunction, L, R]\n",
    "\n",
    "alts :: (Expr -> Expr -> Expr) -> Pointed (Expr -> Expr -> Expr)\n",
    "alts op = Pointed op binaryConnectives"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[((a && b) || c),((a || b) || c),((a L b) || c),((a R b) || c),((a || b) && c),((a && b) && c),((a || b) && c),((a L b) && c),((a R b) && c),((a || b) || c),((a && b) || c),((a || b) || c),((a L b) || c),((a R b) || c),((a || b) L c),((a && b) L c),((a || b) L c),((a L b) L c),((a R b) L c),((a || b) R c),((a && b) R c),((a || b) R c),((a L b) R c),((a R b) R c)]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "getAlts :: Pointed Expr -> [Expr]\n",
    "getAlts (Pointed p alts) = alts\n",
    "\n",
    "disjAlts = getAlts $ alts Disjunction <*> (alts Disjunction <*> pure (mkVar 'a') <*> pure (mkVar 'b')) <*> pure (mkVar 'c')\n",
    "\n",
    "disjAlts"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Below, we compositionally compute the set of alternatives for the formula `a || b || c`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Pointed ((a || b) || c) [((a && b) || c),((a || b) || c),((a L b) || c),((a R b) || c),((a || b) && c),((a && b) && c),((a || b) && c),((a L b) && c),((a R b) && c),((a || b) || c),((a && b) || c),((a || b) || c),((a L b) || c),((a R b) || c),((a || b) L c),((a && b) L c),((a || b) L c),((a L b) L c),((a R b) L c),((a || b) R c),((a && b) R c),((a || b) R c),((a L b) R c),((a R b) R c)]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "alts Disjunction <*> (alts Disjunction <*> pure (mkVar 'a') <*> pure (mkVar 'b')) <*> pure (mkVar 'c')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Semantics\n",
    "\n",
    "Below you can find the basic semantics for propositional logic. The only unusual feature is that `a L b` simply returns the value of `a` relative to the assignment, and `a R b` returns the value of `b` relative to the assignment."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "import Data.Map (Map,fromList,lookup)\n",
    "import Data.List (group,sort)\n",
    "import Data.Maybe (fromMaybe)\n",
    "\n",
    "type Mapping = Map Var Bool\n",
    "\n",
    "variables :: Expr -> [Var]\n",
    "variables expr = let vars_ (Variable      v)     vs = v : vs\n",
    "                     vars_ (Negation      e)     vs = vars_ e vs\n",
    "                     vars_ (Conjunction   e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs\n",
    "                     vars_ (Disjunction   e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs\n",
    "                     vars_ (L   e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs\n",
    "                     vars_ (R   e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs\n",
    "\n",
    "                 in  map head . group . sort $ vars_ expr []\n",
    "                 \n",
    "assignments :: Expr -> [Mapping]\n",
    "assignments expr = let vs = variables expr\n",
    "                       ps = replicateM (length vs) [True, False]\n",
    "                   in  map (fromList . zip vs) ps\n",
    "                   \n",
    "assignments' :: [Var] -> [Mapping]\n",
    "assignments' vs = map (fromList . zip vs) $ replicateM (length vs) [True, False]\n",
    "                   \n",
    "interpret :: Expr -> Mapping -> Bool\n",
    "interpret (Variable      v)         vs = fromMaybe False (lookup v vs)\n",
    "interpret (Negation      expr)      vs = not $ interpret expr vs\n",
    "interpret (Conjunction   exp1 exp2) vs = interpret exp1 vs && interpret exp2 vs\n",
    "interpret (Disjunction   exp1 exp2) vs = interpret exp1 vs || interpret exp2 vs\n",
    "interpret (L   exp1 exp2) vs = interpret exp1 vs\n",
    "interpret (R   exp1 exp2) vs = interpret exp2 vs\n",
    "\n",
    "values :: Expr -> [Bool]\n",
    "values expr = map (interpret expr) (assignments expr)\n",
    "\n",
    "-- | Determines whether an expression is contradictory.\n",
    "isContradiction :: Expr -> Bool\n",
    "isContradiction = not . or . values"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Implementing an exhaustification operator based on minimal worlds"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "proposition :: Expr -> [Mapping] -> [Mapping]\n",
    "proposition expr model = [w | w <- model, interpret expr w]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "entails :: Expr -> Expr -> Bool\n",
    "expr `entails` expr' = all (`elem` proposition expr' (assignments' (variables expr ++ variables expr'))) (proposition expr (assignments' (variables expr ++ variables expr')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 84,
   "metadata": {},
   "outputs": [],
   "source": [
    "isPropersubset :: Eq a => [a] -> [a] -> Bool\n",
    "isPropersubset x y = all (`elem` y) x && x /= y\n",
    "\n",
    "strictPreorder :: [Expr] -> Mapping -> Mapping -> Ordering\n",
    "strictPreorder alts u v\n",
    "    | uAlts `isPropersubset` vAlts = LT\n",
    "    | vAlts `isPropersubset` uAlts = GT\n",
    "    | otherwise = EQ\n",
    "        where uAlts = [p | p <- alts, interpret p u]\n",
    "              vAlts = [q | q <- alts, interpret q v]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 91,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><div class=\"suggestion-name\" style=\"clear:both;\">Move brackets to avoid $</div><div class=\"suggestion-row\" style=\"float: left;\"><div class=\"suggestion-warning\">Found:</div><div class=\"highlight-code\" id=\"haskell\">(disjunctionF <*> (pure $ mkVar 'a')) <*> (pure $ mkVar 'b')</div></div><div class=\"suggestion-row\" style=\"float: left;\"><div class=\"suggestion-warning\">Why Not:</div><div class=\"highlight-code\" id=\"haskell\">(disjunctionF <*> (pure $ mkVar 'a')) <*> pure (mkVar 'b')</div></div><div class=\"suggestion-name\" style=\"clear:both;\">Move brackets to avoid $</div><div class=\"suggestion-row\" style=\"float: left;\"><div class=\"suggestion-warning\">Found:</div><div class=\"highlight-code\" id=\"haskell\">disjunctionF <*> (pure $ mkVar 'a')</div></div><div class=\"suggestion-row\" style=\"float: left;\"><div class=\"suggestion-warning\">Why Not:</div><div class=\"highlight-code\" id=\"haskell\">disjunctionF <*> pure (mkVar 'a')</div></div>"
      ],
      "text/plain": [
       "Line 10: Move brackets to avoid $\n",
       "Found:\n",
       "(disjunctionF <*> (pure $ mkVar 'a')) <*> (pure $ mkVar 'b')\n",
       "Why not:\n",
       "(disjunctionF <*> (pure $ mkVar 'a')) <*> pure (mkVar 'b')Line 10: Move brackets to avoid $\n",
       "Found:\n",
       "disjunctionF <*> (pure $ mkVar 'a')\n",
       "Why not:\n",
       "disjunctionF <*> pure (mkVar 'a')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "[False,True,True,False]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "exhMw :: Pointed Expr -> Mapping -> Bool\n",
    "exhMw (Pointed p alts) w = interpret p w && null [v|v <- assignments p, interpret p v && strictPreorder alts v w == LT]\n",
    "\n",
    "valuesExhMw :: Pointed Expr -> [Bool]\n",
    "valuesExhMw (Pointed p alts) = map (exhMw (Pointed p alts)) (assignments p)\n",
    "\n",
    "disjunctionF :: Pointed (Expr -> Expr -> Expr)\n",
    "disjunctionF = alts Disjunction\n",
    "\n",
    "aAndB = (disjunctionF <*> (pure $ mkVar 'a')) <*> (pure $ mkVar 'b')\n",
    "\n",
    "\n",
    "valuesExhMw aOrB"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Semantics of exhaustification\n",
    "\n",
    "Simple exhaustification of non-weaker alternatives."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [],
   "source": [
    "excl :: Expr -> Expr -> Bool\n",
    "excl s alt = not . isContradiction $ s `Conjunction` Negation alt\n",
    "\n",
    "filterExcl :: Pointed Expr -> Pointed Expr\n",
    "filterExcl (Pointed p alts) = Pointed p (filter (excl p) alts)\n",
    "\n",
    "implicate :: Pointed Expr -> Mapping -> Bool\n",
    "implicate (Pointed p alts) vs = foldr ((&&) . not . (`interpret` vs)) (interpret p vs) alts\n",
    "\n",
    "interpretExh :: Pointed Expr -> Mapping -> Bool\n",
    "interpretExh = implicate . filterExcl\n",
    "\n",
    "valuesExh :: Pointed Expr -> [Bool]\n",
    "valuesExh (Pointed p alts) = map (interpretExh (Pointed p alts)) (assignments p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "metadata": {},
   "outputs": [],
   "source": [
    "aOrB = alts Disjunction <*> pure (mkVar 'a') <*> pure (mkVar 'b')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[False,False,False,False]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "valuesExh aOrB"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Truth-tables"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [],
   "source": [
    "type Printer = (Expr -> String, Bool -> String)\n",
    "\n",
    "-- | The 'truthTable' function produces a truth table for the given expression.\n",
    "truthTable :: Expr -> String\n",
    "truthTable = truthTableP (show, showBool)\n",
    "\n",
    "-- | The 'truthTableP' is a configurable version of 'truthTable' which allows a\n",
    "-- printer function to be selected, so for example one can print ASCII truth\n",
    "-- tables by passing 'showAscii' to 'truthTableP' instead of 'show'.\n",
    "truthTableP :: Printer -> Expr -> String\n",
    "truthTableP (expPrinter, boolPrinter) expr = unlines [header, separator, body]\n",
    "  where\n",
    "    header    = (unwords . map show) vs ++ \" | \" ++ expPrinter expr\n",
    "    body      = init . unlines $ map (showAssignment boolPrinter expr) as\n",
    "    separator = concat $ replicate sepLength \"-\"\n",
    "    sepLength = length vs * 2 + length (expPrinter expr) + 2\n",
    "    as        = assignments expr\n",
    "    vs        = variables   expr\n",
    "    \n",
    "showAssignment :: (Bool -> String) -> Expr -> Mapping -> String\n",
    "showAssignment printer expr a = showVarValues ++ \" | \" ++ showExprValue\n",
    "  where\n",
    "    showVarValues = unwords $ foldr ((:) . printer) [] a\n",
    "    showExprValue = printer $ interpret expr a\n",
    "\n",
    "-- | Prints @T@ for 'True' and @F@ for 'False'.\n",
    "showBool :: Bool -> String\n",
    "showBool True  = \"T\"\n",
    "showBool False = \"F\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "a b | (a || b)\n",
       "--------------\n",
       "T T | T\n",
       "T F | T\n",
       "F T | T\n",
       "F F | F"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "IHaskell.Display.plain $ truthTable $ mkVar 'a' `Disjunction` mkVar 'b'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [],
   "source": [
    "showExh :: Pointed Expr -> String\n",
    "showExh (Pointed p alts) = \"Exh \" ++ show p"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\"Exh ((a || b) || c)\""
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "showExh aOrB"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 95,
   "metadata": {},
   "outputs": [],
   "source": [
    "type PrinterExh = (Pointed Expr -> String, Bool -> String)\n",
    "\n",
    "-- | The 'truthTable' function produces a truth table for the given expression.\n",
    "truthTableExh :: Pointed Expr -> String\n",
    "truthTableExh = truthTablePExh (showExh, showBool)\n",
    "\n",
    "-- | The 'truthTableP' is a configurable version of 'truthTable' which allows a\n",
    "-- printer function to be selected, so for example one can print ASCII truth\n",
    "-- tables by passing 'showAscii' to 'truthTableP' instead of 'show'.\n",
    "truthTablePExh :: PrinterExh -> Pointed Expr -> String\n",
    "truthTablePExh (expPrinter, boolPrinter) (Pointed expr alts) = unlines [header, separator, body]\n",
    "  where\n",
    "    header    = (unwords . map show) vs ++ \" | \" ++ expPrinter (Pointed expr alts)\n",
    "    body      = init . unlines $ map (showAssignment exhMw boolPrinter (Pointed expr alts)) as\n",
    "    separator = concat $ replicate sepLength \"-\"\n",
    "    sepLength = length vs * 2 + length (expPrinter (Pointed expr alts)) + 2\n",
    "    as        = assignments expr\n",
    "    vs        = variables   expr\n",
    "    \n",
    "showAssignment :: (Pointed Expr -> Mapping -> Bool) -> (Bool -> String) -> Pointed Expr -> Mapping -> String\n",
    "showAssignment f printer expr a = showVarValues ++ \" | \" ++ showExprValue\n",
    "  where\n",
    "    showVarValues = unwords $ foldr ((:) . printer) [] a\n",
    "    showExprValue = printer $ f expr a\n",
    "\n",
    "-- | Prints @T@ for 'True' and @F@ for 'False'.\n",
    "showBool :: Bool -> String\n",
    "showBool True  = \"T\"\n",
    "showBool False = \"F\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 96,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "a b | Exh (a || b)\n",
       "------------------\n",
       "T T | F\n",
       "T F | T\n",
       "F T | T\n",
       "F F | F"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "IHaskell.Display.plain $ truthTableExh aOrB"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 108,
   "metadata": {},
   "outputs": [],
   "source": [
    "aOrBandC = mkVar 'a' `Disjunction` (mkVar 'b' `Conjunction` mkVar 'c')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 109,
   "metadata": {},
   "outputs": [],
   "source": [
    "alts' = map Variable $ variables aOrBandC"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 110,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "a b c | Exh (a || (b && c))\n",
       "---------------------------\n",
       "T T T | F\n",
       "T T F | F\n",
       "T F T | F\n",
       "T F F | T\n",
       "F T T | T\n",
       "F T F | F\n",
       "F F T | F\n",
       "F F F | F"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "IHaskell.Display.plain $ truthTableExh (Pointed aOrBandC alts')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 112,
   "metadata": {},
   "outputs": [],
   "source": [
    "-- | Determines whether two expressions are extensionally equivalent (that is,\n",
    "-- have the same values under all interpretations).\n",
    "equivalent :: Expr -> Expr -> Bool\n",
    "equivalent exp1 exp2 = values exp1 == values exp2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 114,
   "metadata": {},
   "outputs": [],
   "source": [
    "getLiteral :: Pointed Expr -> Expr\n",
    "getLiteral (Pointed p alts) = p"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 116,
   "metadata": {},
   "outputs": [],
   "source": [
    "aOrBorCorD = mkVar 'a' `Disjunction` mkVar 'b' `Disjunction` mkVar 'c' `Disjunction` mkVar 'd'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 118,
   "metadata": {},
   "outputs": [],
   "source": [
    "alts'' = map Variable $ variables aOrBorCorD"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 119,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "a b c d | Exh (((a || b) || c) || d)\n",
       "------------------------------------\n",
       "T T T T | F\n",
       "T T T F | F\n",
       "T T F T | F\n",
       "T T F F | F\n",
       "T F T T | F\n",
       "T F T F | F\n",
       "T F F T | F\n",
       "T F F F | T\n",
       "F T T T | F\n",
       "F T T F | F\n",
       "F T F T | F\n",
       "F T F F | T\n",
       "F F T T | F\n",
       "F F T F | T\n",
       "F F F T | T\n",
       "F F F F | F"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "IHaskell.Display.plain $ truthTableExh (Pointed aOrBorCorD alts'')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Checking for closure under some operation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 143,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><div class=\"suggestion-name\" style=\"clear:both;\">Redundant if</div><div class=\"suggestion-row\" style=\"float: left;\"><div class=\"suggestion-warning\">Found:</div><div class=\"highlight-code\" id=\"haskell\">if not (any (\\ z -> z == x `f` y) (x : y : ys)) then False else\n",
       "  undefined</div></div><div class=\"suggestion-row\" style=\"float: left;\"><div class=\"suggestion-warning\">Why Not:</div><div class=\"highlight-code\" id=\"haskell\">not (not (any (\\ z -> z == x `f` y) (x : y : ys))) && undefined</div></div>"
      ],
      "text/plain": [
       "Line 2: Redundant if\n",
       "Found:\n",
       "if not (any (\\ z -> z == x `f` y) (x : y : ys)) then False else\n",
       "  undefined\n",
       "Why not:\n",
       "not (not (any (\\ z -> z == x `f` y) (x : y : ys))) && undefined"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "closed :: Eq a => [a] -> (a -> a -> a) -> Bool\n",
    "closed (x:y:ys) f = if not (any (\\z -> z == x `f` y) (x:y:ys)) then False else undefined\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Haskell - hExh",
   "language": "haskell",
   "name": "ihaskell_hexh"
  },
  "language_info": {
   "codemirror_mode": "ihaskell",
   "file_extension": ".hs",
   "name": "haskell",
   "pygments_lexer": "Haskell",
   "version": "8.4.4"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}