Pruebas de deducción natural LaTeX utilizando Haskell

proof

Question

¿Cómo se puede crear una fuente LaTeX para árboles de prueba de deducción natural ( como los que se muestran aquí ) a través de Haskell, por ejemplo, utilizando HaTeX ? Me gustaría emular a LaTeX .sty s like bussproofs.sty or proof.sty .

Answer 1

Estoy usando tu pregunta como una excusa para mejorar y demostrar una biblioteca de rastreo de llamadas de Haskell en la que estoy trabajando . En el contexto del rastreo, una forma obvia de crear un árbol de prueba es rastrear un verificador de tipos y luego formatear el rastreo como una prueba de deducción natural. Para simplificar las cosas, mi ejemplo de lógica es el cálculo lambda de tipo simple (STLC) , que corresponde al fragmento implicacional de la lógica intuicionista proposicional.

Estoy usando proofs.sty , pero no a través de HaTeX ni de ninguna otra biblioteca de Haskell Latex. El Latex para árboles de prueba es muy simple y usar una biblioteca Haskell Latex solo complicaría las cosas.

He escrito el código de generación del árbol de pruebas dos veces:

1. de forma autocontenida, al escribir un comprobador de tipos que también devuelve un árbol de prueba;

2. utilizando mi biblioteca de rastreo, mediante el rastreo de llamadas de un comprobador de tipos y luego el procesamiento del rastreo en un árbol de prueba.

Dado que no ha preguntado acerca de las bibliotecas de rastreo de llamadas, es posible que esté menos interesado en la versión basada en rastreo de llamadas, pero creo que es interesante comparar ambas versiones.

Ejemplos

Comencemos con algunos ejemplos de salida primero, para ver qué nos trae todo esto. Los primeros tres ejemplos están motivados por un sistema de axiomas para el cálculo proposicional implicacional ; Los dos primeros también corresponden a S y K :

• El primer axioma, K , con términos de prueba:

• El segundo axioma, S , con términos de prueba, pero con premisas en el contexto, no enlazado con lambda:

• El cuarto axioma, modus ponens, sin términos de prueba:

El tercer axioma en ese artículo de Wikipedia (la ley de Peirce) no es constructivo, por lo que no podemos demostrarlo aquí.

Para un tipo diferente de ejemplo, aquí hay una comprobación de tipo fallida del combinador Y :

Las flechas están destinadas a llevarlo al error, que está marcado con un golpe ( ! ).

Código

Ahora describiré el código que generó esos ejemplos. El código es de este archivo a menos que se indique lo contrario. No estoy incluyendo todas las líneas de código aquí; vea ese enlace si quiere algo que realmente pueda construir usando GHC 7.6.3.

La mayor parte del código (la gramática, el analizador y la bonita impresora) es el mismo para ambas versiones; solo los controladores de tipo y los generadores de prueba de árbol difieren. Todo el código común está en el archivo al que se hace referencia .

Gramática STLC

La gramática STLC en ASCII:

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

Y el correspondiente 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)]

Tipo de comprobación + generación de árbol de prueba

Ambas versiones implementan el mismo comprobador de tipo STLC abstracto. En 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

Versión 1: autocontenida con generación de pruebas en línea

El código completo para esta versión está here .

La generación del árbol de pruebas se produce en el comprobador de tipos, pero el código de generación del árbol de pruebas real se addProof en addProof y conclusion .

Verificación de tipos

-- 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

Generación de árbol de prueba

El addProof corresponde a proofTree en la otra versión:

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

El código para la conclusion es común a ambas versiones:

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

Versión 2: a través del rastreo de llamadas, con generación del árbol de pruebas como procesamiento posterior

Aquí el comprobador de tipos ni siquiera conoce la generación del árbol de pruebas, y agregar el rastreo de llamadas es solo una línea.

Verificación de tipos

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

El tipo LogStream y la clase ProofTree son de la biblioteca. LogStream es el tipo de eventos de registro que simpleLogger registro " simpleLogger " de "magic". Nota la linea

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

que define infer como una versión registrada de infer'' , el verificador de tipo real. ¡Eso es todo lo que tienes que hacer para rastrear una función monádica!

No me simpleLogger cómo simpleLogger realmente el simpleLogger aquí, pero el resultado es que cada llamada a infer se registra, incluido el contexto, los argumentos y el valor de retorno, y estos datos se agrupan con todas las llamadas secundarias registradas (aquí solo para infer ) . Sería fácil escribir manualmente dicho código de registro para infer , pero es bueno que con la biblioteca no tenga que hacerlo.

Generación de árbol de prueba

Para generar los árboles de prueba de látex, implementamos ProofTree para publicar el rastreo de llamadas de infer . La biblioteca proporciona una función proofTree que llama a los métodos ProofTree y ensambla los árboles de prueba; solo necesitamos especificar cómo se formatearán las conclusiones de los juicios de tipeo:

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

Las llamadas pp son a una impresora bonita definida por el usuario; Obviamente, la biblioteca no puede saber cómo imprimir sus tipos de datos.

Debido a que las llamadas pueden ser erróneas, la biblioteca detecta errores, tenemos que decir cómo dar formato a las llamadas exitosas y fallidas. Consulte el ejemplo del combinador en Y anterior para ver un ejemplo de verificación de tipo fallido, correspondiente al caso callAndError aquí.

La función proofTree la biblioteca es bastante simple: construye un árbol de pruebas de proofs.sty con la llamada actual como conclusión y las subclaves como premisas:

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

Utilizo proofs.sty en la biblioteca porque permite arbitrariamente muchas premisas, aunque bussproofs.sty funcionaría para este ejemplo de STLC, ya que ninguna regla tiene más de cinco premisas (el límite para bussproofs ). Ambos paquetes de látex se describen aquí .

Impresión bonita

Ahora volvemos al código que es común entre ambas versiones.

La bonita impresora que define los pp utilizados anteriormente es bastante larga: maneja la precedencia y la asociatividad, y está escrita de una manera que debería ser extensible si se añaden más términos, por ejemplo, productos, al cálculo, pero en su mayoría es sencilla. Primero, configuramos una tabla de precedencia y un paréntesis compatible con precedencia y asociatividad:

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

Y luego definimos las impresoras bonitas individuales:

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 ]

Al agregar un argumento de "modo", sería fácil usar la misma impresora bonita para imprimir ASCII simple, lo que sería útil con otros post procesadores de seguimiento de llamadas, como el procesador UnixTree (sin terminar).

Análisis

Un analizador no es esencial para el ejemplo, pero, por supuesto, no ingresé los términos de entrada de ejemplo directamente como Haskell Tm s.

Recordemos la gramática STLC en ASCII:

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

Esta gramática es ambigua: tanto el término aplicación ee como el tipo de función T -> T no tienen asociatividad dada por la gramática. Pero en STLC, la aplicación de términos es asociativa a la izquierda y los tipos de función son asociativos a la derecha, por lo que la gramática desambiguada correspondiente que analizamos es

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

El analizador es quizás demasiado simple: no estoy usando un languageDef y es sensible al espacio en blanco, pero hace el trabajo:

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 '','')

Para aclarar cómo se ven los términos de entrada, aquí están los ejemplos de 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)))''

Generación de documentos de látex

El script ./tm2latex.sh simplemente llama a pdflatex en la salida de los programas de Haskell descritos anteriormente. Los programas de Haskell producen el árbol de prueba y luego lo envuelven en un documento de Latex mínimo:

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}"
  ]

Como puede ver, la mayor parte del látex está dedicado a hacer los árboles de prueba lo más pequeños posible; También planeo escribir un postprocesador de prueba de árbol ASCII, que puede ser más útil en la práctica cuando los ejemplos son más grandes.

Conclusión

Como siempre, se necesita un poco de código para escribir un analizador, un comprobador de tipos y una impresora bonita. Además de eso, agregar la generación del árbol de prueba es bastante simple en ambas versiones. Este es un ejemplo de juguete divertido, pero espero hacer algo similar en el contexto de un verificador de tipos basado en la unificación "real" para un lenguaje de tipo dependiente; allí espero que el rastreo de llamadas y la generación del árbol de prueba (en ASCII) proporcionen una ayuda significativa en la depuración del comprobador de tipos.