complete.hs

module Complete where

import Data.List (transpose, intercalate)

{-

Neste código, a tabela verdade

p0 p1 ... pn
0  0  ... 0  | X0 |
1  0  ... 0  | X1 |
0  1  ...    | X2 |
      ...
1  1  ... 1  | Xn |

É representada como TruthTable [X0, X1, X2, ..., Xn].

Por exemplo:

λ> TruthTable [True, False, False, True]
p0 p1
0 0 | 1
1 0 | 0
0 1 | 0
1 1 | 1

Veja que o Haskell aprendeu a exibir a tabela uma forma bonitinha
(através de uma instância customizada da typeclass Show)

A função disjunctiveNormalForm recebe uma tabela verdade e retorna uma
fórmula equivalente à ela na forma normal conjuntiva

λ> disjunctiveNormalForm (TruthTable [True, False, False, True])
((¬p0 /\ ¬p1) \/ (p0 /\ p1))

Este código é bem mais complexo do que deveria.

Antes de tudo, ele precisa preencher a parte esquerda da tabela
verdade. A função truthTableColumn cria uma coluna dessa tabela. A
coluna é idealizada com tamanho infinito, então só podemos mostrar uma
parte dela. Pegando os 4 primeiros valores de duas colunas:

λ> take 4 (truthTableColumn 0)
[False,True,False,True]
λ> take 4 (truthTableColumn 1)
[False,False,True,True]

A parte esquerda da tabela é dada pela função leftTruthTable, que
recebe como parâmetro o número de átomos. Cada linha dela pode ser
entendida como uma cláusula conjuntiva, digamos, a linha [False,
False] corresponde à fórmula (¬p1 /\ ¬p2), ou p1 é falso e p2 é falso.

λ> leftTruthTable 2
[[False,False],[True,False],[False,True],[True,True]]

A tabela verdade completa é construída por expandTruthTable. Cada
linha dessa tabela expandida é um par ordenado (a, b) onde a é uma
linha da tabela da esquerda e b é o valor da direita. Por exemplo:

λ> expandTruthTable (TruthTable [True, False, False, True])
[([False,False],True),([True,False],False),([False,True],False),([True,True],True)]

Nota: perceba que isto mostra a mesma tabela que o primeiro exemplo,
só que de outro jeito (menos bonitinho). Internamente, ao exibir um
TruthTable, a instância do Show usa a função expandTruthTable.

Perceba outra coisa. Quando se dá uma TruthTable maior, ele "advinha"
que a tabela deve ser maior:

λ> TruthTable [True, False, True, True, True, False, True, True]
p0 p1 p2
0 0 0 | 1
1 0 0 | 0
0 1 0 | 1
1 1 0 | 1
0 0 1 | 1
1 0 1 | 0
0 1 1 | 1
1 1 1 | 1

Ele faz isso chamando a função numAtoms:

λ> numAtoms (TruthTable [True, False, True, True, True, False, True, True])
3

Que nos diz que temos 3 átomos (no caso p0, p1 e p2)

Okay. Uma fórmula ou é um átomo, ou uma negação, ou uma conjunção ou
uma disjunção. O Haskell também exibe fórmulas de forma bonitinha:

λ> Atom 1
p1

λ> And (Or (Not (Atom 1)) (Atom 2)) (Atom 6)
((¬p1 \/ p2) /\ p6)

Átomos são representados internamente como um número inteiro, chamado
aqui de PropVar.

A função literal recebe um PropVar e um Bool e constrói um literal, ou
seja, um átomo ou negação de um átomo:

λ> literal 2 True
p2

λ> literal 0 False
¬p0

A função rowToClause nos mostra a cláusula correspondente à
determinada linha da tabela da esquerda

λ> rowToClause [False, False]
¬p0 /\ ¬p1

λ> rowToClause [True, True, False, True]
(p0 /\ (p1 /\ (¬p2 /\ p3)))

A função disjunctiveNormalForm constrói a tabela verdade expandida
(com a parte esquerda) e coleta em validRows as linhas que representam
cláusulas verdadeiras (possuem valor 1 na tabela). Daí depois pega as
cláusulas correspondentes a cada uma dessas linhas em validClauses e
faz as conjunções delas.

Ou se não tem nenhuma, coloca uma fórmula absurda, que é falsa em
todas as linhas.

-}

type PropVar = Int

data Formula =
  Atom PropVar
  | Not Formula
  | And Formula Formula
  | Or Formula Formula

instance Show Formula where
  show (Atom symbol) = "p" ++ show symbol
  show (Not formula) = "¬" ++ show formula
  show (And f1 f2) = concat ["(", show f1, " /\\ ", show f2, ")"]
  show (Or f1 f2) = concat ["(", show f1, " \\/ ", show f2, ")"]

newtype TruthTable = TruthTable [Bool]

instance Show TruthTable where
  show table =
    concat [intercalate " " (map show atomsList),
            "\n",
            concat (map showLine linesTable)]
    where
      showLine :: ([Bool], Bool) -> String
      showLine (clause, value) =
        concat [intercalate " " (map showTruthValue clause),
                 " | ",
                 showTruthValue value,
                 "\n"]

      showTruthValue :: Bool -> String
      showTruthValue True = "1"
      showTruthValue False = "0"

      atomsList :: [Formula]
      atomsList = map Atom [0 .. numAtoms table - 1]

      linesTable :: [([Bool], Bool)]
      linesTable = expandTruthTable table

literal :: PropVar -> Bool -> Formula
literal atomNumber True = Atom atomNumber
literal atomNumber False = Not (Atom atomNumber)


-- raises exception if the length of truthValues isn't a power of 2
numAtoms (TruthTable truthValues) =
  if not (isInt result) then
     error "Truth table size not a power of 2"
  else
      round result
  where
    isInt :: Float -> Bool
    isInt x = x == fromIntegral (round x)

    result :: Float
    result = logBase 2 (fromIntegral (length truthValues))

truthTableColumn :: PropVar -> [Bool]
truthTableColumn n = cycle (zeroes ++ ones)
  where
    zeroes :: [Bool]
    zeroes = replicate (2^n) False
    ones :: [Bool]
    ones = replicate (2^n) True

leftTruthTable :: Int -> [[Bool]]
leftTruthTable size = transpose (map
                                 (take (2^size) . truthTableColumn)
                                 [0 .. size-1])

expandTruthTable :: TruthTable -> [([Bool], Bool)]
expandTruthTable table@(TruthTable truthValues) =
  zip (leftTruthTable (numAtoms table)) truthValues

-- raises exception on empty row
rowToClause :: [Bool] -> Formula
rowToClause row =
  case folded of
    Nothing -> error "Empty row"
    Just formula -> formula
  where
    folded :: Maybe Formula
    folded = foldr acc Nothing (zip [0, 1 ..] row)

    acc :: (PropVar, Bool) -> Maybe Formula -> Maybe Formula
    acc (n, value) Nothing = Just (literal n value)
    acc (n, value) (Just previous) = Just (And (literal n value) previous)

disjunctiveNormalForm :: TruthTable -> Formula
disjunctiveNormalForm table =
  maybe falsum id (foldr acc Nothing validClauses)
  where
    falsum :: Formula
    falsum = And (Atom 0) (Not (Atom 0))

    acc :: Formula -> Maybe Formula -> Maybe Formula
    acc clause Nothing = Just clause
    acc clause (Just previous) = Just (Or clause previous)

    validClauses :: [Formula]
    validClauses = map rowToClause validRows

    validRows :: [[Bool]]
    validRows = [fst x | x <- expandedTable, clauseValue x]

    clauseValue :: ([Bool], Bool) -> Bool
    clauseValue = snd

    expandedTable :: [([Bool], Bool)]
    expandedTable = expandTruthTable table