5

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. Derivation tree from cardelli

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.

4
  • logicmatters.net/latex-for-logicians/nd best package I’ve found yet
    – bugybunny
    Nov 19, 2015 at 15:09
  • Welcome to TeX.SE! There are several packages for this in the proof topic on CTAN. Nov 19, 2015 at 15:31
  • @TonioElGringo Thanks! The ebproof package looks really good. Guess I didn’t know what to look for. I try to reconstruct it and if I have I will post my solution as answer.
    – bugybunny
    Nov 19, 2015 at 16:23
  • Or bussproofs, but this is definitely covered at LaTeX for Logicians.
    – cfr
    Nov 20, 2015 at 12:36

1 Answer 1

5

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}

enter image description here

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .