⏴ Matrix CombinatorsLisp ⏵
Contents

Pet Theories

Gotta prove 'em all!

[Compiling...]

Deduced again (naturally)

Combinatory logic is to Hilbert systems as lambda calculus is to natural deduction.

Hilbert systems apply tautologies to one another to produce more tautologies. This is clumsy, so logicians devised natural deduction, where we can focus on one part of a deduction just as lambda calculus allow us to cordon off parts of a program in the body of a lambda abstraction.

I built the above game to teach myself natural deduction from Jean-Yves Girard, Proofs and Types. See also:

The existential elimination rule in Girard’s notes are surprisingly simple. Other sources describe substituting a unique constant term for the quantified variable (skolemizing) to start off the side deduction, and ensuring the conclusion reached from this hypothesis contains no occurrences of this placeholder term.

Girard mentions no such substitution, and merely requires that the quantified variable \(\xi\) is no longer free in the hypotheses or the conclusion. I’m unsure why others present a more complex rule, as they seem equivalent: when the existential is dropped, occurrences of the variable \(\xi\) that were bound become free. Unless the hypothesis is discharged in the side deduction, we are unable to bind \(\xi\) with a universal quantifier, which seems to be the only hazard.

Playing the game feels eerily like programming due to the Curry-Howard correspondence. For example, a common manoeuvre is to introduce an implication with zero discharges, then immediately eliminate the implication, so the result is two live hypotheses \(x, y\) leading to the conclusion \(x\). In other words, it’s a bizarre roundabout way of writing Haskell’s const function.

Curry-Howard also helps us understand why natural deduction is in fact awkward in practice. For example, in Haskell, given a function with type, say:

(t -> Int) -> Int -> (Int -> u -> Int)

we can write a function with type:

(t -> Char) -> Char -> (Char -> u -> Char)

by judicious insertions of ord and chr. It’s a slog, yet undeservedly so: we can easily convert Int to Char and back, so why is it so much trouble to convert the code?

Analogously, with natural deduction, given the hypotheses \(x \Rightarrow y\) and its converse, one does not simply replace each \(x\) with a \(y\) in a deduction. Instead, we have to break down a formula, replace the occurrences piecemeal, then stitch it all up again. Just like traversing an abstract syntax tree to add ord and chr.

Friendlier theorem provers like HOL Light have equational reasoning built into their rules.

Classical Versus Intuitionistic Logic

Our game explores more than one type of logic, though in all of them, we represent falsehood with ⊥ and treat ¬a as syntax sugar for a⇒⊥. Other logics define ¬ to be a primitive logical operator.

This scheme makes proof easier to express than refutation, when we are perhaps better off giving the two concepts equal status. But we’ll tolerate this asymmetry for now.

The Law of Excluded Middle (LEM), or tertium non datur, and equivalent to proof by contradiction, or reductio ad absurdum. In our game the LEM rule captures the principle of double negation:

\[ ((a\Rightarrow \bot)\Rightarrow \bot) \Rightarrow a \]

LEM is the hallmark of classical logic. Some levels limit the player to introduction and elimination rules for implication, and the Law of Excluded Middle. Along with a false proposition, these yield all of classical propositional logic: implicational propositional calculus.

However, the LEM rule may be too strong. In particular, the corresponding types make no sense for programming languages based on lambda calculus. For instance, if f is a function that takes an integer but is buggy then LEM is sort of claiming we can feed f to another buggy function to somehow cancel out the bugs and magically produce an integer! On the other hand, LEM makes sense in lambda-mu calculus.

Removing LEM entirely yields minimal logic, which as the name suggests, has limited use. Better to replace LEM with the weaker ⊥-elimination rule, which embodies the principle of explosion or ex falso quodlibet:

\[ \bot \Rightarrow a \]

This leads to intuitionistic logic. We cannot show a∨¬a, but we can get close with ¬¬(a∨¬a).

Must See

The game features famous landmarks of logic.

Terms and Formulas

We start with a data type to represent logical formulas, along with routines for printing and parsing them.

data Term = Term String [Term] deriving Eq
instance Show Term where
  showsPrec _ (Term fun args) = (fun++) . case args of
    [] -> id
    _ -> showParen True $ foldr (.) id $ intersperse (", "++) $ shows <$> args
data Expr = Expr :-> Expr | Expr :& Expr | Expr :+ Expr
  | Predicate String [Term] | Bot | Top
  | Forall String Expr | Exists String Expr deriving Eq

instance Show Expr where
  showsPrec p = \case
    Bot -> ("⊥"++)
    Top -> ("⊤"++)
    Predicate fun args -> (fun++) . case args of
      [] -> id
      _ -> showParen True $ foldr (.) id $ intersperse (", "++) $ shows <$> args
    x :-> y -> showParen (p > 1) $ showsPrec 2 x . ("⇒"++) . showsPrec 1 y
    x :+  y -> showParen (p > 2) $ showsPrec 2 x . ("∨"++) . showsPrec 2 y
    x :&  y -> showsPrec 3 x . ("∧"++) . showsPrec 3 y
    Forall x t -> showParen (p > 0) $ ("∀"++) . (x++) . ('.':) . shows t
    Exists x t -> showParen (p > 0) $ ("∃"++) . (x++) . ('.':) . shows t
jsEval "curl_module('../compiler/Charser.ob')"
import Charser
chainl1 p op = foldl (\x (f, y) -> f x y) <$> p <*> (many $ (,) <$> op <*> p)
chainr1 p op = go id where
  go d = do
    x <- p
    (op >>= \f -> go (d . (f x:))) <|> pure (foldr ($) x $ d [])

isVar (h:_) = 'a' <= h && h <= 'z'

formula :: Charser Expr
formula = space *> expr <* eof where
  expr = atm `chainl1` and' `chainl1` or' `chainr1` imp
  var = (:) <$> lowerChar <*> many alphaNumChar
  atm = spch '(' *> expr <* spch ')'
    <|> spch '0' *> pure Bot
    <|> spch '1' *> pure Top
    <|> spch '#' *> (Predicate "" . (:[]) <$> term)
    <|> Forall <$> (spch '\\' *> var <* spch '.') <*> expr
    <|> Exists <$> (spch '_' *> var <* spch '.') <*> expr
    <|> pred
  args = spch '(' *> sepBy term (spch ',') <* spch ')' <|> pure []
  term = do
    s <- (:) <$> letterChar <*> many alphaNumChar
    space
    if isVar s then pure $ Term s [] else Term s <$> args
  pred = do
    h <- letterChar
    t <- many alphaNumChar
    space
    Predicate (h:t) <$> args
  imp = sp (string "->" <|> string "=>") *> pure (:->)
  and' = sp (string "&" <|> string "*") *> pure (:&)
  or' = sp (string "|" <|> string "+") *> pure (:+)
  sp :: Charser a -> Charser a
  sp = (<* space)
  spch = sp . char

mustFormula :: String -> Expr
mustFormula = either undefined id . parse formula ""
mustFormula "a->b"

Deductions

As with lambda expressions, natural deductions almost have a tree structure. In lambda calculus, we must keep track of where variables are bound. The Curry-Howard equivalent in natural deduction is keeping track of when hypotheses are discharged.

I chose SVG for this game. I thought it might be easiest to associate a translation transform with each parent node of the tree, because once child nodes are combined via some rule, there’s no need to move them independently. But then I realized I need to know the absolute position of each node so I can figure out what a mouse click is selecting.

I settled on a strange design with one level of nesting: each Deduction contains its bounding box in absolute terms, and every Spot contains its box in coordinates relative to the Deduction containing it. Thus transforming a Deduction automatically moves all its Spots, and chasing mouse clicks only requires one adjustment, at the cost of requiring every Spot in a Deduction be retranslated every time a rule its root Deduction moves.

It seems I’m maintaining an SVG elements that mirrors the tree structure of each deduction, while enjoying few of the benefits. In retrospect I might have been better off defining onclick callbacks for each node to avoid computing translations. I suppose part of me wanted to manipulate coordinates for some reason.

I forget the source of our version of the Law of Excluded Middle. It seems a more popular incarnation is to step from \((a → \perp) → \perp\) to \(a\).

data Tree a = Node { rootLabel :: a, subForest :: [Tree a] } deriving (Show,Eq)
instance Functor Tree where
  fmap f (Node a xs) = Node (f a) (fmap f <$> xs)

type Forest a = [Tree a]
data Pos a = Loc
  { _content   :: Tree a
  , _before    :: Forest a
  , _after     :: Forest a
  , _parents   :: [(Forest a, a, Forest a)]
  } deriving (Show,Eq)

data Spot = Spot
  { _id :: String
  , _xywh :: [Int]
  , _expr :: Expr
  } deriving Show

data Deduction = Deduction
  { _did :: String
  , _dim :: [Int]
  , _tree :: Tree Spot
  } deriving Show

data Game = Game
  { _deds :: [Deduction]
  , _goal :: Expr
  , _level :: Int
  , _click :: Int -> Int -> IO ()
  , _sym :: Int
  , _live :: [String]
  , _animcb :: IO ()
  }
minVB = 100
vgap = 10
hgap = 8
cellHeight = 18
hf = (`div` 2)

utf8length = \case
  [] -> 0
  c:rest
    | n >= 128, n < 192 -> utf8length rest
    | otherwise -> succ $ utf8length rest
    where n = ord c

hafwid s = hf (11 * utf8length (show s)) + 3
initSpots = go 0 0 where
  go x idx = \case
    [] -> []
    expr:rest -> dedu : go (x + w + hgap) (succ idx) rest
      where
      hw = hafwid expr
      w = 2*hw
      sp = Spot { _id = "spot" ++ show idx, _xywh = [0, 0, w, cellHeight], _expr = expr }
      dedu = Deduction ("dedu" ++ show idx) [x, 0, w, cellHeight] (Node sp [])
svgSpot (Spot idAttr [x, y, w, h] expr) = concat
  [ "<g id='", idAttr, "' transform='translate"
  , show (x, y), "'> <rect width='", show w, "' height='", show h
  , "' fill='none' stroke='black' stroke-width='2' x='0' y='0' rx='4' ry='4'></rect>"
  , "<text x='", show $ hf w, "' y='9' text-anchor='middle' alignment-baseline='central'>"
  , show expr
  , "</text></g>"
  ]

drawDedu (Deduction did [x, y, w, h] t) = do
  jsEval_ $ concat
    [ "soil.innerHTML += `<g id='", did, "' transform='translate"
    , show (x,y), "'>"
    , svgSpot $ rootLabel t
    , "</g>`;"
    ]

redden (Deduction did _ _) = jsEval_ $ concat ["redden(", did, ");"]

blurb s = jsEval_ $ "blurb(`" ++ s ++ "`);"

select (Node sp _) = let
  [_, _, w, h] = _xywh sp
  in jsEval_ $ concat ["pick(", _id sp, ", ", show w, ", ", show h, ");"]
examine (Node sp ks, (_, dedu, _)) = do
  lives <- _live <$> global
  blurb $ intercalate ", " $ concat
    [ [(if _id sp `elem` lives then "live" else "dead") ++ " hypothesis" | null ks]
    , ["conclusion" | _id sp == _id (rootLabel $ _tree dedu)]
    ]
  getAny \r@(node@(Node sp' _), _) -> do
    untool
    unless (_id sp == _id sp') do
      select node
      examine r

untool = do
  getAny examine
  jsEval_ "untool();"

seek f dedu = go $ _tree dedu where
  go node@(Node v ks) = case f dedu v of
    Just _ -> Just node
    Nothing -> asum $ go <$> ks

zFind f xs = go [] xs where
  go bef aft = case aft of
    [] -> Nothing
    a:at -> case f a of
      Nothing -> go (a:bef) at
      Just r -> Just (r, (bef, a, at))

click x y = do
  f <- _click <$> global
  f x y

someSpot sps xRaw yRaw = zFind (seek hit) sps where
  hit dedu spot
    | x >= x0 && y >= y0 && x <= x0 + w && y <= y0 + h = Just ()
    | otherwise = Nothing
    where
    [x0, y0, w, h] = _xywh spot
    [xd, yd, _, _] = _dim dedu
    x = xRaw - xd
    y = yRaw - yd

getAny f = do
  g <- global
  setGlobal g { _click = anySpot f }

anySpot f xRaw yRaw = do
  g <- global
  maybe untool go $ someSpot (_deds g) xRaw yRaw
  where
  go r@(node, _) = do
    select node
    f r

shove xdelta dedu@(Deduction did (xd:rest@(yd:_)) t) = do
  jsEval $ concat [did, ".setAttribute('transform', 'translate", show (xd', yd), "');"]
  pure $ Deduction did (xd':rest) t
  where
  xd' = xd + xdelta

animGrow x dx = jsEval_ $ concat [ "animGrow(", show x, ", ", show dx, ");" ]

animX xdelta dedu@(Deduction did (xd:rest@(yd:_)) t) = do
  jsEval $ concat [ "animTr(", did, ", ", show xd, ", ", show xdelta, ", ", show yd, ");" ]
  pure $ Deduction did (xd+xdelta:rest) t
genSym = do
  g <- global
  setGlobal g { _sym = succ $ _sym g }
  pure $ _sym g

animThen f = do
  jsEval_ "animStart();"
  g <- global
  setGlobal g { _animcb = f }

animDone = do
  g <- global
  _animcb g
checkGoal dedu = do
  g <- global
  let
    t = _tree dedu
    live (Node sp ks) = case ks of
      [] -> _id sp `elem` _live g
      _ -> or $ live <$> ks
  when (_expr (rootLabel t) == _goal g && not (live t)) $ jsEval_ "qed();"

findIds f (Node sp ks) = case ks of
  [] | f sp -> [_id sp]
     | otherwise -> []
  _ -> findIds f =<< ks

discharge hypo dedu = do
  g <- global
  let
    liveMatches = findIds (\sp -> _expr sp == hypo && _id sp `elem` _live g) $ _tree dedu
  mapM_ (\s -> jsEval_ $ "unredden(`" ++ s ++ "`);") liveMatches
  setGlobal g { _live = _live g \\ liveMatches }

getConc f = getAny \x@(Node sp _, (_, dedu, _)) -> \cases
  | _id sp == _id (rootLabel $ _tree dedu) -> f x
  | otherwise -> oops $ "want conclusion"

getLive f = getAny \x@(Node sp _, (_, dedu, _)) -> do
  lives <- _live <$> global
  if _id sp `elem` lives then f x else oops $ "want live hypothesis"

implies = do
  blurb "pick live hypothesis"
  getLive \(node, ctx@(_, dedu, _)) -> do
    let hypo = _expr $ rootLabel node
    discharge hypo dedu
    implies' hypo ctx

impliesZ = do
  blurb "pick any antecedent"
  getAny \(lhs, _) -> do
    blurb "pick consequent conclusion"
    getConc \(rhs, ctx) -> implies' (_expr $ rootLabel lhs) ctx

implies' ante ctx@(_, dedu, _) = deduce (ante :-> _expr (rootLabel $ _tree dedu)) ctx

translateTree dx dy = go where
  go (Node sp ks) = do
    jsEval_ $ concat
      [_id sp, ".setAttribute('transform', 'translate", show (x', y'), "');"]
    Node sp { _xywh = x':y':rest } <$> mapM go ks
    where
    x:y:rest = _xywh sp
    x' = x + dx
    y' = y + dy

untrans x0 y0 (Deduction _ (x:y:_) t) = translateTree (x - x0) (y - y0) t

deduce conc (bef, dedu, aft) = do
  let
    [xLast, _, wLast, _] = _dim $ last (dedu:aft)
    origW = wLast + xLast
    t = _tree dedu
    [xd, yd, wd, hd] = _dim dedu
    [_, y, _, _] = _xywh $ rootLabel t
    hw = hafwid conc
    xtra = max 0 $ hw - hf wd
  sym <- genSym
  t <- translateTree xtra 0 t
  let
    sp = Spot ("spot" ++ show sym) [max 0 $ hf wd - hw, y + cellHeight + vgap, 2*hw, cellHeight] conc
    dedu' = dedu { _dim = [xd - xtra, yd, wd + 2*xtra, hd + cellHeight + vgap], _tree = t }
  aft <- mapM (animX $ 2*xtra) aft
  dedu' <- animX xtra dedu'
  dedu' <- pure $ dedu' { _tree = Node sp [_tree dedu'] }
  g <- global
  setGlobal g { _deds = reverse bef ++ (dedu' : aft) }

  let
    srcW = max minVB origW
    tgtW = max minVB $ origW + 2*xtra
  when (tgtW > srcW) $ animGrow srcW $ tgtW - srcW

  animThen do
    jsEval_ $ concat
      [ _did dedu, ".innerHTML+=`", svgSpot sp, "`;"
      , _id sp, ".innerHTML+=`"
      , "<rect fill='grey' width='1' height='", show vgap, "' x='", show hw, "' y='", show $ -vgap,"'></rect>"
      , "`;"
      , "fadeIn(", _id sp, ");"
      , "borderOut(", _id $ rootLabel t, ");"
      ]
    jsEval_ "unleashUnreddens();"
    animThen $ checkGoal dedu'
    untool

merge u ks = do
  sym <- genSym
  let
    [xa, y, wa, _] = _dim $ head ks
    [xd, _, wd, _] = _dim $ last ks
    hmax = foldr1 max $ (!!3) . _dim <$> ks
    hw = hafwid u
    sp = Spot ("spot" ++ show sym) [hf w - hw, hmax + vgap, 2*hw, cellHeight] u
    w = xd - xa + wd
    x = xa
    h = hmax + vgap + cellHeight
    did = "dedu" ++ show sym
    newKid k = do
      jsEval_ $ concat [did, ".append(...", _did k, ".childNodes);"]
      jsEval_ $ concat [_did k, ".remove();"]
      let
        [xk,yk,wk,hk] = _xywh $ rootLabel $ _tree k
        idKid = _id $ rootLabel $ _tree k
      jsEval_ $ concat
        [ idKid, ".innerHTML+=`"
        , "<rect fill='grey' width='1' height='"
        , show $ (_xywh sp!!1) - yk - cellHeight - hf vgap
        , "' x='", show $ hf wk, "' y='", show cellHeight,"'></rect>"
        , "`;"
        , "borderOut(", idKid, ");"
        ]
  jsEval_ $ concat
    [ "soil.innerHTML += `<g id='", did, "' transform='translate"
    , show (x,y), "'>"
    , svgSpot sp
    , "</g>`;"
    , "fadeIn(", _id sp, ");"
    ]
  let
    xL = hf wa - _xywh sp!!0
    l2r = w - hf (wa + wd) + 1

  jsEval_ $ concat [ _id sp, ".innerHTML+=`"
    , "<rect fill='grey' width='1' height='", show $ hf vgap, "' x='", show $ hf (_xywh sp!!2), "' y='", show  -(hf vgap), "'></rect>"
    , "<rect fill='grey' width='", show l2r, "' height='1' x='", show xL, "' y='", show -(hf vgap), "'></rect>"
    , "`;"
    ]
  mapM_ newKid ks
  Deduction did [x,y,w,h] . Node sp <$> mapM (untrans x y) ks

deduceMulti u ds (bef, dedu, aft) = do
  let
    [xLast, _, wLast, _] = _dim $ last (dedu:aft)
    origW = wLast + xLast
    offsets f w = \case
      [] -> (w, f [])
      d@(Deduction did dim _):rest
        | elem did (_did <$> ds) -> offsets f w rest
        | otherwise -> offsets (f . ((w - dim!!0, d):)) (w + dim!!2 + hgap) rest

    offsets' f w = \case
      [] -> (w, f [])
      d@(Deduction did dim _):rest -> offsets' (f . ((w - dim!!0, d):)) (w + dim!!2 + hgap) rest

    anim (w, as) = (w,) <$> mapM (uncurry animX) as

  (w, bef) <- anim $ offsets id 0 $ reverse bef
  (w, mids) <- anim $ offsets' id w $ ds ++ [dedu]
  (w, aft) <- anim $ offsets id w aft
  let
    srcW = max minVB origW
    tgtW = max minVB $ w - hgap
  when (tgtW > srcW) $ animGrow srcW $ tgtW - srcW

  animThen do
    conc <- merge u mids
    jsEval_ "unleashUnreddens();"
    animThen do
      g <- global
      setGlobal g { _deds = bef ++ (conc : aft) }
    untool

oops s = do
  untool
  blurb $ "oops: " ++ s

unor = do
  lives <- _live <$> global
  blurb "pick X&or;Y conclusion"
  getConc \(orNode, (_, d0, _)) -> case _expr $ rootLabel orNode of
    x :+ y -> do
      blurb "pick first live hypothesis"
      getLive \case
        (node1, (_, d1, _))
          | x == _expr (rootLabel node1) -> do
            blurb "pick second live hypothesis"
            getLive \case
              (node2, ctx@(_, d2, _))
                | y == _expr (rootLabel node2) -> if c == c'
                  then do
                    discharge x d1
                    discharge y d2
                    deduceMulti c [d0, d1] ctx
                  else oops $ concat ["mismatch: ", show c, " vs. ", show c']
                | otherwise -> oops $ concat ["want ", show y, ", got ", show $ _expr (rootLabel node2)]
                where
                c = _expr $ rootLabel $ _tree d1
                c' = _expr $ rootLabel $ _tree d2
          | otherwise -> oops $ concat ["want ", show x, ", got ", show $ _expr (rootLabel node1)]
    _ -> oops "want X&or;Y"

or1 = do
  blurb "pick conclusion"
  getConc \(lhs, ctx) -> do
    blurb "pick any formula"
    getAny \(rhs, _) -> do
      deduce (_expr (rootLabel lhs) :+ _expr (rootLabel rhs)) ctx

or2 = do
  blurb "pick any formula"
  getAny \(lhs, _) -> do
    blurb "pick conclusion"
    getConc \(rhs, ctx) -> do
      deduce (_expr (rootLabel lhs) :+ _expr (rootLabel rhs)) ctx

forAll = do
  blurb "pick a variable"
  getAny \r@(node@(Node sp _), _) -> case _expr sp of
    Predicate "" [Term s []] | isVar s -> do
      blurb "pick a conclusion"
      getConc \(rhs, ctx) -> do
        -- TODO: Free variable check.
        deduce (Forall s $ _expr $ rootLabel rhs) ctx
    _ -> oops "want variable"

unforAll = do
  blurb "pick a term"
  getAny \r@(node@(Node sp _), _) -> case _expr sp of
    Predicate "" [term] -> do
      blurb "pick a &forall; conclusion"
      getConc \(rhs, ctx) -> case _expr $ rootLabel rhs of
        Forall x body -> deduce (beta term x body) ctx
        _ -> oops "want &forall;"
    _ -> oops "want term"

-- TODO: Avoid variable capture.
beta term x = go where
  go = \case
    a :-> b -> go a :-> go b
    a :& b -> go a :& go b
    a :+ b -> go a :+ go b
    Forall v body
      | v == x -> Forall v body
      | otherwise -> Forall v $ go body
    Exists v body
      | v == x -> Exists v body
      | otherwise -> Exists v $ go body
    Predicate fun args -> Predicate fun $ termSub <$> args
    t -> t
  termSub (Term fun args)
    | fun == x, null args = term
    | otherwise = Term fun $ termSub <$> args

andIntro = do
  blurb "pick first conclusion"
  getConc \(lhs, (_, d1, _)) -> do
    blurb "pick second conclusion"
    getConc \(rhs, ctx) -> do
      deduceMulti (_expr (rootLabel lhs) :& _expr (rootLabel rhs)) [d1] ctx

unand1 = do
  blurb "pick X&and;Y conclusion"
  getConc \(node, ctx@(_, dedu, _)) -> do
    case _expr (rootLabel node) of
      x :& _ -> deduce x ctx
      otherwise -> oops "want X&and;Y"

unand2 = do
  blurb "pick X&and;Y conclusion"
  getConc \(node, ctx@(_, dedu, _)) -> do
    untool
    case _expr (rootLabel node) of
      _ :& x -> deduce x ctx
      otherwise -> oops "want X&and;Y"

unimplies = do
  blurb "pick antecedent conclusion"
  getConc \(lhs, (_, ante, _)) -> do
    blurb "pick X&rArr;Y conclusion"
    getConc \(rhs, ctx@(_, dedu, _)) -> do
      case _expr $ rootLabel rhs of
        t :-> u
          | t == _expr (rootLabel lhs) -> do
            deduceMulti u [ante] ctx
          | otherwise -> oops $ concat ["want ", show t, ", got ", show $ _expr $ rootLabel lhs]
        _ -> oops "want X&rArr;Y"

lem = do
  blurb "pick live X&rArr;&perp; with &perp; conclusion"
  getLive \(node, ctx@(_, dedu, _)) -> do
    let hypo = _expr $ rootLabel node
    case hypo of
      t :-> Bot -> case _expr $ rootLabel $ _tree dedu of
        Bot -> do
          discharge hypo dedu
          deduce t ctx
        _ -> oops "want &perp; conclusion"
      _ -> oops "want X&rArr;Y"

unbot = do
  blurb "pick &perp; conclusion"
  getConc \(bot, ctx) -> \cases
    | Bot == _expr (rootLabel bot) -> do
      blurb "pick any formula"
      getAny \(node, _) -> deduce (_expr $ rootLabel node) ctx
    | otherwise -> oops "want &perp;"
readLevels = go . lines <$> jsEval "lvls.getElementsByTagName('pre')[0].innerText;" where
  go = \case
    flav:goal:src:rules:rest -> f $ go rest
      where
      f = either error (:) do
        g <- parse formula "" goal
        xs <- mapM (parse formula "") $ words src
        pure (flav, g, xs, words rules)
    _ -> []

levels = unsafePerformIO $ newIORef =<< readLevels

initLevel n = do
  ls <- readIORef levels
  if n < length ls then initSingle n (ls!!n) else do
    jsEval_ "sandbox.style.display='';campaign.style.display='none';"
    jsEval_ "initButtons();"
    jsEval_ "const es = rules.getElementsByClassName('pushme'); for (const e of es) showLogic(e);"
    jsEval_ "soil.innerHTML = ''; chosen = undefined;"
    let vb = [-5, -5, minVB + 10, minVB + 10]
    jsEval_ $ concat ["soil.setAttribute('viewBox', '", unwords $ show <$> vb, "');"]
    setGlobal $ Game
      { _deds = []
      , _goal = Bot
      , _level = n
      , _click = anySpot examine
      , _sym = 0
      , _live = []
      , _animcb = undefined
      }

initSingle n (flav, goal, starts, rules) = do
  jsEval_ "sandbox.style.display='none';campaign.style.display='';"
  jsEval_ $ concat ["initButtons();thmno.innerText = '", show n, "';"]
  jsEval_ $ concat ["flavour.innerHTML = `<i>", flav, "</i>`;"]
  mapM_ (\s -> jsEval_ $ "showLogic(" ++ s ++ ");") rules
  let
    deds = initSpots starts
    [x, _, w, _] = _dim (last deds)
    sz = max minVB $ x + w

  setGlobal $ Game
    { _deds = deds
    , _goal = goal
    , _level = n
    , _click = anySpot examine
    , _sym = length starts
    , _live = ("spot"++) . show <$> [0..length starts - 1]
    , _animcb = undefined
    }
  let vb = [-5, -5, sz + 10, sz + 10]
  g <- global
  jsEval_ $ concat ["goal.innerHTML=`", show $ _goal g, "`;"]
  jsEval_ $ concat ["soil.setAttribute('viewBox', '", unwords $ show <$> vb, "');"]
  jsEval_ "soil.innerHTML = ''; chosen = undefined;"
  mapM_ drawDedu $ _deds g
  mapM_ redden $ _deds g

initLevel 0
jsEval "initGame(repl);"
reset = do
  untool
  initLevel . _level =<< global

advance = do
  g <- global
  initLevel $ _level g + 1
parseHypo = do
  s <- jsEval "hypoText.value;"
  case parse formula "" s of
    Left err -> oops err
    Right expr -> do
      sym <- genSym
      g <- global
      let
        deds = _deds g
        xD = case deds of
          [] -> 0
          _ -> x + w + hgap where [x, _, w, _] = _dim $ last deds
        hw = hafwid expr
        w = 2*hw
        spid = "spot" ++ show sym
        did = "dedu" ++ show sym
        sp = Spot { _id = spid, _xywh = [0, 0, w, cellHeight], _expr = expr }
        dedu = Deduction did [xD, 0, w, cellHeight] (Node sp [])
        srcW = max minVB $ xD - hgap
        tgtW = max minVB $ xD + w
      when (tgtW > srcW) $ animGrow srcW $ tgtW - srcW
      setGlobal g { _deds = deds ++ [dedu], _live = spid : _live g }
      drawDedu dedu
      redden dedu
      animThen $ pure ()
Show yourself!
a->a
a
implies
Ghosts of departed hypotheses
a->b->a
a b
implies impliesZ
An introduction to elimination
a->(a->b)->b
a a->b
implies impliesZ unimplies
Take me to your Reader
(a->b->c)->(a->b)->a->c
a a a->b a->b->c
implies impliesZ unimplies
Two wrongs make a right
((a->0)->0)->a
a->0 (a->0)->0
implies impliesZ unimplies LEM
Logic bomb
0->a
0 a->0
implies impliesZ unimplies LEM
Aftershock
(a->0)->a->b
a a->0 b->0
implies impliesZ unimplies LEM
The lie becomes the truth
((a->0)->a)->a
a->0 a->0 (a->0)->a
implies impliesZ unimplies LEM
Peirce is worse
((a->b)->a)->a
a a->0 a->0 b->0 (a->b)->a
implies impliesZ unimplies LEM
One rule to rule them all
((a->b)->c)->((c->a)->(d->a))
a a->0 a->0 b->0 d c->a (a->b)->c
implies impliesZ unimplies LEM
Just a second
a&b->b
a&b
implies impliesZ unimplies unand1 unand2
Caboodle and kit
a&b->b&a
a&b a&b
implies impliesZ unimplies and unand1 unand2
Or else what?
a->a+b
a b
implies impliesZ unimplies or1 or2 unor
Shine or rain
a+b->b+a
a+b a b
implies impliesZ unimplies or1 or2 unor
You say either and I say disjunction
(a->c)->(b->c)->a+b->c
a b a->c b->c a+b
implies impliesZ unimplies or1 or2 unor
Intuitionistic logic bomb
0->a
0 a
implies impliesZ unimplies unbot
Two wrongs no longer make a right
(a+(a->0)->0)->0
a a->0 a+(a->0)->0 a+(a->0)->0
implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2
Disjunction to implication
a+b->(a->b)->b
a+b a b a->b
implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2
One-way trip
((((a->b)->b)->a+b)->0)->0
a a b b (a->b)->b (((a->b)->b)->a+b)->0 (((a->b)->b)->a+b)->0
implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2
Not to be confused with Distributivism
a&b+a&c->a&(b+c)
b c a&b a&b a&c a&c a&b+a&c
implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2
The proof is always easier on the other side
a&(b+c)->a&b+a&c
b c a&(b+c) a&(b+c) a&(b+c)
implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2
⏴ Matrix CombinatorsLisp ⏵
Contents
Ben Lynn blynn@cs.stanford.edu 💡