Producing Inference Rules With irtex
irtex.py
Some lab assignments in this course include a file irtex.py. This Python script inputs a data file of a particular format (which we name “IRF” for “inference rule formatting”) and generates LaTeX. The purpose of this data file is to make inference rules and proofs more readable in source code form but still allow them to be formatted nicely in LaTeX so that they are readable in their traditional form as well.
You probably will not call this script yourself. Instead, your lab assignment will call this script from within its Makefile; that is, when you run make, this script will run and convert a file in your lab assignment into LaTeX for you. The starter code in the lab will include the generated output in your assignment .tex file; all you need to do is use the appropriate command to place the generated LaTeX in the right place in your assignment.
The .irf File Format By Example
irtex.py takes an .irf file as input. This file must be formatted in a specific way in order for irtex.py to generate LaTeX from it. The .irf file format is indentation-sensitive (similar to Python) and describes tree-like structures. Each line (or similarly-indented group of lines) is a node in the tree; further-indented lines are children of previous lines. At the top level, each tree represents either a single rule or a single proof.
Axioms
Consider the following .irf syntax for the F♭ Value Rule.
rule Value
axiom
v \Rightarrow v
This snippet starts with the keyword rule followed by the name we give to the rule. This name must be alphabetic because LaTeX cannot define commands with numbers in their names. The snippet creates a LaTeX macro \ruleValue which we can use to typeset the rule in our document. The next line must be indented and contains the keyword axiom to indicate that this is an axiomatic rule. Under axiom, we have an indented line containing the conclusion of our axiom; this line is LaTeX code. We can use this rule in LaTeX like so:
\begin{mathpar}
\ruleValue
\end{mathpar}
This will show something like the following output:
\[ {\textrm{V}\scriptsize\textrm{ALUE}}\; \dfrac{ }{v \Rightarrow v} \]
Non-Axiomatic Rules
Rules with premises can be written in a similar intuitive fashion. Consider the following .irf syntax for a variation of the F♭ Or Rule
rule Or
if
e_1 \Rightarrow \texttt{False}
and
e_2 \Rightarrow \texttt{False}
then
e_1 \texttt{ Or } e_2 \Rightarrow \texttt{False}
As above, the rule starts with the keyword rule and is followed by a rule name; this snippet creates the LaTeX macro \ruleOr which can be used to show the rule. If we view this text as a tree, the if, and, and then lines represent three children of the rule line. These children must be named in this fashion: if is the text of the first child, then is the text of the last child, and all other children are named and. Each of those children carries indented LaTeX code used to represent it in the rule. The last (then) LaTeX is used as the conclusion of the rule; the others are used as the premises. If we write the LaTeX
\begin{mathpar}
\ruleOr
\end{mathpar}
it will show something like
\[ {\textrm{O}\scriptsize\textrm{R}}\; \dfrac{e_1 \Rightarrow \texttt{False} \qquad e_2 \Rightarrow \texttt{False}}{e_1 \texttt{ Or } e_2 \Rightarrow \texttt{False}} \]
Proofs and Axioms
The .irf format can also be used to specify proof trees. Similar to rules, a proof begins with the keyword proof and is followed by a name for the proof; this name is used to name the LaTeX command. Following this keyword is a line of LaTeX code giving the conclusion of the proof. The remainder of the tree consists of the rest of the proof together with the rules which justify this conclusion.
As an example, consider the following .irf proof which uses the Value Rule as an axiom:
proof TrueIsTrue
\texttt{True} \Rightarrow \texttt{True}
axiomatically
The second line of this text is the LaTeX representing the conclusion of the proof. The third line justifies the conclusion by claiming that it is true from an axiom in our rules. (Since .irf is just a layout format, it’s not checking that this is true; it’s just producing LaTeX for us to see.)
Because this is a proof, its corresponding LaTeX command is \proofTrueIsTrue. That command would typeset as follows:
\[ \dfrac{ }{\texttt{True} \Rightarrow \texttt{True}} \]
Note that this is different from the \ruleValue macro above in that it is a use of the Value Rule, not a definition of it.
We might prefer to give the name of the axiom and have it appear in our proof. To do so, we change the third line which justifies our conclusion:
proof TrueIsTrue
\texttt{True} \Rightarrow \texttt{True}
by Value axiom
Here, by and axiom are keywords; the text appearing between them is used as the name of the axiom which justifies this conclusion. This typesets as:
\[ {\textrm{V}\scriptsize\textrm{ALUE}}\; \dfrac{ }{\texttt{True} \Rightarrow \texttt{True}} \]
Subproofs
Of course, most proofs are not simply uses of axioms: they use inductive rules which have premises which must also be proven. For instance, the expression True Or False evaluates to True, but the Or Rule requires that we prove evaluation for the two subexpressions. Instead of axiomatically or by Value axiom, we may instead give a series of justifications. For instance, the following .irf text will produce a proof of the evaluation of True Or False:
proof TrueAndFalseIsFalse
\texttt{True Or False} \Rightarrow \texttt{True}
because
\texttt{True} \Rightarrow \texttt{True}
axiomatically
and
\texttt{False} \Rightarrow \texttt{False}
axiomatically
The line because appears before the first subproof while the work and appears before each subsequent subproof. Indented under these words are the subproofs that we use to show the premises of the Or Rule. These subproofs use the same syntax as the axiomatic proof we showed above.
This produces a command \proofTrueAndFalseIsFalse which typesets as follows:
\[
\dfrac{
\dfrac{
}{
\texttt{True} \Rightarrow \texttt{True}
}
\qquad
\dfrac{
}{
\texttt{False} \Rightarrow \texttt{False}
}
}{
\texttt{True Or False} \Rightarrow \texttt{True}
}
\]
Of course, we might want to show the names of the rules used in this proof. We can use the by ... axiom form as mentioned above as well as a by ... because form in place of the because on the third line:
proof TrueAndFalseIsFalse
\texttt{True Or False} \Rightarrow \texttt{True}
by Or because
\texttt{True} \Rightarrow \texttt{True}
by Value axiom
and
\texttt{False} \Rightarrow \texttt{False}
by Value axiom
Using the above .irf snippet, we generate LaTeX code which produces the following result:
\[
{\textrm{O}\scriptsize\textrm{R}}\;
\dfrac{
{\textrm{V}\scriptsize\textrm{ALUE}}\;
\dfrac{
}{
\texttt{True} \Rightarrow \texttt{True}
}
\qquad
{\textrm{V}\scriptsize\textrm{ALUE}}\;
\dfrac{
}{
\texttt{False} \Rightarrow \texttt{False}
}
}{
\texttt{True Or False} \Rightarrow \texttt{True}
}
\]
A Deeper Proof
These subproofs may continue arbitrarily deep. Here is the .irf code for the evaluation of the expression True And (False Or (True And True)):
proof BooleanExpression
\texttt{True And (False Or (True And True))} \Rightarrow \texttt{True}
by And because
\texttt{True} \Rightarrow \texttt{True}
by Value axiom
and
\texttt{False Or (True And True)} \Rightarrow \texttt{False}
by Or because
\texttt{False} \Rightarrow \texttt{False}
by Value axiom
and
\texttt{True And True} \Rightarrow \texttt{True}
by And because
\texttt{True} \Rightarrow \texttt{True}
by Value axiom
and
\texttt{True} \Rightarrow \texttt{True}
by Value axiom
This in turn produces the following output:
\[
{\textrm{A}\scriptsize\textrm{ND}}\;
\dfrac{
{\textrm{V}\scriptsize\textrm{ALUE}}\;
\dfrac{
}{
\texttt{True} \Rightarrow \texttt{True}
}
\qquad
{\textrm{O}\scriptsize\textrm{R}}\;
\dfrac{
{\textrm{V}\scriptsize\textrm{ALUE}}\;
\dfrac{
}{
\texttt{False} \Rightarrow \texttt{False}
}
\qquad
{\textrm{A}\scriptsize\textrm{ND}}\;
\dfrac{
{\textrm{V}\scriptsize\textrm{ALUE}}\;
\dfrac{
}{
\texttt{True} \Rightarrow \texttt{True}
}
\qquad
{\textrm{V}\scriptsize\textrm{ALUE}}\;
\dfrac{
}{
\texttt{True} \Rightarrow \texttt{True}
}
}{
\texttt{True And True} \Rightarrow \texttt{True}
}
}{
\texttt{False Or (True And True)} \Rightarrow \texttt{True}
}
}{
\texttt{True And (False Or (True And True))} \Rightarrow \texttt{True}
}
\]
Incrementally Writing Proofs
The proofs in your document can get quite large and may become difficult to read. Although .irf is intended to make the source code of your proof easier to follow, it’s helpful to build your proof a little bit at a time. Instead of axiomatically, by ... axiom, because, or by ... because, you can write todo or TODO as a justification. This will highlight that the premise is unproven. For instance,
proof Example
\texttt{True And False} \Rightarrow \texttt{True}
todo
will generate something like
\[ \dfrac{ \textbf{TODO} }{ \texttt{True Or False} \Rightarrow \texttt{True} } \]
This is useful if you have written part of your proof and you want to see what it looks like in the final document before proceeding with the rest of your proof. It can also help you keep track of which claims you have not yet proven.
Multiple Commands
Multiple rules and proofs can appear in a single .irf file. You would ordinarily use a single .irf file for your lab assignment, though you are not required to do so. For instance, you may write
rule Value
axiom
v \Rightarrow v
rule Let
if
e_1 \Rightarrow v_1
and
e_2[v_1/x] \Rightarrow v_2
then
\texttt{Let }x\texttt{ = }e_1\texttt{ In }e_2 \Rightarrow v_2
to define both the \ruleValue and \ruleLet commands. You may then use these commands in the appropriate places in your LaTeX document to typeset the rules. You may do likewise with proofs: multiple proofs may appear in the same file and may appear alongside rules.
Comments and Blank Lines
Blank lines in .irf files are ignored; they have no impact regardless of spaces. Lines with # as the first non-space character are comments and are also ignored. If # appears elsewhere on a line, it is treated as a normal character and not as a comment.