haskell latex proof

Pruebas de deducción natural LaTeX utilizando Haskell



proof (1)

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

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.