I worked with type theoretical concepts during my postgrads and often used the mathpartir package while writing reports with LaTeX. Among other things, mathpartir offers the \inferrule command that can be used to display derivation trees like the one shown in Figure 1.
Structure of inferrule
mathpartir lets us format inference rules using the \inferrule command.
An inference rule consists of a set of assumptions and a conclusion as represented below:
assm_1 assm_2 ... assum_k
─────────────────────────────
concl
This can be written like the following using \inferrule:
\inferrule{
assm_1 \\
assm_2 \\
...
assm_k \\
}{
concl
}\inferrule
Such rules can be nested as needed to produce proof trees as shown in Figure 3.
assm_1 assm_2 assm_1 assm_2
────────────── ──────────────
concl_1 concl_2
────────────────────────────────────
concl
For example, consider the derivation tree depicted in Figure 4.
a b b c
───────── ─────────
a ∧ b b ∧ c
──────────────────────────
a ∧ b ∧ c
This tree can be made using mathpartir via the LaTeX shown in Snippet 2.
\begin{mathpar}
\inferrule{
\inferrule{
a \\ b
}{
a \land b
}
\\
\inferrule{
b \\ c
}{
b \land c
}
}{
a \land b \land c
}
\end{mathpar}The thing is, for larger trees, it quickly gets difficult to write the LaTeX code.
A way to build named sub-trees which may then be joined up together to create the overall tree would be quite useful. Kind of like a let-binding. For instance, it would be more convenient to write the tree shown in Figure 1 as something like Snippet 3.
let
\r1 = \inferrule{a \\ b}{a \land b}
\r2 = \inferrule{b \\ c}{b \land c}
in
\inferrule{\r1 \\ \r2}{a \land b \land c}
end
let expression in LaTeX
TeX has a \let, but it is not actually a let-binding. It is more like a way of giving an alias to a macro (See this).
For example, both \dhi and \hi in Snippet 4 expand to hi.
% Make a macro \dhi
\def\dhi{hi}
% Make a macro \hi with the same meaning as \dhi
\let\hi\dhi
\bye
% Use xdvi to open resultant dvi file\let in TeX
Though we don't have a \let in TeX, we can still give names to parts of the tree via macros. We can do this either with \def of TeX or \newcommand of LaTeX (or perhaps even \NewCommand of expl3).
Something like what is shown in Snippet 3 can be achieved for Snippet 2 using the LaTeX shown in Snippet 5.
\newcommand\rone{
\inferrule{a \\ b}{a \land b}
}
\newcommand\rtwo{
\inferrule{b \\ c}{b \land c}
}
\inferrule{\rone \\ \rtwo}{a \land b \land c}Macro names cannot have numbers in it (see this discussion for a 'workaround'). So I used names like rone instead of r1.
An example use
All right, let us try a more concrete example.
The proof tree shown in Figure 1 is from an exercise in the Types and Programming Languages book (Exercise 9.2.2). This proof tree can be written using mathpar with the code snippet shown in Snippet 6.
\documentclass{article}
\usepackage{amssymb}
\usepackage{mathpartir}
\newcommand\pr{\vdash}
\begin{document}
\begin{mathpar}
\inferrule*[right=T-App]{
\inferrule*{ }{
f: \mathbb{B} \to \mathbb{B}
}
\\
\inferrule*[right=T-If]{
\inferrule*[right=T-Var]{
\bot: \mathbb{B} \in \Gamma
}{
\Gamma \pr \bot: \mathbb{B}
}
\\
\inferrule*[right=T-Var]{
\top: \mathbb{B} \in \Gamma
}{
\Gamma \pr \top: \mathbb{B}
}
}{
\Gamma \pr
(\mathtt{if}\ \bot\ \mathtt{then}\ \top\
\mathtt{else}\ \bot): \mathbb{B}
}
}{
\Gamma \pr
(f\ (\mathtt{if}\ \bot\ \mathtt{then}\ \top\
\mathtt{else}\ \bot)): \mathbb{B}
}
\end{mathpar}
\end{document}There are 5 rules (same as the number of horizontal lines) being written with the above snippet (See Figure 5). This not very pleasant to write because all five rules are kind of interwoven together.
It can be difficult to see where one sub-tree ends and another begins. Larger the proof tree, easier is it to mess up. Some modularity would be nice, wherein we can deal with each rule independent of others. We can achieve such a 'let-binding'-like effect by defining local macros as was described earlier.
So, the code in Snippet 6 can be re-written as the LaTeX shown in Snippet 7.
\begin{mathpar}
% T-Var
\newcommand\tvarone{%
\inferrule*[right=T-Var]{
\top: \mathbb{B} \in \Gamma
}{
\Gamma \pr \top: \mathbb{B}
}
}
% T-Var
\newcommand\tvartwo{%
\inferrule*[right=T-Var]{
\bot: \mathbb{B} \in \Gamma
}{
\Gamma \pr \bot: \mathbb{B}
}
}
% T-If
\newcommand\tif{%
\inferrule*[right=T-If]{
\tvartwo \\ \tvarone
}{
\Gamma \pr
(\mathtt{if}\ \bot\ \mathtt{then}\ \top\
\mathtt{else}\ \bot): \mathbb{B}
}
}
% Function f given as premise
\newcommand\premf{%
\inferrule*{ }{f: \mathbb{B} \to \mathbb{B}}
}
% T-App
\newcommand\tapp{%
\inferrule*[right=T-App]{
\premf \\ \tif
}{
\Gamma \pr
(f\ (\mathtt{if}\ \bot\ \mathtt{then}\ \top\
\mathtt{else}\ \bot)): \mathbb{B}
}
}
% Final proof tree
\tapp
\end{mathpar}Observe how specific parts of the proof tree can be named and set aside, which can then be plugged in to create the complete derivation tree. Though this might look longer than the original snippet, this is much more easier to deal with. Especially since now one can have a clear idea which part of the code correspond to which sub-tree.
This way of composing tree from its sub-trees is useful in any situation where there is a tree structure being built. For example, in family tree diagrams built with the geneologytree package.
\def vs \newcommand
As mentioned earlier, \def and \newcommand are both ways to define macros. Plain TeX uses \def whereas LaTeX can also use \newcommand.
One of the differences between the two is that \newcommand will give error if we retry to redefine a pre-existing macro (got to use \renewcommand for that), whereas \def will simply overwrite the pre-existing definition.
The no-questions-asked rewrite behaviour of \def can cause confusion, especially larger code base..
Acknowledgement
Before realizing macros could be used to compose sub-trees into trees, I had set out trying to make a LaTeX package for it. I had made some progress getting familiar with expl3 and had actually made parts of such a package. Then I was able to attend TUG'25, which at Trivandrum this year. I talked to Boris Veytsman about my need and it was him who suggested using macros. Thanks Boris!
Thanks also to TUG for funding my TUG'25 expenses.