MATH formulas in
PARagraph mode
Typesetting Inference Rules

Didier Rémy

(Version 1.4.0, last modified 15/02/2020)

Abstract: This package provides macros for displaying lists of formulas that are typeset in mixed horizontal and vertical modes. The package is two-folded.

The first part is an environment mathpar that generalizes the math display mode to allow several formulas on the same line, and several lines in the same display. The arrangement of the sequence of formulas into lines is automatic depending on the line width and on a minimum inter-formula space and line width alike words in a paragraphs (in centerline mode). A typical application is displaying a set of type inference rules.

The second par is a macro inferrule to typeset inference rules themselves. Here again, both premises and conclusions are presented as list of formulas that should be displayed in almost the same way, except that the width is not fixed in advance; and the inference rule should use no more width than necessary so that other inference rules are given a chance to appear on the same line.

Although mathpar and inferrule look similar in their specification, and are often used in combination, they are in fact completely different in their implementations.

1  License

Mathpartir is Copyright (C) 2001, 2002, 2003, 2005, 2015 INRIA. Mathpartir has been developed by Didier Rémy. Mathpartir is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2, or (at your option) any later version. See the GNU General Public License for more details (http://pauillac.inria.fr/~remy/license/GPL). Mathpartir is distributed in the hope that it will be useful, but without any warranty.

2  The mathpar environment

The mathpar environment is a “paragraph mode for formulas”. It allows to typeset long list of formulas putting as many as possible on the same line:

\begin{mathpar} A-Formula \and Longer-Formula \and And \and The-Last-One \end{mathpar}
AFormula 
LongerFormula
And 
TheLastOne

Formulas are separated by \and (or equivalently by a blank line). To enforce a vertical break it suffices to replace \and by \\.

The implementation of mathpar entirely relies on the paragraph mode for text. It starts a new paragraph, and a math formula within a paragraph, after adjusting the spacing and penalties for breaks. Then, it simply binds \and to something like \goodbreak.

Since version 1.5.0, the environment mathpar reduces the vertical skip using TEX variable \abovedisplayshortskip instead of \abovedisplayskip when the first line of the display is short enough not to overlap with the last line before the display:

one 
two
three
four
five 

This is to be compared with

one
two
three

which would overlap with the previous line. This behavior is automatic. Currently, it can be canceled with \shortmathparfalse, in case of a problem with the new behavior. However, there should be no reason to do so and this options may be removed in the future.

An alternative environment mathparpagebreakable allows for page breaks in the middle of the display. This cancels the previous optimisation for short displays.

3  The inferrule macro

The inferrule macro is designed to typeset inference rules. It should only1 be used in math mode (or display math mode).

The basic use of the rule is

\inferrule
  {one \\ two \\ three \\ or \\ more \\ premisses}
  {and \\ any \\ number \\ of \\ conclusions \\ as \\ well}

This is the rendering on a large page

one           two           three           or           more           premises
and           any           number           of           conclusions           as           well

However, the same formula on a narrower page will automatically be typeset like that:

one           two           three           or           more           premises
and           any           number           of           conclusions           as           well

An inference rule is mainly composed of a premise and a conclusion. The premise and the conclusions are both list of formulas where the elements are separated by \\.

Note the asymmetry between typesetting of the premises and of conclusions where lines closer to the center are fit first.

A newline can be forced by adding an empty line \\\\

\inferrule {aa \\\\ bb} {dd \\ ee \\ ff}
aa                   bb
dd           ee           ff

3.1  Single rules

Single rules are the default mode. Rules are aligned on their fraction bar, as illustrated below:

aa           bb
ee
      
aa                    bb           ee
ee

If the premise or the conclusion is empty, then the fraction bar is not typeset and the premise or the conclusion is centered (when both of them are empty, which does not make sense, we substitute them by question marks with a warning):

\inferrule {}{aa} + \inferrule {aa \\\\ aa}{} + \inferrule {}{}
aa
+
aa                    aa
+

Use use { } instead of {} to get an axiom for instance:

\inferrule { }{aa} + \inferrule {aa}{ }
 
aa
+
aa
 

The macro \inferrule accepts a label as optional argument, which will be typeset on the top left corner of the rule:

\inferrule [yop] {aa \\ bb} {cc}
Yop
aa           bb
cc

See section ?? for changing typesetting of labels. A label can also be placed next to the rule directly, since the rule is centered:

\inferrule {aa \\ bb} {cc} \quad (\textsc {Yop})
aa           bb
cc
   (Yop)

3.2  Customizing presentation

By default, lines are centered in inference rules. However, this can be changed by either \mprset{flushleft} or \mprset{center}. For instance,

$$\mprset{flushleft} \inferrule {a \\ bbb \\\\ ccc \\ dd} {dd \\ ee \\ ff}$$
  @percent 0.45@percent
a           bb            ccc           dddd
e           ff           gg

Note that lines are aligned independently in the premise and the conclusion, which are both themselves centered. In particular, left alignment will not affect a single-line premise or conclusion.

3.3  Customizing rules

One may wish to change use rules for rewriting rule or implications, etc. There is a generic way of definition new rules by providing three parts: a tail, a body, and a head. The rule will then be built by joining all three components in this order and filling the body with leaders to extend as much as necessary. Here are examples

$$\mprset{fraction={===}} \inferrule {a \\ bbb} {cc}$$
a           bbb
cc
$$\mprset {fraction={\models=\Rightarrow}} \inferrule {a \\ bbb} {cc}$$
a           bbb
cc

The height and depth of the body are used to adjust vertical space. One, may “smash” the body to reduce the vertical space

$$\mprset {fraction={% {\scriptstyle\vdash}% {\smash-}% {\rightarrow\!\!}% }} \inferrule {a \\ bbb} {cc}\,\,$$
a           bbb
cc
$$\mprset {fraction={\cdot\cdots\cdot}} \inferrule {a \\ bbb} {cc}$$
a           bbb
cc

Since vertical skip does not take header and footer into account, which is usually better but sometimes odd, this can be adjusted explicitly:

$$\mprset {fraction={|=/}, fractionaboveskip=0.6ex, fractionbelowskip=0.4ex} \inferrule {a \\ bbb_{\downarrow}} {cc^{\T\uparrow}}$$
a           bbb
cc

Finally, it is also possible to provide its own definition of fraction by

\def \Over #1#2{\hbox{$#1 \over #2$}} $$\mprset{myfraction=\Over} \inferrule {a \\ bbb} {cc}$$
a           bbb
cc

Customizing the horizontal skip between premises

(default value is 2em).

$$\mprset {sep=6em} \inferrule {a \\ bbb} {cc}$$
 
a           bbb
cc

Customizing the vertical space between premises

(default value is empty). Notice that leaving it empty and setting vskip to 0em is not quite equivalent as show below between the third and fourth rules (because the typesetting cannot use the primitive typesetting of fractions).

$$\def\R{\inferrule {aa\\aa\\\\bbb\\bbb} {cc} \hspace{3em}} \R \mprset{vskip=0ex}\R \mprset{vskip=1ex}\R$$
aa           aa                     bbb           bbb
cc
     
aa           aa                     bbb           bbb
cc
     
aa           aa                     bbb           bbb
cc
     
aa           aa                     bbb           bbb
cc
   

3.4  Tabulars in inference rules

Although you probably do not want to do that, you may still use tabular, array or minipage environments inside inference rules, but between braces, as follows:

\infer [Tabular-Rule] {some \\ math \\ and \\ {\begin{tabular}[b]{|l|r|} \hline Ugly & and \\[1ex]\hline table & text \\\hline \end{tabular}} \\ {\begin{minipage}[b]{6em} Do you really wish to do that? \end{minipage}} \\ } {some \\ conclusions}
Tabular-Rule
some          math          and         
Uglyand
tabletext
         
Do you really wish to do that? 
          
some          conclusions

3.5  Derivation trees

To help writing cascades of rules forming a derivation tree, inference rules can also be aligned on their bottom line. For this, we use the star-version:

\inferrule* {\inferrule* {aa \\ bb}{cc} \\ dd} {ee}
aa           bb
cc
          dd
ee

The star version can also take an optional argument, but with a different semantics. The optional argument is parsed by the keyval package, so as to offer a set of record-like options:

keyargEffect
beforetexExecute tex before typesetting the rule. Useful for instance to change the maximal width of the rule.
widthdSet the width of the rule to d
narrowerdSet the width of the rule to d times \hsize.
labPut label ℓ on the top of the rule as with the non-start version.
Labsame as lab
leftPut label ℓ on the left of the rule
LeftIdem, but as if label ℓ had zero width.
RightAs Left, but on the right of the rule.
rightAs left, but on the right of the rule.
leftskipdCheat by (skip negative space) d on the left side.
rightskipdCheat by d on the right side of the rule.
vdotsdRaise the rule by d and insert vertical dots.

We remind at the end the global options that we’ve seen above that can also be set locally in derivation trees:

 
sepdSet the separation between premises and conclusions to s.
flushleftflush premises to the left hand side
centercenter premises on each line.
rewrited 
myfractiontexset fraction to tex command
fractionlmrset fraction pattern to lm...mr with leaders.
vskipdSet the vertical skip between premises and conclusions to h.
vcenter Make the rule centered around the fraction line as the non-star version

Here is an example of a complex derivation:

Foo 
a           a                    bb           cc           dd Bar
ee 

          ff           gg
 hh
         
XX
uu           vv
ww
 (when n > 0)
(1) 

and its code

\inferrule* [left=Total,rightstyle=\em,right={(when $n > 0$)}] {\inferrule* [Left=Foo] {\inferrule* [Right=Bar,rightstyle=\bf, leftskip=2em,rightskip=vdots=1.5em] {a \\ a \\\\ bb \\ cc \\ dd} {ee} \\ ff \\ gg} {hh} \\ \inferrule* [lab=XX]{uu \\ vv}{ww}} {(1)}

3.6  Label styles

The package uses \DefTirNameStyle, \LabTirNameStyle, \LeftTirNameStyle, and \RightTirNameStyle to typeset labels introduced with the default option, Lab-, Left-, or Right-, respectively (or their uncapitalized variants). This can safely be redefined by the user. \DefTirName is normally used for defining occurrences (i.e. in rule \inferrule) while the three other forms are used for referencing names (i.e. in the star-version). The styles can also be redefined using labeled-arguments of the star-version of \inferrule as described in table below.

Instead of just changing the style, the whole typesetting of labels may be changed by redefining the commands \DefTirName, \LabTirName, \LeftTirName, and \RightTirName, each of which receives the label to be typeset as argument.

Notice, that if the package hyperref is loader, one can automatically attach hypertarget to rule definitions names of rules defined with the non-star version of \inferrule and refers to them by \RefTirName defined as follows:

\renewcommand{\DefTirName}[1]{\hypertarget{#1}{\TirName {#1}}}
\newcommand{\RefTirName}[1]{\hyperlink{#1}{\TirName {#1}}}
keyargEffect
styletexset the default style for labels to tex
leftstyletexidem for labels
rightstyletexidem for right labels

3.7  Star v.s. non-star version

The package also defines \infer as a shortcut for \inferrule but only if it is not previously defined.

There are two differences between the plain and star versions of \inferrule. The plain version centers the rule on the fraction line, while the star one centers the rule on the last conclusion, so as to be used in derivation trees.

Another difference is that the optional argument of the plain version is a label to always be placed on top of the rule, while the ∗-version takes a record of arguments. Hence, it can be parameterized in many more ways.

One may recover the plain version from the star version by passing the extra argument vcenter as illustrated below (the base line is aligned with the dotted line):

⋯⋯ ⋯⋯
aa  aa                    aa           bb
cc           cc                    dd
⋯⋯ ⋯⋯
aa  aa                    aa           bb
cc           cc                    dd
⋯⋯ ⋯⋯

This is convenient, for instance to typeset rules with side conditions and keep them attached to the rule:

aa            aa if n>0
cc 
aa            aa if n<0
cc 

Or differently,

if n>0
aaa            aaa
cc
if n<0
aaa            aaa
cc

3.8  Triple rules

There is also a version \triplerule originally design to print Hoare triples as rules, which will be rendered as follows, horizontally aligning rules at their bottom horizontal rule line.

Hoare
ppppp            pppp           pppp
mmm           mmm           mm
ccccc           cccc
Rule
ppppp            pppp           pppp
mmm           mmm
ccccc          


         top 
         bot


The first rule typeset as follows (in an environment where \hsize is 8em to folow its typesetting on several lines).

\triplerule[Hoare] {ppppp \\ pppp \\ pppp} {mmm \\ mmm \\ mm} {ccccc \\ cccc}

Here is the code for the second rule

\triplerule[Rule] {ppppp \\ pppp \\ pppp} {mmm \\ mmm} {ccccc \\ {\left(\begin{array}{c} top \cr bot \end{array}\right)} } }

Notice that the array environment is surrounded by braces, as explaned in section §??.

3.9  Implementation

The main macro in the implementation of inference rules is the one that either premises and conclusions. The macros uses two box-registers one hbox for typesetting each line and one vbox for collecting lines. The premise appears as a list with \\ as separator. Each element is considered in turn typeset in a hbox in display math mode. Its width is compare to the space left on the current line. If the box would not fit, the current horizontal line is transferred to the vertical box and emptied. Then, the current formula can safely be added to the horizontal line (if it does not fit, nothing can be done). When moved to the vertical list, lines are aligned on their center (as if their left-part was a left overlapped). At the end the vbox is readjusted on the right.

This description works for conclusions. For premises, the elements used to be processes in reverse order and the vertical list is simply built upside down, which was annoying when using counters in the premises. This has recently been fixed, with a quite different implementation. In case of problem, the old behavoir can be recovered by calling \MprRecoverOlderVerPremise.

For example,

\newcount \clab \newcommand {\lab}[1] {\global\advance \clab by 1\relax (\the\clab)} \infer [New] {\lab A \\ \lab B} {\lab C \\ \lab D}

produces:

    
New behavior
 by 1 ()                     by 1 ()            by 1 ()
 by 1 ()           by 1 ()            by 1 ()
0  
Old behavior
 by 1 ()                     by 1 ()            by 1 ()
 by 1 ()           by 1 ()            by 1 ()

4  Other Options for the mathpar environment

The vertical space in mathpar is adjusted by \MathparLineskip. To restore the normal paragraph parameters in mathpar mode (for instance for some inner paragraph), use the command \MathparNormalpar. The environment uses \MathparBindings to rebind \\, and, and \par. You can redefine thus command to change the default bindings or add your own.

5  Examples

See the source of this documentation —the file mathpartir.tex— for full examples.

6  HEVEA compatibility

The package also redefines \hva to do nothing in mathpar environment and nor in inference rules.

In HeVeA, \and will always produce a vertical break in mathpar environment; to obtain a horizontal break, use \hva \and instead. Conversely, \\ will always produce a horizontal break in type inference rules; to obtain a vertical break, use \hva \\ instead.

For instance, by default the following code,

\begin{mathpar} \inferrule* [Left=Foo]{}{} \inferrule* [Left=Foo] {\inferrule* [Right=Bar,width=8em, leftskip=2em,rightskip=2em,vdots=1.5em] {a \\ a \\ bb \\ cc \\ dd} {ee} \\ ff \\ gg} {hh} \and \inferrule* [lab=XX]{uu \\ vv}{ww} \end{mathpar}

which typesets in TEX as follows,

Foo 
a           a           bb           cc           dd Bar
ee 

          ff           gg
 hh
XX
uu           vv
ww

would appear as follows with the compatible HEVEA mode:

Foo 
a           a           bb           cc           dd Bar
ee 
          ff           gg
 hh
XX
uu           vv
ww

To obtain (almost) the same rendering as in TEX, it could be typed as

\begin{mathpar} \inferrule* [Left=Foo] {\inferrule* [Right=Bar,width=8em, leftskip=2em,rightskip=2em,vdots=1.5em] {a \\ a \hva \\ bb \\ cc \\ dd} {ee} \\ ff \\ gg} {hh} \hva \and \inferrule* [lab=XX]{uu \\ vv}{ww} \end{mathpar}

Actually, it would be typeset and follows with the compatible HEVEA mode:

      
Foo 
a           a                    bb           cc           dd Bar
ee 
          ff           gg
 hh
  
XX
uu           vv
ww

1
Even though the basic version may work in text mode, we discourage its use in text mode; the star-version cannot be used in text-mode

This document was translated from LATEX by HEVEA.