Derivation tree for type evaluations

Question

I’d like to create derivations trees for a type evaluation (dunno what this is exactly called). Basically I want to reproduce this bottom up „tree“ on page 15 from http://lucacardelli.name/papers/typesystems.pdf.

The closest thing I’ve found yet is posted in the comment (LaTeX for logicians) since I have <10 reputation an can only post one link. But there may be a package for exactly this or an easy way for doing this.

I already build single parts of the tree with

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

This creates a single part of the tree with the tagon the right side. But I don‘t know how to have two of this equations on the same height with their tag right near them. Also I don’t know to center these equations and bundle them alltogether.

Answer 1

The ebproof package is indeed handy. The only drawback it that I was'nt able to align all the lines of the inference rules. Some twicking with tikz could help you to achieve that, but, in the meantime, that is what you could get:

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