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

Question

如何通过Haskell为自然演绎证明树(like those shown here)创建LaTeX源，例如使用HaTeX？我想模拟LaTeX .sty，例如bussproofs.sty或proof.sty。

Answer 1

我以您的问题为借口来改进和演示a Haskell call-tracing library I'm working on。在上下文中
跟踪，创建证明树的一种明显方法是跟踪类型
检查，然后将迹线格式化为自然推论证明。至
保持简单，我的示例逻辑是simply-typed lambda calculus (STLC)，
对应于命题的暗示片段
intuitionistic logic。

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

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

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

使用我的跟踪库，通过调用跟踪类型检查器，然后使用

将跟踪后处理到证明树中。

由于您没有询问 call 跟踪库，因此您可能会少一些
对基于 call 跟踪的版本感兴趣，但我认为这是
比较两个版本很有趣。

例子

让我们首先从一些输出示例开始，看看这一切能给我们带来什么。
前三个例子是有动机的
由an axiom system for implicational propositional calculus;
前两个碰巧也对应于 S and K :

第一个公理K，带有证明条款:

第二个公理S，带有证明条款，但前提是
上下文，不受lambda约束:

第四个公理，惯用法，没有证明条款:

该维基百科文章(皮尔斯定律)中的第三个公理是
非 build 性的，因此我们在这里无法证明。

对于另一种示例，这是Y combinator的类型检查失败:

箭头旨在引导您找到错误，并标有一个
砰(!)。

码

现在，我将描述生成这些示例的代码。该代码是
来自this file
除非另有说明。我没有在这里包括每一行代码。
如果您想要可以使用GHC进行实际构建的内容，请参见该链接
7.6.3。

大多数代码-语法，解析器和 pretty-print -是
两个版本相同；仅类型检查器和证明树
发电机不同。所有通用代码都在file just referenced中。

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:自包含，带有内嵌证明树生成

该版本的完整代码为
here。

证明树的生成发生在类型检查器中，但是实际
证明树生成代码分解为addProof和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:通过 call 跟踪，带有证明树生成作为后处理

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

类型检查

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 type
和 ProofTree class
来自图书馆。 LogStream是日志事件的类型，
魔术”
simpleLogger
日志。注意行

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

将infer定义为infer'的记录版本，实际
类型检查器。这就是跟踪单子(monad)函数所要做的全部!

我不会在这里了解simpleLogger的实际工作原理，但是
结果是记录了对infer的每次调用，包括
上下文，参数和返回值，然后将这些数据分组
以及所有记录的子调用(此处仅到infer)。这将是
手动为infer编写这样的日志记录代码很容易，但这很好
无需使用图书馆。

证明树生成

为了生成Latex证明树，我们实现ProofTree来发布
处理infer的 call 跟踪。该库提供了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调用是针对用户定义的 pretty-print 的；显然，
库不知道如何漂亮地打印数据类型。

因为调用可能是错误的，所以库会检测到错误
-我们必须说如何格式化
成功和失败的通话。请引用上面的Y组合器示例
例如，类型检查失败，对应于
此处是callAndError的情况。

library's proofTree function
非常简单:它使用当前代码构建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软件包均已描述
here。

漂亮的打印

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

定义上面使用的pp的 pretty-print 相当长-
它处理优先级和关联性，并且以
如果有更多的用语，例如产品，已添加到
演算-但大多是直接的。首先，我们设置一个优先级
表和一个具有优先级和关联性的括号:

- 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 ++ ")"

然后我们定义各个 pretty-print :

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 ]

通过添加“mode”参数，可以很容易地使用相同的
打印机以打印纯ASCII，这对于其他打印机很有用
call 跟踪后处理程序，例如(未完成的) UnixTree processor。

解析中

解析器对于示例不是必需的，但是我当然没有输入
示例输入术语直接作为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

解析器可能太简单了-我没有使用languageDef和
它对空格敏感-但可以完成工作:

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脚本仅在
上述的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证明树文章
处理器，当示例是
更大。

结论

与往常一样，编写解析器，类型检查器和
pretty-print 。最重要的是，添加证明树生成是
在两个版本中都非常简单。这是一个有趣的玩具示例，但我
期望在“真实”的背景下做类似的事情
基于类型的依存类型检查器，用于依赖类型的语言；那里
我希望可以提供 call 跟踪和证明树生成(以ASCII格式)
对调试类型检查器有很大帮助。