haskell - 使用 Haskell 的 LaTeX 自然演绎证明

Question

如何通过 Haskell（例如使用HaTeX ）为自然演绎证明树（如此处所示）创建 LaTeX 源？我想模仿像bussproofs.sty或proof.sty这样的 LaTeX 。.sty

Answer 1

我以您的问题为借口来改进和演示我正在开发的 Haskell 调用跟踪库。在跟踪的上下文中，创建证明树的一种明显方法是跟踪类型检查器，然后将跟踪格式化为自然演绎证明。为了简单起见，我的示例逻辑是简单类型的 lambda 演算 (STLC)，它对应于命题 直觉逻辑的暗示片段。

我正在使用proofs.sty，但不是通过HaTeX或任何其他 Haskell Latex 库。证明树的 Latex 非常简单，使用 Haskell Latex 库只会使事情复杂化。

我已经编写了两次证明树生成代码：

1. 以一种自包含的方式，通过编写一个类型检查器来返回一个证明树；

2. 使用我的跟踪库，通过调用跟踪类型检查器，然后将跟踪后处理到证明树中。

由于您没有询问调用跟踪库，您可能对基于调用跟踪的版本不太感兴趣，但我认为比较两个版本很有趣。

例子

让我们首先从一些输出示例开始，看看这一切给我们带来了什么。前三个例子是由蕴含命题演算的公理系统激发的；前两个也恰好对应于Sand K：

• 第一个公理 ，K带有证明项：

  

• 第二个公理 ，S带有证明项，但在上下文中有前提，而不是 lambda 约束：

  

• 第四个公理，作案方式，没有证明项：

  

维基百科文章中的第三个公理（皮尔士定律）是非建设性的，所以我们不能在这里证明它。

对于另一种示例，这是Y 组合器的类型检查失败：

箭头旨在将您引向错误，该错误标有 bang ( !)。

代码

现在我将描述生成这些示例的代码。 除非另有说明，否则代码来自此文件。我没有在这里包含每一行代码；如果您想要可以使用 GHC 7.6.3 实际构建的东西，请查看该链接。

两个版本的大部分代码——语法、解析器和漂亮的打印机——都是相同的。只有类型检查器和证明树生成器不同。所有通用代码都在刚刚引用的文件中。

STLC 语法

ASCII 中的 STLC 语法：

-- Terms
e ::= x | \x:T.e | e e
-- Types
T ::= A | T -> T
-- Contexts
C ::= . | C,x:T

以及相应的 Haskell：

type TmVar = String
type TyVar = String
data Tm = Lam TmVar Ty Tm
        | TmVar TmVar
        | Tm :@: Tm
  deriving Show
data Ty = TyVar TyVar
        | Ty :->: Ty
  deriving (Eq , Show)
type Ctx = [(TmVar,Ty)]

类型检查+证明树生成

两个版本都实现了相同的抽象 STLC 类型检查器。在 ASCII 中：

(x:T) in C
---------- Axiom
C |- x : T

C,x:T1 |- e : T2
--------------------- -> Introduction
C |- \x:T1.e : T1->T2

C |- e : T1 -> T2    C |- e1 : T1
--------------------------------- -> Elimination
C |- e e1 : T2

版本 1：自包含的内联证明树生成

这个版本的完整代码在 这里。

证明树生成发生在类型检查器中，但实际的证明树生成代码被分解为addProofand conclusion。

类型检查

-- The mode is 'True' if proof terms should be included.
data R = R { _ctx :: Ctx , _mode :: Bool }
type M a = Reader R a

extendCtx :: TmVar -> Ty -> M a -> M a
extendCtx x t = local extend where
  extend r = r { _ctx = _ctx r ++ [(x,t)] }

-- These take the place of the inferred type when there is a type
-- error.
here , there :: String
here = "\\,!"
there = "\\,\\uparrow"

-- Return the inferred type---or error string if type inference
-- fails---and the latex proof-tree presentation of the inference.
--
-- This produces different output than 'infer' in the error case: here
-- all premises are always computed, whereas 'infer' stops at the
-- first failing premise.
inferProof :: Tm -> M (Either String Ty , String)
inferProof tm@(Lam x t e) = do
  (et' , p) <- extendCtx x t . inferProof $ e
  let et'' = (t :->:) <$> et'
  addProof et'' [p] tm
inferProof tm@(TmVar x) = do
  mt <- lookup x <$> asks _ctx
  let et = maybe (Left here) Right mt
  addProof et [] tm
inferProof tm@(e :@: e1) = do
  (et , p) <- inferProof e
  (et1 , p1) <- inferProof e1
  case (et , et1) of
    (Right t , Right t1) ->
      case t of
        t1' :->: t2 | t1' == t1 -> addProof (Right t2)   [p , p1] tm
        _ ->                       addProof (Left here)  [p , p1] tm
    _ ->                           addProof (Left there) [p , p1] tm

证明树生成

addProof对应于proofTree其他版本：

-- Given the inferred type, the proof-trees for all premise inferences
-- (subcalls), and the input term, annotate the inferred type with a
-- result proof tree.
addProof :: Either String Ty -> [String] -> Tm -> M (Either String Ty , String)
addProof et premises tm = do
  R { _mode , _ctx } <- ask
  let (judgment , rule) = conclusion _mode _ctx tm et
  let tex = "\\infer[ " ++ rule ++ " ]{ " ++
            judgment ++ " }{ " ++
            intercalate " & " premises ++ " }"
  return (et , tex)

两个版本的代码conclusion是通用的：

conclusion :: Mode -> Ctx -> Tm -> Either String Ty -> (String , String)
conclusion mode ctx tm e = (judgment mode , rule tm)
  where
    rule (TmVar _) = "\\textsc{Axiom}"
    rule (Lam {}) = "\\to \\text{I}"
    rule (_ :@: _) = "\\to \\text{E}"

    tyOrError = either id pp e

    judgment True = pp ctx ++ " \\vdash " ++ pp tm ++ " : " ++ tyOrError
    judgment False = ppCtxOnlyTypes ctx ++ " \\vdash " ++ tyOrError

版本 2：通过调用跟踪，将证明树生成作为后处理

在这里，类型检查器甚至不知道证明树的生成，添加调用跟踪只是一行。

类型检查

type Mode = Bool
type Stream = LogStream (ProofTree Mode)
type M a = ErrorT String (ReaderT Ctx (Writer Stream)) a

type InferTy = Tm -> M Ty
infer , infer' :: InferTy
infer = simpleLogger (Proxy::Proxy "infer") ask (return ()) infer'

infer' (TmVar x) = maybe err pure . lookup x =<< ask where
  err = throwError $ "Variable " ++ x ++ " not in context!"
infer' (Lam x t e) = (t :->:) <$> (local (++ [(x,t)]) . infer $ e)
infer' (e :@: e1) = do
  t <- infer e
  t1 <- infer e1
  case t of
    t1' :->: t2 | t1' == t1 -> pure t2
    _ -> throwError $ "Can't apply " ++ show t ++ " to " ++ show t1 ++ "!"

LogStream 类型 和ProofTree 类 来自库。这LogStream是“魔术”记录的日志事件的类型 simpleLogger 。注意线

infer = simpleLogger (Proxy::Proxy "infer") ask (return ()) infer'

它定义为实际类型检查器infer的记录版本。infer'这就是追踪一元函数所需要做的一切！

我不会simpleLogger在这里讨论实际是如何工作的，但结果是每次调用infer都会被记录下来，包括上下文、参数和返回值，并且这些数据会与所有记录的子调用组合在一起（这里只有 to infer）。为 手动编写这样的日志记录代码很容易infer，但是使用该库您不必这样做，这很好。

证明树生成

为了生成 Latex 证明树，我们实现ProofTree了 post processinfer的调用跟踪。该库提供了一个proofTree 调用ProofTree方法并组装证明树的函数；我们只需要指定打字判断的结论将如何格式化：

instance ProofTree Mode (Proxy (SimpleCall "infer" Ctx InferTy ())) where
  callAndReturn mode t = conclusion mode ctx tm (Right ty)
    where
      (tm , ()) = _arg t
      ty = _ret t
      ctx = _before t
  callAndError mode t = conclusion mode ctx tm (Left error)
    where
      (tm , ()) = _arg' t
      how = _how t
      ctx = _before' t
      error = maybe "\\,!" (const "\\,\\uparrow") how

调用的pp是用户定义的漂亮打印机；显然，库不知道如何漂亮地打印您的数据类型。

因为调用可能是错误的——库检测错误——我们必须说明如何格式化成功和失败的调用。有关类型检查失败的示例，请参阅上面的 Y-combinator 示例，对应于 callAndError此处的情况。

该库的proofTree 功能 非常简单：它proofs.sty以当前调用为结论，以子调用为前提构建一个证明树：

proofTree :: mode -> Ex2T (LogTree (ProofTree mode)) -> String
proofTree mode (Ex2T t@(CallAndReturn {})) =
  "\\infer[ " ++ rule ++ " ]{ " ++ conclusion ++ " }{ " ++ intercalate " & " premises ++ " }"
  where
    (conclusion , rule) = callAndReturn mode t
    premises = map (proofTree mode) (_children t)
proofTree mode (Ex2T t@(CallAndError {})) =
  "\\infer[ " ++ rule ++ " ]{ " ++ conclusion ++ " }{ " ++ intercalate " & " premises ++ " }"
  where
    (conclusion , rule) = callAndError mode t
    premises = map (proofTree mode)
                   (_children' t ++ maybe [] (:[]) (_how t))

我proofs.sty在图书馆中使用它是因为它允许任意多个前提，尽管bussproofs.sty适用于这个 STLC 示例，因为没有规则有超过五个前提（ 的限制 bussproofs）。两个 Latex 包都在 这里描述。

漂亮的印刷

现在我们回到两个版本之间通用的代码。

定义上述pp使用的漂亮打印机相当长——它处理优先级和关联性，并且如果将更多术语（例如乘积）添加到微积分中，则其编写方式应该是可扩展的——但主要是直截了当的。首先，我们设置了一个优先表和一个优先级和关联性感知括号：

- Precedence: higher value means tighter binding.
type Prec = Double

between :: Prec -> Prec -> Prec
between x y = (x + y) / 2

lowest , highest , precLam , precApp , precArr :: Prec
highest = 1
lowest = 0
precLam = lowest
precApp = between precLam highest
precArr = lowest

-- Associativity: left, none, or right.
data Assoc = L | N | R deriving Eq

-- Wrap a pretty print when the context dictates.
wrap :: Pretty a => Assoc -> a -> a -> String
wrap side ctx x = if prec x `comp` prec ctx
                  then pp x
                  else parens . pp $ x
  where
    comp = if side == assoc x || assoc x == N
           then (>=)
           else (>)
    parens s = "(" ++ s ++ ")"

然后我们定义各个漂亮的打印机：

class Pretty t where
  pp :: t -> String
  prec :: t -> Prec
  prec _ = highest
  assoc :: t -> Assoc
  assoc _ = N

instance Pretty Ty where
  pp (TyVar v) = v
  pp t@(t1 :->: t2) = wrap L t t1 ++ " {\\to} " ++ wrap R t t2
  prec (_ :->: _) = precArr
  prec _ = highest
  assoc (_ :->: _) = R
  assoc _ = N

instance Pretty Tm where
  pp (TmVar v) = v
  pp (Lam x t e) = "\\lambda " ++ x ++ " {:} " ++ pp t ++ " . " ++ pp e
  pp e@(e1 :@: e2) = wrap L e e1 ++ " " ++ wrap R e e2
  prec (Lam {}) = precLam
  prec (_ :@: _) = precApp
  prec _ = highest
  assoc (_ :@: _) = L
  assoc _ = N

instance Pretty Ctx where
  pp [] = "\\cdot"
  pp ctx@(_:_) =
    intercalate " , " [ x ++ " {:} " ++ pp t | (x,t) <- ctx ]

通过添加“模式”参数，可以很容易地使用相同的漂亮打印机打印纯 ASCII，这对于其他调用跟踪后处理器（例如（未完成的）UnixTree 处理器）很有用。

解析

解析器对于示例来说不是必需的，但是我当然没有将示例输入项直接作为 Haskell 输入Tm。

回忆一下 ASCII 中的 STLC 语法：

-- Terms
e ::= x | \x:T.e | e e
-- Types
T ::= A | T -> T
-- Contexts
C ::= . | C,x:T

该文法是模棱两可的：术语应用程序e e 和函数类型T -> T都没有文法给出的关联性。但是在 STLC 中，应用是左结合的，函数类型是右结合的，所以我们实际解析的对应的消歧文法是

-- Terms
e ::= e' | \x:T.e | e e'
e' ::= x | ( e )
-- Types
T ::= T' | T' -> T
T' ::= A | ( T )
-- Contexts
C ::= . | C,x:T

解析器可能太简单了——我没有使用 alanguageDef并且它对空格敏感——但它完成了工作：

type P a = Parsec String () a

parens :: P a -> P a
parens = Text.Parsec.between (char '(') (char ')')

tmVar , tyVar :: P String
tmVar = (:[]) <$> lower
tyVar = (:[]) <$> upper

tyAtom , arrs , ty :: P Ty
tyAtom = parens ty
     <|> TyVar <$> tyVar
arrs = chainr1 tyAtom arrOp where
  arrOp = string "->" *> pure (:->:)
ty = arrs

tmAtom , apps , lam , tm :: P Tm
tmAtom = parens tm
     <|> TmVar <$> tmVar
apps = chainl1 tmAtom appOp where
  appOp = pure (:@:)
lam = uncurry Lam <$> (char '\\' *> typing)
                  <*> (char '.' *> tm)
tm = apps <|> lam

typing :: P (TmVar , Ty)
typing = (,) <$> tmVar
             <*> (char ':' *> ty)

ctx :: P Ctx
ctx = typing `sepBy` (char ',')

为了阐明输入术语的样子，以下是 Makefile 中的示例：

#           OUTFILE  CONTEXT                TERM
./tm2latex.sh S.ctx  'x:P->Q->R,y:P->Q,z:P' 'xz(yz)'
./tm2latex.sh S.lam  ''                     '\x:P->Q->R.\y:P->Q.\z:P.xz(yz)'
./tm2latex.sh S.err  ''                     '\x:P->Q->R.\y:P->Q.\z:P.xzyz'
./tm2latex.sh K.ctx  'x:P,y:Q'              'x'
./tm2latex.sh K.lam  ''                     '\x:P.\y:Q.x'
./tm2latex.sh I.ctx  'x:P'                  'x'
./tm2latex.sh I.lam  ''                     '\x:P.x'
./tm2latex.sh MP.ctx 'x:P,y:P->Q'           'yx'
./tm2latex.sh MP.lam ''                     '\x:P.\y:P->Q.yx'
./tm2latex.sh ZERO   ''                     '\s:A->A.\z:A.z'
./tm2latex.sh SUCC   ''                     '\n:(A->A)->(A->A).\s:A->A.\z:A.s(nsz)'
./tm2latex.sh ADD    '' '\m:(A->A)->(A->A).\n:(A->A)->(A->A).\s:A->A.\z:A.ms(nsz)'
./tm2latex.sh MULT   '' '\m:(A->A)->(A->A).\n:(A->A)->(A->A).\s:A->A.\z:A.m(ns)z'
./tm2latex.sh Y.err  ''                        '\f:A->A.(\x:A.f(xx))(\x:A.f(xx))'
./tm2latex.sh Y.ctx  'a:A->(A->A),y:(A->A)->A' '\f:A->A.(\x:A.f(axx))(y(\x:A.f(axx)))'

Latex 文档生成

该./tm2latex.sh脚本仅调用pdflatex上述 Haskell 程序的输出。Haskell 程序生成证明树，然后将其包装在一个最小的 Latex 文档中：

unlines
  [ "\\documentclass[10pt]{article}"
  , "\\usepackage{proof}"
  , "\\usepackage{amsmath}"
  , "\\usepackage[landscape]{geometry}"
  , "\\usepackage[cm]{fullpage}"
  -- The most slender font I could find:
  -- http://www.tug.dk/FontCatalogue/iwonalc/
  , "\\usepackage[light,condensed,math]{iwona}"
  , "\\usepackage[T1]{fontenc}"
  , "\\begin{document}"
  , "\\tiny"
  , "\\[" ++ tex ++ "\\]"
  , "\\end{document}"
  ]

如您所见，大部分 Latex 致力于使证明树尽可能小；我还计划编写一个 ASCII 证明树后处理器，当示例更大时，它在实践中可能更有用。

结论

与往常一样，编写解析器、类型检查器和漂亮的打印机需要一些代码。最重要的是，在两个版本中添加证明树生成都非常简单。这是一个有趣的玩具示例，但我希望在依赖类型语言的“真正的”基于统一的类型检查器的上下文中做类似的事情；在那里，我希望调用跟踪和证明树生成（以 ASCII 格式）为调试类型检查器提供重要帮助。