Skip to content

Stuart A Kurtz / autumn-2020-cmsc-16100-quine

Go to a project
Commit ec64b825 by Stuart Kurtz
Options

Initial commit

parents
Expand all
Inline Side-by-side
Showing with 575 additions and 0 deletions
.gitignore 0 → 100644
dist
dist-newstyle
LICENSE 0 → 100644
This diff is collapsed. Click to expand it.
Makefile 0 → 100644
quine: quine.hs Analyze.hs MonoidMap.hs Proposition.hs
ghc quine
theorems.html: quine theorems.txt
./quine theorems.txt theorems.html
test: theorems.html
open theorems.html
hlint:
hlint *.hs
clean:
rm -rf quine *.{o,hi} theorems.html
Setup.hs 0 → 100644
import Distribution.Simple
main = defaultMain
lecture.html 0 → 100644
<!DOCTYPE HTML>
<html><head><title>Propositional Tautologies</title><script type="text/javascript" src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.2/MathJax.js?config=TeX-MML-AM_CHTML"></script><script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { inlineMath: [['$','$']] }, TeX: { Macros: { limplies: "{\\rightarrow}", ltrue: "{\\top}", lfalse: "{\\bot}", proves: "{\\vdash}"} } });</script><style type="text/css">h1,h2,p.box { color: maroon }</style></head><body><h1>Propositional Tautologies</h1><h2>Proposition 1: ${\alpha}{\;\limplies\;}{\alpha}$</h2><p>Quine Alternatives:</p><ul><li><p>${\alpha}{\;\limplies\;}{\alpha}$ $[{\alpha}:={\ltrue}]$<p>Simplification</p><ul><li>${\ltrue}{\;\limplies\;}{\ltrue}$</li><li>${\ltrue}$</li></ul><p>Reduced to ${\ltrue}$.</p></p></li><li><p>${\alpha}{\;\limplies\;}{\alpha}$ $[{\alpha}:={\lfalse}]$<p>Simplification</p><ul><li>${\lfalse}{\;\limplies\;}{\lfalse}$</li><li>${\ltrue}$</li></ul><p>Reduced to ${\ltrue}$.</p></p></li></ul><p class="box">$\Box$ Proposition 1</p><h2>Proposition 2: ${\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\alpha}$</h2><p>Quine Alternatives:</p><ul><li><p>${\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\alpha}$ $[{\alpha}:={\ltrue}]$<p>Simplification</p><ul><li>${\ltrue}{\;\limplies\;}{\beta}{\;\limplies\;}{\ltrue}$</li><li>${\beta}{\;\limplies\;}{\ltrue}$</li><li>${\ltrue}$</li></ul><p>Reduced to ${\ltrue}$.</p></p></li><li><p>${\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\alpha}$ $[{\alpha}:={\lfalse}]$<p>Simplification</p><ul><li>${\lfalse}{\;\limplies\;}{\beta}{\;\limplies\;}{\lfalse}$</li><li>${\ltrue}$</li></ul><p>Reduced to ${\ltrue}$.</p></p></li></ul><p class="box">$\Box$ Proposition 2</p><h2>Proposition 3: ${\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\gamma}{\;\limplies\;}{\alpha}$</h2><p>Quine Alternatives:</p><ul><li><p>${\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\gamma}{\;\limplies\;}{\alpha}$ $[{\alpha}:={\ltrue}]$<p>Simplification</p><ul><li>${\ltrue}{\;\limplies\;}{\beta}{\;\limplies\;}{\gamma}{\;\limplies\;}{\ltrue}$</li><li>${\beta}{\;\limplies\;}{\gamma}{\;\limplies\;}{\ltrue}$</li><li>${\beta}{\;\limplies\;}{\ltrue}$</li><li>${\ltrue}$</li></ul><p>Reduced to ${\ltrue}$.</p></p></li><li><p>${\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\gamma}{\;\limplies\;}{\alpha}$ $[{\alpha}:={\lfalse}]$<p>Simplification</p><ul><li>${\lfalse}{\;\limplies\;}{\beta}{\;\limplies\;}{\gamma}{\;\limplies\;}{\lfalse}$</li><li>${\ltrue}$</li></ul><p>Reduced to ${\ltrue}$.</p></p></li></ul><p class="box">$\Box$ Proposition 3</p><h2>Proposition 4: ${\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\beta}$</h2><p>Quine Alternatives:</p><ul><li><p>${\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\beta}$ $[{\alpha}:={\ltrue}]$<ul><li>${\ltrue}{\;\limplies\;}{\beta}{\;\limplies\;}{\beta}$</li><li>${\beta}{\;\limplies\;}{\beta}$</li></ul><p>Substitution instance of Proposition 1 $[{\alpha}{\;\limplies\;}{\alpha}]$ at</p><ul><li>${\alpha} := {\beta}$</li></ul></p></li><li><p>${\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\beta}$ $[{\alpha}:={\lfalse}]$<p>Simplification</p><ul><li>${\lfalse}{\;\limplies\;}{\beta}{\;\limplies\;}{\beta}$</li><li>${\ltrue}$</li></ul><p>Reduced to ${\ltrue}$.</p></p></li></ul><p class="box">$\Box$ Proposition 4</p><h2>Proposition 5: ${\alpha}{\;\limplies\;}({\alpha}{\;\limplies\;}{\beta}){\;\limplies\;}{\beta}$</h2><p>Quine Alternatives:</p><ul><li><p>${\alpha}{\;\limplies\;}({\alpha}{\;\limplies\;}{\beta}){\;\limplies\;}{\beta}$ $[{\alpha}:={\ltrue}]$<ul><li>${\ltrue}{\;\limplies\;}({\ltrue}{\;\limplies\;}{\beta}){\;\limplies\;}{\beta}$</li><li>$({\ltrue}{\;\limplies\;}{\beta}){\;\limplies\;}{\beta}$</li><li>${\beta}{\;\limplies\;}{\beta}$</li></ul><p>Substitution instance of Proposition 1 $[{\alpha}{\;\limplies\;}{\alpha}]$ at</p><ul><li>${\alpha} := {\beta}$</li></ul></p></li><li><p>${\alpha}{\;\limplies\;}({\alpha}{\;\limplies\;}{\beta}){\;\limplies\;}{\beta}$ $[{\alpha}:={\lfalse}]$<p>Simplification</p><ul><li>${\lfalse}{\;\limplies\;}({\lfalse}{\;\limplies\;}{\beta}){\;\limplies\;}{\beta}$</li><li>${\ltrue}$</li></ul><p>Reduced to ${\ltrue}$.</p></p></li></ul><p class="box">$\Box$ Proposition 5</p><h2>Proposition 6: ${\alpha}{\,\lor\,}{\beta}{\;\limplies\;}({\alpha}{\;\limplies\;}{\gamma}){\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}$</h2><p>Quine Alternatives:</p><ul><li><p>${\alpha}{\,\lor\,}{\beta}{\;\limplies\;}({\alpha}{\;\limplies\;}{\gamma}){\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}$ $[{\alpha}:={\ltrue}]$<ul><li>${\ltrue}{\,\lor\,}{\beta}{\;\limplies\;}({\ltrue}{\;\limplies\;}{\gamma}){\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}$</li><li>${\ltrue}{\;\limplies\;}{\gamma}{\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}$</li><li>${\gamma}{\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}$</li></ul><p>Substitution instance of Proposition 2 $[{\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\alpha}]$ at</p><ul><li>${\alpha} := {\gamma}$</li><li>${\beta} := {\beta}{\;\limplies\;}{\gamma}$</li></ul></p></li><li><p>${\alpha}{\,\lor\,}{\beta}{\;\limplies\;}({\alpha}{\;\limplies\;}{\gamma}){\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}$ $[{\alpha}:={\lfalse}]$<ul><li>${\lfalse}{\,\lor\,}{\beta}{\;\limplies\;}({\lfalse}{\;\limplies\;}{\gamma}){\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}$</li><li>${\beta}{\;\limplies\;}{\ltrue}{\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}$</li><li>${\beta}{\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}$</li></ul><p>Substitution instance of Proposition 5 $[{\alpha}{\;\limplies\;}({\alpha}{\;\limplies\;}{\beta}){\;\limplies\;}{\beta}]$ at</p><ul><li>${\alpha} := {\beta}$</li><li>${\beta} := {\gamma}$</li></ul></p></li></ul><p class="box">$\Box$ Proposition 6</p><h2>Proposition 7: ${\alpha}{\,\lor\,}{\beta}{\,\lor\,}{\gamma}{\;\limplies\;}({\alpha}{\;\limplies\;}{\delta}){\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$</h2><p>Quine Alternatives:</p><ul><li><p>${\alpha}{\,\lor\,}{\beta}{\,\lor\,}{\gamma}{\;\limplies\;}({\alpha}{\;\limplies\;}{\delta}){\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$ $[{\alpha}:={\ltrue}]$<ul><li>${\ltrue}{\,\lor\,}{\beta}{\,\lor\,}{\gamma}{\;\limplies\;}({\ltrue}{\;\limplies\;}{\delta}){\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$</li><li>${\ltrue}{\,\lor\,}{\gamma}{\;\limplies\;}{\delta}{\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$</li><li>${\ltrue}{\;\limplies\;}{\delta}{\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$</li><li>${\delta}{\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$</li></ul><p>Substitution instance of Proposition 3 $[{\alpha}{\;\limplies\;}{\beta}{\;\limplies\;}{\gamma}{\;\limplies\;}{\alpha}]$ at</p><ul><li>${\alpha} := {\delta}$</li><li>${\beta} := {\beta}{\;\limplies\;}{\delta}$</li><li>${\gamma} := {\gamma}{\;\limplies\;}{\delta}$</li></ul></p></li><li><p>${\alpha}{\,\lor\,}{\beta}{\,\lor\,}{\gamma}{\;\limplies\;}({\alpha}{\;\limplies\;}{\delta}){\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$ $[{\alpha}:={\lfalse}]$<ul><li>${\lfalse}{\,\lor\,}{\beta}{\,\lor\,}{\gamma}{\;\limplies\;}({\lfalse}{\;\limplies\;}{\delta}){\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$</li><li>${\beta}{\,\lor\,}{\gamma}{\;\limplies\;}{\ltrue}{\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$</li><li>${\beta}{\,\lor\,}{\gamma}{\;\limplies\;}({\beta}{\;\limplies\;}{\delta}){\;\limplies\;}({\gamma}{\;\limplies\;}{\delta}){\;\limplies\;}{\delta}$</li></ul><p>Substitution instance of Proposition 6 $[{\alpha}{\,\lor\,}{\beta}{\;\limplies\;}({\alpha}{\;\limplies\;}{\gamma}){\;\limplies\;}({\beta}{\;\limplies\;}{\gamma}){\;\limplies\;}{\gamma}]$ at</p><ul><li>${\alpha} := {\beta}$</li><li>${\beta} := {\gamma}$</li><li>${\gamma} := {\delta}$</li></ul></p></li></ul><p class="box">$\Box$ Proposition 7</p></body></html>
\ No newline at end of file
lecture.txt 0 → 100644
a -> a
a -> b -> a
a -> b -> c -> a
a -> b -> b
a -> (a -> b) -> b
a | b -> (a -> c) -> (b -> c) -> c
a | b | c -> (a -> d) -> (b -> d) -> (c -> d) -> d
quine.cabal 0 → 100644
name: quine
version: 0.1.0.0
synopsis: Quine method prover
-- description:
license: GPL-3
license-file: LICENSE
author: Stuart Kurtz
maintainer: stuart@cs.uchicago.edu
-- copyright:
category: Logic
build-type: Simple
extra-source-files: ChangeLog.md
cabal-version: >=1.10
executable quine
main-is: Main.hs
other-modules: Proposition, Quine, QuineHtml
-- other-extensions:
build-depends: base, blaze-html, containers, mtl
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -Wall
src/Main.hs 0 → 100644
module Main where
import Control.Monad.State ( when, gets, modify, evalState, State )
import Data.Either ( isRight )
import System.Environment ( getArgs, getProgName )
import System.Exit ( ExitCode(ExitFailure), exitWith )
import System.IO ( stderr, hPutStrLn )
import Text.Read ( readMaybe )
import Proposition ( Proposition )
import Quine ( analyze )
import QuineHtml ( ProofObject, renderQuine )
data TraversalState = TraversalState
{ index :: Int -- the index of the next proposition
, tauts :: [(Int,Proposition)] -- processed, indexed tautologies
}
startState :: TraversalState
startState = TraversalState { index = 1, tauts = [] }
inc :: State TraversalState ()
inc = modify $ \st -> st { index = index st + 1 }
nextIndex :: State TraversalState Int
nextIndex = gets index <* inc
processArg
:: String
-> State TraversalState ProofObject
processArg str = do
ix <- nextIndex
case readMaybe str of
Nothing -> pure (ix,Left str)
Just prop -> do
ts <- gets tauts
let analysis = analyze ts prop
when (isRight analysis) $
modify $ \st -> st{ tauts = (ix,prop):ts }
pure (ix, Right (prop,analysis))
usage :: IO ()
usage = do
progname <- getProgName
hPutStrLn stderr $ "usage: " ++ progname ++ " infile outfile"
exitWith $ ExitFailure 255
main :: IO ()
main = do
args <- getArgs
case args of
[infile,outfile] -> do
objects <- lines <$> readFile infile
writeFile outfile
. renderQuine
. flip evalState startState
. traverse processArg
$ objects
_ -> usage
\ No newline at end of file
src/Proposition.hs 0 → 100644
-- | Define the 'Proposition' ADT for propositional boolean expressions,
-- including Show and Read instances, and an abstract evaluator.
module Proposition where
import Data.Char ( isLower )
import Data.Functor.Identity ( Identity(Identity, runIdentity) )
import Text.ParserCombinators.ReadP as ReadP
( ReadP,
(<++),
between,
chainl1,
chainr1,
char,
readP_to_S,
satisfy,
skipSpaces,
string )
-- | An abstract data type for representing boolean propositions.
data Proposition
= Var String
| Boolean Bool
| Not Proposition
| And Proposition Proposition
| Or Proposition Proposition
| Implies Proposition Proposition
deriving Eq
-- | Strings that are used to define the syntactic representation of
-- various propositional operators.
impliesT,andT,orT,notT,trueT,falseT :: String
impliesT = "->"
andT = "&"
orT = "|"
notT = "!"
trueT = "T"
falseT = "F"
-- | A simple parser combinator that associates a string with a meaning
means :: String -> a -> ReadP a
name `means` meaning = skipSpaces *> ReadP.string name *> pure meaning
-- | A "missing" parser combinator for parsing zero or more applications
-- of a prefix operator to value.
prefix :: ReadP a -> ReadP (a -> a) -> ReadP a
prefix p op = result where
result = p <++ (op <*> result)
-- | Modify a parser to expect to read parentheses around its input.
parens :: ReadP a -> ReadP a
parens = between (skipSpaces *> char '(') (skipSpaces *> char ')')
-- | The Read instance for Proposition.
instance Read Proposition where
readsPrec _ = readP_to_S prec0 where
prec0 = chainr1 prec1 (impliesT `means` Implies)
prec1 = chainl1 prec2 (orT `means` Or)
prec2 = chainl1 prec3 (andT `means` And)
prec3 = prefix prec4 (notT `means` Not)
prec4 = parseVar <++ parens prec0 <++ parseBool
parseVar = skipSpaces
*> (Var . (:[]) <$> satisfy isLower)
parseBool = Boolean <$> (trueT `means` True
<++ falseT `means` False)
-- | The Show instance for Proposition
instance Show Proposition where
show = showp (0 :: Int) where
showp _ (Boolean True) = trueT
showp _ (Boolean False) = falseT
showp _ (Var v) = v
showp _ (Not p) = notT ++ showp 3 p
showp i (And s t) =
paren 2 i $ unwords [ showp 2 s, andT, showp 2 t ]
showp i (Or s t) =
paren 1 i $ unwords [ showp 1 s, orT, showp 1 t ]
showp i (Implies s t) =
paren 0 i $ unwords [ showp 1 s, impliesT, showp 0 t]
paren cutoff precedence str
| precedence > cutoff = "(" ++ str ++ ")"
| otherwise = str
-- | An abstract evaluator for Propositions, in which evaluation takes
-- place within an evaluation context.
abstractEval :: (Applicative m)
=> (String -> m b) -- ^ Var
-> (Bool -> m b) -- ^ Boolean
-> (b -> b) -- ^ Not
-> (b -> b -> b) -- ^ And
-> (b -> b -> b) -- ^ Or
-> (b -> b -> b) -- ^ Implies
-> Proposition
-> m b
abstractEval varf boolf notf andf orf impliesf = eval where
eval (Var a) = varf a
eval (Boolean b) = boolf b
eval (Not p) = pure notf <*> eval p
eval (And p q) = pure andf <*> eval p <*> eval q
eval (Or p q) = pure orf <*> eval p <*> eval q
eval (Implies p q) = pure impliesf <*> eval p <*> eval q
-- | An evaluator for Propositions, in which evaluation
-- does not take place within an evaluation context.
simpleEval :: (String -> b) -- ^ Var
-> (Bool -> b) -- ^ Boolean
-> (b -> b) -- ^ Not
-> (b -> b -> b) -- ^ And
-> (b -> b -> b) -- ^ Or
-> (b -> b -> b) -- ^ Implies
-> Proposition
-> b
simpleEval varf boolf notf andf orf impliesf prop
= runIdentity
$ abstractEval (Identity . varf)
(Identity . boolf)
notf andf orf impliesf prop
src/Quine.hs 0 → 100644
module Quine where
import Control.Monad ( guard, msum )
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (fromJust)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Semigroup ( Sum(Sum, getSum) )
import Proposition ( Proposition(..), simpleEval )
data QuineProof
= Split
[Proposition] -- ^ simplifications
String -- ^ variable to split on
QuineProof -- ^ case where split variable is true
QuineProof -- ^ case where split variable is false
| Trivial
[Proposition] -- ^ simplifications
| Reference
[Proposition] -- ^ simplifications
Int -- ^ index of reference tautology
Proposition -- ^ reference tautology
Substitution -- ^ reference map
deriving (Show)
data Refutation = Refutation (Map String Bool)
deriving (Show)
type Analysis = Either Refutation QuineProof
simplify :: Proposition -> Proposition
simplify = simpleEval Var Boolean notf andf orf impliesf where
notf p = case p of
Boolean b -> Boolean (not b)
Not p' -> p' -- eliminate double negations
_ -> Not p
andf p q = case (p,q) of
(Boolean True,_) -> q
(Boolean False,_) -> Boolean False
(_,Boolean True) -> p
(_,Boolean False) -> Boolean False
_ -> And p q
orf p q = case (p,q) of
(Boolean True,_) -> Boolean True
(Boolean False,_) -> q
(_,Boolean True) -> Boolean True
(_,Boolean False) -> p
_ -> Or p q
impliesf p q = case (p,q) of
(Boolean True,_) -> q
(Boolean False,_) -> Boolean True
(_,Boolean True) -> Boolean True
(_,Boolean False) -> Not p
_ -> Implies p q
simplifyInSteps :: Proposition -> [Proposition]
simplifyInSteps = converge step where
converge f = untilFixed . iterate f where
untilFixed (p:qs@(q:_))
| p == q = [p]
| otherwise = p : untilFixed qs
untilFixed _ = error "untilFixed: impossible error"
step prop = case prop of
v@(Var _) -> v
b@(Boolean _) -> b
Not p -> case p of
Boolean b -> Boolean (not b)
Not p' -> p'
_ -> Not $ step p
And p q -> case (p,q) of
(Boolean True,_) -> q
(Boolean False,_) -> Boolean False
(_,Boolean True) -> p
(_,Boolean False) -> Boolean False
_ -> And (step p) (step q)
Or p q -> case (p,q) of
(Boolean True,_) -> Boolean True
(Boolean False,_) -> q
(_,Boolean True) -> Boolean True
(_,Boolean False) -> p
_ -> Or (step p) (step q)
Implies p q -> case (p,q) of
(Boolean True,_) -> q
(Boolean False,_) -> Boolean True
(_,Boolean True) -> Boolean True
(_,Boolean False) -> Not p
_ -> Implies (step p) (step q)
instanceOf :: Proposition -> Proposition -> Maybe Substitution
instanceOf target pattern = case (target,pattern) of
(t, Var v) -> Just $ Map.singleton v t
(Boolean t,Boolean p) -> guard (t == p) >> pure Map.empty
(Not t, Not p) -> instanceOf t p
(And t1 t2, And p1 p2) -> process t1 t2 p1 p2
(Or t1 t2, Or p1 p2) -> process t1 t2 p1 p2
(Implies t1 t2, Implies p1 p2) -> process t1 t2 p1 p2
_ -> Nothing
where
process t1 t2 p1 p2 = do
m1 <- instanceOf t1 p1
m2 <- instanceOf t2 p2
if m1 `Map.intersection` m2 == m2 `Map.intersection` m1
then pure $ Map.union m1 m2
else Nothing
type Substitution = Map String Proposition
substitute :: Substitution -> Proposition -> Proposition
substitute sub = simpleEval varf Boolean Not And Or Implies where
varf v = Map.findWithDefault (Var v) v sub
-- | A Heuristic selects the "attack variable" for a step of
-- Quine's algorithm. A Nothing result is returned if the
-- Proposition has no variables.
type Heuristic = Proposition -> Maybe String
-- | Produce a 'Map' that counts the number of times each item
-- occurs in a container.
counts :: (Foldable f,Ord a) => f a -> Map a Int
counts = fmap getSum . foldMap (`Map.singleton` (Sum 1))
-- | Determine the key for which a map takes on a maximal value.
argMax :: (Ord k, Ord a) => Map k a -> Maybe k
argMax m = fst <$> Map.foldrWithKey maxPair Nothing m where
maxPair k1 a1 b2@(Just (_,a2)) =
if a1 >= a2 then Just (k1,a1) else b2
maxPair k1 a1 Nothing = Just (k1,a1)
variables :: Proposition -> Set String
variables = simpleEval Set.singleton (const Set.empty) id
Set.union Set.union Set.union
heuristicFirst :: Heuristic
heuristicFirst = Set.lookupMin . variables
heuristicMost :: Heuristic
heuristicMost = argMax . counts . variables
analyzeWithHeuristic
:: Heuristic -- variable selection heuristic
-> [(Int,Proposition)] -- list of indexed tautologies
-> Proposition -- the Proposition to analyze
-> Analysis
analyzeWithHeuristic heuristic tautologies = analyze_ Map.empty where
analyze_ :: Map String Bool -> Proposition -> Analysis
analyze_ valuation prop = case last steps of
Boolean True -> pure $ Trivial steps
Boolean False -> Left $ Refutation valuation
prop' -> case findTaut prop' of
Nothing -> do
let var = fromJust $ heuristic prop'
trueBranch <- analyze_ (Map.insert var True valuation)
(setVar prop' var True)
falseBranch <- analyze_ (Map.insert var False valuation)
(setVar prop' var False)
pure $ Split steps var trueBranch falseBranch
Just (i,pat,m) -> return $ Reference steps i pat m
where
steps = simplifyInSteps prop
setVar p a b = substitute (Map.singleton a (Boolean b)) p
findTaut target = msum $ map tryMatch tautologies where
tryMatch (i,pat) = (,,) i pat <$> target `instanceOf` pat
analyze
:: [(Int,Proposition)]
-> Proposition
-> Analysis
analyze = analyzeWithHeuristic heuristicMost
src/QuineHtml.hs 0 → 100644
{-# LANGUAGE OverloadedStrings #-}
module QuineHtml where
import Control.Monad.State ( void, when )
import qualified Data.Map as Map
import Data.Map (Map)
import Text.Blaze.Html
( toHtml, stringValue, Html, ToMarkup(toMarkup), (!) )
import Text.Blaze.Html5
( body,
docTypeHtml,
h1,
h2,
li,
p,
script,
title,
ul )
import Text.Blaze.Html5.Attributes ( class_, src, type_ )
import qualified Text.Blaze.Html5 as H
import Text.Blaze.Html.Renderer.String (renderHtml)
import Proposition ( Proposition(..) )
import Quine ( Analysis, Refutation(..), QuineProof(..) )
type ProofObject = (Int,Either String (Proposition, Analysis))
newtype WrappedProposition = WrappedProposition Proposition
instance ToMarkup WrappedProposition where
toMarkup (WrappedProposition prop) = "$" *> toTeX prop *> "$"
toHtml' :: Proposition -> Html
toHtml' = toHtml . WrappedProposition
toTeX :: Proposition -> Html
toTeX = prec 0 where
prec _ (Boolean bool) = boolDict Map.! bool
prec _ (Var v) = greekDict Map.! v
prec _ (Not prop) = "{\\lnot}" >> prec 3 prop
prec ix(And s t) = paren 2 ix $
prec 2 s >> "{\\,\\land\\,}" >> prec 2 t
prec ix (Or s t) = paren 1 ix $
prec 1 s >> "{\\,\\lor\\,}" >> prec 1 t
prec ix (Implies s t) = paren 0 ix $
prec 1 s >> "{\\;\\limplies\\;}" >> prec 0 t
paren :: Int -> Int -> Html -> Html
paren cutoff prec' markup
| prec' > cutoff = "(" >> markup >> ")"
| otherwise = markup
greekDict :: Map String Html
greekDict = Map.fromList $
[ ("a","{\\alpha}"),("b","{\\beta}"),("c","{\\gamma}")
, ("d","{\\delta}"),("e","{\\epsilon}"),("f","{\\zeta}")
, ("g","{\\eta}"),("h","{\\theta}"), ("i","{\\iota}")
, ("j","{\\kappa}"),("k","{\\lambda}"),("l","{\\mu}")
, ("m","{\\nu}"),("n","{\\xi}"),("o","{\\omicron}")
, ("p","{\\pi}"),("q","{\\rho}"),("r","{\\sigma}"),("s","{\\tau}")
, ("t","{\\upsilon}"),("u","{\\phi}"),("v","{\\chi}")
, ("w","{\\psi}"),("x","{\\omega}")]
boolDict :: Map Bool Html
boolDict = Map.fromList $
[ (True,"{\\ltrue}")
, (False,"{\\lfalse}")
]
renderItem :: ProofObject -> Html
renderItem (ix,item) = case item of
Right (prop,analysis) -> renderAnalysis ix prop analysis
Left str -> renderUnparseable ix str
renderUnparseable :: Int -> String -> Html
renderUnparseable ix str = do
h2 $ "Unparseable " >> toHtml ix >> ": " >> toHtml (show str)
p ! class_ "box" $
"$\\Diamond$ Unparseable " >> toHtml ix
renderAnalysis :: Int -> Proposition -> Analysis -> Html
renderAnalysis ix prop analysis = case analysis of
Right proof -> renderProof ix prop proof
Left refutation -> renderRefutation ix prop refutation
renderProof :: Int -> Proposition -> QuineProof -> Html
renderProof ix prop proof = do
h2 $ "Proposition " >> toHtml ix >> ": " >> toHtml' prop
format proof
p ! class_ "box" $
"$\\Box$ Proposition " >> toHtml ix
where
format prf = case prf of
Split props var trueb falseb -> do
when (length props > 1) $ do
p "Simplification"
ul . void $ traverse (li . toHtml') props
let prop' = last props
p "Quine Alternatives:"
ul $ do
li $ showBranch prop' var True trueb
li $ showBranch prop' var False falseb
Trivial props -> do
p "Simplification"
ul . void $ traverse (li . toHtml') props
p $ "Reduced to " >> toHtml' (Boolean True) >> "."
Reference props citation pattern bindings -> do
ul . void . traverse (li . toHtml') $ props
p $ "Substitution instance of Proposition "
>> toHtml citation
>> " $[" >> toTeX pattern >> "]$ at"
ul . void . flip Map.traverseWithKey bindings
$ \k v -> li $ "$" >> greekDict Map.! k >> " := "
>> toTeX v >> "$"
showBranch prop' var bool branch = p $ do
toHtml' prop' >> " $[" >> greekDict Map.! var >> ":="
>> boolDict Map.! bool >> "]$"
format branch
renderRefutation :: Int -> Proposition -> Refutation -> Html
renderRefutation ix prop (Refutation refutation) = do
h2 $ "Refutable " >> toHtml ix >> ": " >> toHtml' prop
p "Refuting valuation"
ul . void . flip Map.traverseWithKey refutation $ \k v ->
li $ "$" >> greekDict Map.! k >> " := "
>> boolDict Map.! v >> "$"
p $ "Reduced to " >> toHtml' (Boolean False) >> "."
p ! class_ "box" $
"$\\Diamond$ Refutable" >> toHtml ix
renderQuine :: [ProofObject] -> String
renderQuine objects = renderHtml. docTypeHtml $ do
H.head $ do
title "Propositional Tautologies"
script ! type_ "text/javascript"
! src mathjax
$ ""
script ! type_ "text/x-mathjax-config"
$ config
H.style ! type_ "text/css"
$ css
body $ do
h1 "Propositional Tautologies"
void $ traverse renderItem objects
where
mathjax = stringValue $
"https:"
++ "//cdnjs.cloudflare.com/"
++ "ajax/libs/mathjax/2.7.2/MathJax.js?config=TeX-MML-AM_CHTML"
config = do
"MathJax.Hub.Config({"
" tex2jax: {"
" inlineMath: [['$','$']]"
" },"
" TeX: {"
" Macros: {"
" limplies: \"{\\\\rightarrow}\","
" ltrue: \"{\\\\top}\","
" lfalse: \"{\\\\bot}\","
" proves: \"{\\\\vdash}\"}"
" } "
"});"
css = "h1,h2,p.box { color: maroon }"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or sign in to comment