Proofnetify: Draw Proof-nets in LaTeX

UPDATE: Fixed a bug that prevented latex from finding the .mps files. Also have now added linlog.sty to the tarball.

After struggling mightily with xypic and other TeX friendly diagram tools I decided that drawing linear logic proof nets was too difficult. I wrote a small tool to do it for me. It's quite limited but hopefully someone will find it useful. It should work on any sane unix system (including Mac OS X), but will probably fail spectacularly on windows.

What you need

The tool is a bit of a hotchpotch of different stuff. You will need the following:

• LaTeX (actually TeX will do, but you will need to reconfigure some stuff); the diagrams won't appear in DVI files so you need either pdflatex or dvips aswell.
• Metapost; should be supplied with your TeX distribution. If not try TeTex. The command to invoke metapost must be mpost otherwise it won't work. This is a bug. Workaround: make an alias.
• Perl: should be /usr/bin/perl
• OCaml.
• Optional: by default proofnetify uses linlog.sty to provide linear logic symbols. I recommend this in general but you don't need it. It seems to have disappeared from the web so I'll mirror it here.

With the possible exception of ocaml most unix systems will have all that stuff already.

The toolkit

There are three files you need:

• proofnets.sty : use this package in your latex sources; make sure it's on you TEXINPUTS path.
• proofnetify : a perl script
• proofnetinator : an ocaml bytecode program

If you have any problems with the ocaml code you probably need to recompile it. Here is a tarball of the complete source, including the other two files, and a makefile.

Usage

In your latex source put the command:

  \usepackage{proofnets}

in your document preamble. To draw a proof-net use the command

  \proofnet{formulae}{links}

where links is a comma separated list of pairs of number like so:

  (1,3),(2,4),(5,6)

and formulae is comma separated list of formulae subject to some constraints:

• Atoms must be upper case latin letters, optionally with superscripts. The superscripts are limited to latex macros without arguments or the character "*".
• Only binary connectives are allowed. These are also restricted to latex macros without arguments.
• Bracket defensively using "(" and ")".

For example:

\proofnet{A\TIMES A,A^\lNEG\PAR A^\lNEG}{(1,4),(2,3)}

generates the proofnet:

The restriction to nullary latex macros is a limitation of the parser. It can be worked around by defining macros for whatever you want. For example, define \newcommand{\cut}{\text{CUT}} and then you can use \cut in your proof-nets. If you place these definitions in you metapost preamble (see later) latex will never see them so you won't pollute your document's namespace.

Once you're finished editing the .tex file do

proofnetify yourfile.tex

to generate the diagrams, and then run latex as usual. As mentioned earlier, the diagrams won't appear in the dvi file so you'll need to use dvips or pdflatex to see them.

Here is an example tex file, and here is the pdf output from it.

Some Caveats:

• \proofnet{...}{...} must be the only thing on its line in the latex file. No white space before or after, no comments, nada. Otherwise proofnetify won't see the proof-net. This is a bug.
• I don't count \{ and \} among the nullary latex macros for the purposes of defining formulae. If you use them the parser will become confused and things will go wrong.
• The diagrams are produced by METAPOST which normally expects to see TeX not latex. You need to set the environment variable $TEX to your local latex (usually just "latex", even if you are using pdflatex).
• If you find the diagram are not quite right, you'll have a metapost file xxxx_pn.mp where xxxx is your original tex file. You can edit this file to get them just so. However when you run metapost on it you will get a bunch of files called xxxx_pn.y where y is the diagram number. You will need to rename these to xxxx_pny.mps otherwise latex won't find your modified diagrams.
• If you haven't finished editing your file when you proofnetify I recommend unproofnetifying it using the -u option before doing anymore editing. This is to protect the rather brittle changes that proofnetify will make to your file. This is essential in the case where you put in a new diagram after proofnetifying: in this case the new diagram will overwrite the old.

Options

-q

quiet mode. Supresses most output; but not from Metapost.

-v

verbose mode. doesn't supress output. This is the default.

-u

undo mode. Restores the tex file to the state it was in before you ran proofnetify, assuming you didn't edit inside its changes...

-h file

use file as metapost premable. If you are using latex it is essential that this file contains the following:

verbatimtex
\documentclass{article}

\begin{document}
etex

This provides the latex environment your diagrams will be rendered in. If you want other packages then include them between the \documentclass and \begindocument as usual. If this argument is not supplied proofnetify will use a default preamble including linlog.sty. If you don't have that package you will to supply your own header file.

-f file

use file as metapost postamble. Usually not needed. If you do supply one it must include the following:

verbatimtex
\end{document}
etex
end

Future Features:

• Unary links
• More robust parser
• Make the case of (1,3),(2,4) a bit prettier
• slices?

I hope some one will find this program useful. At the moment it only handles the MLL case really, but that should change soon. Any questions bug reports etc email to rwd@comlab.ox.ac.uk