类型评估的派生树

Question

我想创建派生树来进行类型评估（不知道这到底叫什么）。基本上，我想重现第 15 页上的这棵自下而上的“树”，来自http://lucacardelli.name/papers/typesystems.pdf。

到目前为止，我发现最接近的东西发布在评论中（逻辑学家使用的 LaTeX），因为我的声誉不到 10，只能发布一个链接。但可能有一个完全适合这个的软件包或一种简单的方法来实现这一点。

我已经用以下代码构建了树的各个部分

% 1: numerator
% 2: denominator
% 3: rule name
% 4: label without eqn:, can be referenced with \eqref{eqn:#4} 
\newcommand{\ruledef}[4] 
    {
        \begin{equation}
            \fontsize{11pt}{12pt}\selectfont
            \tag{\textsc{#3}}
            \frac{\text{#1}}{\text{#2}}
            \label{eqn:#4}
        \end{equation}
    }

这样就创建了树的单个部分，标签位于右侧。但我不知道如何将两个方程放在同一高度，并且标签就在它们旁边。我也不知道如何将这些方程居中并将它们捆绑在一起。

Answer 1

这个ebproof包确实很方便。唯一的缺点是我无法对齐推理规则的所有行。使用 tikz 进行一些 twicking 可以帮助您实现这一点，但与此同时，这就是您能得到的：

\documentclass{article}
\usepackage{ebproof}
% \usepackage{tikz} % Useless, but might be handy to draw fancier lines.
\usepackage{amssymb} % To provide the \varnothing symbol
\newcommand{\nothing}{\varnothing} % different from \emptyset
\begin{document}
    \begin{prooftree} %[rule code={\hbox{\tikz \draw (0em,0) -- (\hsize,0);}}] % You should refer to ebproof's manual to twickle lines.
%1st branch
        \Infer0[by (Env \(\nothing\))]{\nothing \vdash \diamond}
        \Infer1[by (Type Const)]{\nothing \vdash K}
        \Infer0[by (Env \(\nothing\))]{\nothing \vdash \diamond}
        \Infer1[by (Type Const)]{\nothing \vdash K}
        \Infer2[by (Type Arrow)]{\nothing \vdash K \to K}
        \Infer1[by (Env \(x\))]{\nothing, y: K \to K  \vdash  \diamond}
        \Infer1[by (Type Const)]{\nothing, y: K \to K  \vdash  K}
        \Infer1[by (Env \(x\))]{\nothing, y: K \to K, z:K  \vdash \diamond}
        \Infer1[by (Val \(x\))]{\nothing, y: K \to K, z:K  \vdash y : K \to K}      
% 2nd branch
        \Infer0[by (Env \(\nothing\))]{\nothing \vdash \diamond}
        \Infer1[by (Type Const)]{\nothing \vdash K}
        \Infer0[by (Env \(\nothing\))]{\nothing \vdash \diamond}
        \Infer1[by (Type Const)]{\nothing \vdash K}
        \Infer2[by (Type Arrow)]{\nothing \vdash K \to K}
        \Infer1[by (Env \(x\))]{\nothing, y: K \to K  \vdash  \diamond}
        \Infer1[by (Type Const)]{\nothing, y: K \to K  \vdash  K}
        \Infer1[by (Env \(x\))]{\nothing, y: K \to K, z:K  \vdash \diamond}
        \Infer1[by (Val \(x\))]{\nothing, y: K \to K, z:K  \vdash z : K \to K}  
% Conclusion
        \Infer2[by (Val Appl)]{\nothing, y: K \to K, z:K  \vdash y(z) : K}  
        \Infer1[by (Val Fun)]{\nothing, y: K \to K, z:K  \vdash \lambda z : K.y(z) : K \to K}           
    \end{prooftree}
\end{document}