File: mathpartir.tex

package info (click to toggle)
mathpartir 1.2.0-7
  • links: PTS, VCS
  • area: main
  • in suites: buster
  • size: 344 kB
  • sloc: makefile: 2
file content (568 lines) | stat: -rw-r--r-- 16,267 bytes parent folder | download | duplicates (5)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
%
%  Copyright (C) 2001, 2002, 2003, 2005 Didier Rmy
%
%  Author         : Didier Remy 
%  Version        : 1.2.0
%  Bug Reports    : to author
%  Web Site       : http://pauillac.inria.fr/~remy/latex/
% 
%  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.
%  
%  Mathpartir is distributed in the hope that it will be useful,
%  but WITHOUT ANY WARRANTY; without even the implied warranty of
%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%  GNU General Public License for more details 
%  (http://pauillac.inria.fr/~remy/license/GPL).
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  File mathpartir.tex (Documentation)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass {article}

\usepackage {mathpartir}
\usepackage {listings}
\usepackage {array}
\usepackage {url}
\newif \ifhevea 
%HEVEA \heveatrue
\ifhevea 
\usepackage {hevea}
\fi

\lstset {basicstyle=\tt}
\let \lst \verb

\title {
%HEVEA\begin{tabular}{>{\huge}c}
\textbf{MATH} formulas in \\ 
\textbf{PAR}ragraph mode\\[-1ex]
\ifhevea\else{}\hskip 0em\hbox to 12em {\hrulefill}\\\fi
%HEVEA\hline
\textbf Typesetting \textbf Inference \textbf Rules \\
%HEVEA\end{tabular}
}
\author {Didier R{\'{e}}my}
\date {(Version 1.2.0, last modified 20/12/2005)}


\begin{document}

\maketitle

\begin{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 \verb"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 \lst"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 \verb"mathpar" and \verb"inferrule" look similar in their
specification, and are often used in combination, they are in fact
completely different in their implementations.
\end{abstract}

\ifhevea
 \section {License}

Mathpartir is Copyright (C) 2001, 2002 INRIA.  Mathpartir has been developed
by Didier R{\'{e}}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 (\url{http://pauillac.inria.fr/~remy/license/GPL}).  Mathpartir is
distributed in the hope that it will be useful, but without any
warranty. 
\fi

\section {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{tabular}{m{0.45\hsize}m{0.45\hsize}}
\begin{lstlisting}{Ocaml}
\begin{mathpar}
A-Formula \and 
Longer-Formula \and 
And \and The-Last-One
\end{mathpar}
\end{lstlisting}
&
\begin{mathpar}
A-Formula 
\and
Longer-Formula
\and
And 
\and
The-Last-One
\end{mathpar}
\end{tabular}
$$
Formulas are separated by \verb"\and" (or equivalently by a blank line). 
To enforce a vertical break it sufficies to replace \verb"\and" by
\verb"\\". 

The implementation of \verb"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
\verb"\and" to something like \verb"\goodbreak". 

\section {The inferrule macro}

The inferrule macro is designed to typeset inference rules.  It should
only\footnote {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} be used in math mode (or display math mode). 

The basic use of the rule is 
\begin{verbatim}
\inferrule
  {one \\ two \\ three \\ or \\ more \\ premisses}
  {and \\ any \\ number \\ of \\ conclusions \\ as \\ well}
\end{verbatim}
This is the rendering on a large page
\def \one {\inferrule
  {one \\ two \\ three \\ or \\ more \\ premisses}
  {and \\ any \\ number \\ of \\ conclusions \\ as \\ well}
}
$$
\ifhevea \one
\else
\fbox {\vbox {\advance \hsize by -2\fboxsep \advance \hsize by -2\fboxrule
       \linewidth\hsize
        $$\one$$}}
\fi
$$
However, the same formula on a narrower page will automatically be typsetted
like that:
$$
\ifhevea \one
\else
\fbox {\hsize 0.33 \hsize \vbox {$$\one$$}}
\fi
$$
An inference rule is mainly composed of a premisse and a conclusion. 
The premisse and the conclusions are both list of formulas where the
elements are separated by \verb"\\". 

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

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

\begin{tabular}{m{0.44\hsize}m{0.44\hsize}}
\begin{lstlisting}{Ocaml}
\inferrule 
   {aa \\\\ bb}
   {dd \\ ee \\ ff}
\end{lstlisting}
&
$\inferrule {aa \\\\bb}{dd \\ ee \\ ff}$
\\
\end{tabular}

\subsection {Single rules}

Single rules are the default mode. 
Rules are aligned on their fraction bar, as illustrated below:
$$
\inferrule {aa \\ bb}{ee} \hspace {4em} \inferrule {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:
$$
\begin{tabular}{m{0.45\hsize}m{0.45\hsize}}
\begin{lstlisting}{Ocaml}
\inferrule {}{aa} + 
\inferrule {aa \\\\ aa}{}
\end{lstlisting}
&
$
\inferrule {}{aa} + 
\inferrule {aa \\\\ aa}{}
$
\\
\end{tabular}
$$
Use use \verb"{ }" instead of \verb"{}" to get an axiom for instance:
$$
\begin{tabular}{m{0.45\hsize}m{0.45\hsize}}
\begin{lstlisting}{Ocaml}
\inferrule { }{aa} + 
\inferrule {aa}{ }
\end{lstlisting}
&
\mbox {$
\inferrule { }{aa} + 
\inferrule {aa}{ }
$}
\\
\end{tabular}
$$

The macro \lst"\inferrule" acceps a label as optional argument, which will
be typeset on the top left corner of the rule: 
\par
\begin{tabular}{m{0.45\hsize}m{0.45\hsize}}
\begin{lstlisting}{Ocaml}
\inferrule [yop]
   {aa \\ bb}
   {cc}
\end{lstlisting}
&
$\inferrule [Yop]{aa \\ bb}{cc}$
\\
\end{tabular}
\par\noindent
See section~\ref {options} for changing typesetting of labels. 
A label can also be placed next to the rule directly, since the rule is
centered: 
\par
\begin{tabular}{m{0.45\hsize}m{0.45\hsize}}
\begin{lstlisting}{Ocaml}
\inferrule 
   {aa \\ bb}
   {cc}
\quad (\textsc {Yop})
\end{lstlisting}
&
$\inferrule{aa \\ bb}{cc} \quad (\textsc {Yop})$
\\
\end{tabular}

\subsection {Customizing presentation}

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

\begin{tabular}{m{0.44\hsize}m{0.44\hsize}}
\begin{lstlisting}{Ocaml}
$$\mprset{flushleft}
  \inferrule 
    {a \\ bbb \\\\ ccc \\ dd}
    {dd \\ ee \\ ff}$$ 
\end{lstlisting}
&
$$\mprset{flushleft} 
\hsize 0.45\hsize
\inferrule {a \\ bb  \\ ccc \\ dddd}{e \\ ff \\ gg}$$
\\
\end{tabular}

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

\subsection {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

\begin{tabular}{m{0.54\hsize}m{0.44\hsize}}
\begin{lstlisting}{Ocaml}
$$\mprset{fraction={===}}
  \inferrule {a \\ bbb} {cc}$$ 
\end{lstlisting}
&
$$\mprset{fraction={===}}
  \inferrule {a \\ bbb} {cc}$$ 

\\
\begin{lstlisting}{Ocaml}
$$\mprset
  {fraction={\models=\Rightarrow}}
 \inferrule {a \\ bbb} {cc}$$ 
\end{lstlisting}
&
$$\mprset
  {fraction={\models=\Rightarrow}}
  \inferrule {a \\ bbb} {cc}$$ 
\\
\end{tabular}
The height and depth of the \emph{body} are used to adjust vertical space. 
One, may ``smash'' the body to reduce the vertical space

\begin{tabular}{m{0.54\hsize}m{0.44\hsize}}
\begin{lstlisting}{Ocaml}
$$\mprset
  {fraction={%
      {\scriptstyle\vdash}%
      {\smash-}%
      {\rightarrow\!\!}%
      }}
 \inferrule {a \\ bbb} {cc}\,\,$$ 
\end{lstlisting}
&
$$\mprset
  {fraction={{\scriptstyle\vdash}{\smash-}{\rightarrow\!\!}}}
  \inferrule {a \\ bbb} {cc}$$ 
\\
\begin{lstlisting}{Ocaml}
$$\mprset
  {fraction={\cdot\cdots\cdot}
 \inferrule {a \\ bbb} {cc}$$ 
\end{lstlisting}
&
$$\mprset {fraction={{}{\,\smash\cdot\,}{}}}
  \inferrule {a \\ bbb} {cc}$$ 
\\
\end{tabular}
Finally, it is also possible to provide its own definition 
of fraction by

\begin{tabular}{m{0.54\hsize}m{0.44\hsize}}
\begin{lstlisting}{Ocaml}
\def \Over #1#2{\hbox{$#1 \over #2$}}
$$\mprset{myfraction=\Over}
  \inferrule {a \\ bbb} {cc}$$ 
\end{lstlisting}
&
\def \Over #1#2{\hbox{$#1 \over #2$}}
$$\mprset{myfraction=\Over}
  \inferrule {a \\ bbb} {cc}$$ 

\\
\end{tabular}






\subsection {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:
$$
\begin{tabular}{m{0.65\hsize}m{0.45\hsize}}
\begin{lstlisting}{Ocaml}
\inferrule*
   {\inferrule* {aa \\ bb}{cc}
    \\ dd}
   {ee}
\end{lstlisting}
&
$
\inferrule*
   {\inferrule* {aa \\ bb}{cc}
    \\ dd}
   {ee}
$
\\
\end{tabular}
$$
The star version can also take an optional argument, 
but with a different semantics. The optional argument is parsed by the 
\verb"keyval" package, so as to offer a set of record-like options: 
$$
\def \val {{\em v}}
\def \arraystretch {1.4}
\begin{tabular}{|>{\tt}c|p{0.7\hsize}|}
\hline
\bf key & \bf Effect for value {\val}
\\\hline\hline
before & Execute {\val} before typesetting the rule.
         Useful for instance to change the maximal width of the rule.
\\\hline
width &  Set the width of the rule to {\val}
\\\hline
narrower & Set the width of the rule to {\val} times \verb"\hsize".
\\\hline
left & Put a label {\val} on the left of the rule
\\\hline
Left & Idem, but as if the label had zero width. 
\\\hline
Right & As \verb"Left", but on  the right of the rule.
\\\hline
right & As \verb"left",  but on the right of the rule.
\\\hline
leftskip & Cheat by (skip negative space) {\val} on the left side.
\\\hline
rightskip & Cheat by {\val} on the right side of the rule.
\\\hline
vdots & Raise the rule by {\val} and insert vertical dots. 
\\\hline
\end{tabular}
$$
Here is an example of a complex derivation:
$$
\inferrule* [left=Total]
  {\inferrule* [Left=Foo]
     {\inferrule* [Right=Bar,
                       leftskip=2em,rightskip=2em,vdots=1.5em]
         {a \\ a \\\\ bb \\ cc \\ dd}
         {ee}
       \\ ff \\ gg}
     {hh}
  \\
  \inferrule* [lab=XX]{uu \\ vv}{ww}}
  {(1)}
$$
and its code
\begin{lstlisting}{Ocaml}
\inferrule* [left=Total]
  {\inferrule* [Left=Foo]
     {\inferrule* [Right=Bar,
                       leftskip=2em,rightskip=2em,vdots=1.5em]
         {a \\ a \\\\ bb \\ cc \\ dd}
         {ee}
       \\ ff \\ gg}
     {hh}
  \\
  \inferrule* [lab=XX]{uu \\ vv}{ww}}
  {(1)}
\end{lstlisting}

\def \L#1{\lower 0.4ex \hbox {#1}}
\def \R#1{\raise 0.4ex \hbox {#1}}
\def \hevea {H\L{E}\R{V}\L{E}A}
\def \hevea {$\mbox {H}\!_{\mbox {E}}\!\mbox {V}\!_{\mbox {E}}\!\mbox {A}$}

\subsection {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
\verb"hbox" for typesetting each line and one \verb"vbox" for collecting
lines. The premise appears as a list with
\verb"\\" as separator. Each element is considered in turn typeset in a
\verb"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 must be
processes in reverse order and the vertical list is simply built upside
down. 

\section {Other Options}

\label {options}

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

The package uses \verb"\TirName" and \verb"\RefTirName" to typeset labels,
which can safely be redefined by the user. The former is used for defining
occurrences ({\em ie.} in rule \lst"\inferrule") while the latter is used
for referencing ({\em ie.} in the star-version). 

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

\section {Examples}

See the source of this documentation ---the file \lst"mathpartir.tex"---
for full examples. 

\section {{\hevea} compatibility}

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

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

For instance, by default the following code,
\begin{lstlisting}{Ocaml}
\begin{mathpar}
\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}
\end{lstlisting}
which typesets in {\TeX} as follows,
\begin{mathpar}
\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}
would appear as follows with the compatible {\hevea} mode:
\begin{mathpar}
\inferrule* [left=Foo]
   {\inferrule* [right=Bar]
      {a \\ a \\ bb \\ cc \\ dd}
      {ee}
    \\ ff \\ gg}
   {hh}
\\
\inferrule* [lab=XX]{uu \\ vv}{ww}
\end{mathpar}
To obtain (almost) the same rendering as in {\TeX}, it could be typed as 
\begin{lstlisting}[escapechar=\%]{Ocaml}
\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}
\end{lstlisting}
Actually, it would be typeset and follows with the compatible {\hevea} mode:
\begin{mathpar}
\inferrule* [left=Foo]
   {\inferrule* [right=Bar]
      {a \\ a \\\\ bb \\ cc \\ dd}
      {ee}
    \\ ff \\ gg}
   {hh}
\and
\inferrule* [lab=XX]{uu \\ vv}{ww}
\end{mathpar}


\end{document}

\end{document}

% LocalWords:  mathpar aa Yop bb dd ee ff cc Ocaml Foo leftskip rightskip vdots
% LocalWords:  gg hh uu vv ww HeVeA escapechar