Modernized LCF: The Logic of Goals and Tactics.

Here, I present a judgemental reconstruction of LCF-style tactic systems, called Modernized LCF, which admits various extensions including validations (checkable certificates). The purpose is to present the structure and meaning of refinement proof directly as a logical theory with a meaning explanation, in contrast to the standard practice of taking refinement proof as an extra-logical “finishing touch”.

A logical theory is given by a species of judgements \(\mathbf{J}\); such a theory is explained intuitionistically by assigning each \(J\in\mathbf{J}\) a meaning explanation, which states the the conditions under \(J\) may become evident to the knowing subject. Formally, though, in order to build a refinement logic for this theory, we fix a basis of inference rules \(\mathbf{R}\) which are valid according to the meaning explanation.

The naïve way to specify the species \(\mathbf{R}\) is to say that it consists in pairs of judgements with vectors of judgements (i.e. \(\mathbf{R}\subseteq\mathbf{J}\times\mathbf{J}^\star\)), where a rule \(R\equiv{\langle J, \vec{J}\rangle}\) is one with a conclusion \(J\) and premises \(\vec{J}\). This, however, is too fine-grained, and does not permit a finitary presentation of the refinement rules for a logical theory.

In Modernized LCF, we specify that \(\mathbf{R}\) is a species of objects such that for each \(R\in\mathbf{R}\), there is a unique \({[R]}\in\mathbf{J}\rightharpoonup\mathbf{J}\star\), i.e. each rule shall correspond to a partial function from judgements (conclusions) to vectors of judgements (premises). Then, for a logical theory \({\langle \mathbf{J}, \mathbf{R}\rangle}\), we shall define a logic of refinement proof, by incrementally adding more structure.

the meaning of goals

The first concept relating to refinement proof that we shall explain is that of goals, using the judgement \({{{\color{MidnightBlue}{u}}}\ \mathit{goal}}\); we do not explain this judgement by listing the formal rules for its evidence, but rather we follow Martin-Löf and Pfenning in propounding its meaning explanation, and then showing how certain rules are evident under those semantics.

To know \({{{\color{MidnightBlue}{u}}}\ \mathit{goal}}\) is to know how to apply an arbitrary rule \(R\in\mathbf{R}\) to \(u\), and if it is applicable, to know the subgoals \(\vec{v}\) generated by this application.

Now, for each judgement \(J\in\mathbf{J}\), the assertion of \({{{\color{MidnightBlue}{J}}}\ \mathit{goal}}\) is clearly justified. Fix \(R\in\mathbf{R}\); then, if \({{{\color{MidnightBlue}{{[R]}(J)}}}\equiv{{\color{Maroon}{\vec{J}}}}}\), we say that \(R\) was applicable, yielding subgoals \(\vec{J}\). The evidence that we have given for \({{{\color{MidnightBlue}{J}}}\ \mathit{goal}}\) is well-founded by induction on the length of the vector \(\vec{J}\). QED

Note that whilst we have fixed the species of judgements \(\mathbf{J}\), the meaning explanation that we have given for goals is open-ended; it may be that at a later time, we discover a new kind of goal which is not merely a judgement of the underlying logical theory. (In a later post, I will propose just this!)

the meaning of tactics

The next concept to be explained is that of tactics; the definition will proceed by analogy with the open-ended explanation of goals, introducing the new form of judgement \({{{\color{MidnightBlue}{\tau}}}\ \mathit{tac}}\).

To know \({{{\color{MidnightBlue}{\tau}}}\ \mathit{tac}}\) is to know, for any goal \(u\), whether \(\tau\) is applicable to \(u\), and if it is, what subgoals it generates.

Think carefully about the above meaning explanation before proceeding! The program of Modernized LCF is to enrich the closed collections of judgements and rules into open-ended categories1. The way this is done, informally, is to say that a goal is anything that behaves like a judgement with respect to arbitrary rules, and that a tactic is anything that behaves like a rule with respect to arbitrary goals.

In the same way that we convinced ourselves that each judgement is a goal, we shall also cause it to become evident that \({{{\color{MidnightBlue}{R}}}\ \mathit{tac}}\) for any \(R\in\mathbf{R}\). Let’s remind ourselves of what we’re trying to know:

For any goal \(u\), whether \(R\in\mathbf{R}\) is applicable to \(u\), and if it is, what subgoals it generates.

But, by inverting the meaning explanation of \({{{\color{MidnightBlue}{u}}}\ \mathit{goal}}\), we already know how to apply an arbitrary rule \(R'\in\mathbf{R}\) to \(u\), and if it is applicable, the subgoals \(\vec{v}\) generated by this application. QED

It is now that we may begin adding the standard menagerie of LCF tacticals to our theory, by showing that they respect the meaning explanation. In particular, here are the additional (meta-)rules that we wish to make evident:

\[ {\dfrac{\matrix{}}{{{{\color{MidnightBlue}{{\mathsf{id}}}}}\ \mathit{tac}}}} \qquad {\dfrac{\matrix{}}{{{{\color{MidnightBlue}{{\mathsf{fail}}}}}\ \mathit{tac}}}} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{\tau_1}}}\ \mathit{tac}} & {{{\color{MidnightBlue}{\tau_2}}}\ \mathit{tac}} }}{ {{{\color{MidnightBlue}{{\tau_1;\tau_2}}}}\ \mathit{tac}} }} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{\tau_1}}}\ \mathit{tac}} & {{{\color{MidnightBlue}{\tau_2}}}\ \mathit{tac}} }}{ {{{\color{MidnightBlue}{{\tau_1\mid\tau_2}}}}\ \mathit{tac}} }} \]

We know that \({{{\color{MidnightBlue}{{\mathsf{id}}}}}\ \mathit{tac}}\), because we shall say that \({\mathsf{id}}\) is applicable to any goal \(u\), yielding subgoals \({\langle u\rangle}\). Likewise, \({{{\color{MidnightBlue}{{\mathsf{fail}}}}}\ \mathit{tac}}\) because \({\mathsf{fail}}\) is not applicable to any goal. We also know \({{{\color{MidnightBlue}{{\tau_1;\tau_2}}}}\ \mathit{tac}}\) for tactics \(\tau_1,\tau_2\), since the sequencing is applicable whenever \(\tau_2\) is applicable to all the subgoals of \(\tau_1\), yielding the union of the subgoals generated by \(\tau_2\) in each case. Other tacticals may be explained as well, but we need not do so now, since the open meaning explanation allows new tacticals to be defined at any time.

Finally, based on the judgements that we have given so far, we introduce a last form of judgement, \({{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{\tau}}}\Rightarrow{{\color{Maroon}{\vec{v}}}}}\):

To know \({{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{\tau}}}\Rightarrow{{\color{Maroon}{\vec{v}}}}}\) (presupposing \({{{\color{MidnightBlue}{u}}}\ \mathit{goal}}\), \({{{\color{MidnightBlue}{\tau}}}\ \mathit{tac}}\), and \({{{\color{MidnightBlue}{v}}}\ \mathit{goal}}\) for each \(v\) in \(\vec{v}\)) is to know that \(\tau\) is applicable to \(u\), yielding subgoals \(\vec{v}\).

Now, the notation of this judgement is meant to be suggestive, since it is possible to assign a preorder structure to goals, such that goals constitute a kind of frame, and familiar monotonicity properties hold. I will go into this idea in a later post.

The meaning of this judgement validates the following rules, defined in mutual recursion with an auxiliary judgement form \({{{\color{MidnightBlue}{\vec{u}}}}\Vdash^\star{{\color{MidnightBlue}{\tau}}}\Rightarrow{{\color{Maroon}{\vec{v}}}}}\):

\[ {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{R}}}\Rightarrow{{\color{Maroon}{\vec{v}}}}} }}{ {{{\color{MidnightBlue}{{[R]}(u)}}}\equiv{{\color{Maroon}{\vec{v}}}}} }} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{\tau_1}}}\Rightarrow{{\color{Maroon}{\vec{v}}}}} }}{ {{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{{\tau_1\mid\tau_2}}}}\Rightarrow{{\color{Maroon}{\vec{v}}}}} }} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{\tau_2}}}\Rightarrow{{\color{Maroon}{\vec{v}}}}} }}{ {{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{{\tau_1\mid\tau_2}}}}\Rightarrow{{\color{Maroon}{\vec{v}}}}} }}\\[18pt] {\dfrac{\matrix{ }}{ {{{\color{MidnightBlue}{\cdot}}}\Vdash^\star{{\color{MidnightBlue}{\tau}}}\Rightarrow{{\color{Maroon}{\cdot}}}} }} \qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{\vec{u}}}}\Vdash^\star{{\color{MidnightBlue}{\tau}}}\Rightarrow{{\color{Maroon}{\vec{w}_1}}}} & {{{\color{MidnightBlue}{v}}}\Vdash{{\color{MidnightBlue}{\tau}}}\Rightarrow{{\color{Maroon}{\vec{w}_2}}}} }}{ {{{\color{MidnightBlue}{\vec{u},v}}}\Vdash^\star{{\color{MidnightBlue}{\tau}}}\Rightarrow{{\color{Maroon}{\vec{w}_1,\vec{w}_2}}}} }}\\[18pt] {\dfrac{\matrix{ {{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{\tau_1}}}\Rightarrow{{\color{Maroon}{\vec{v}}}}} & {{{\color{MidnightBlue}{\vec{v}}}}\Vdash^\star{{\color{MidnightBlue}{\tau_2}}}\Rightarrow{{\color{Maroon}{\vec{w}}}}} }}{ {{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{{\tau_1;\tau_2}}}}\Rightarrow{{\color{Maroon}{\vec{v}, \vec{w}}}}} }}\\[18pt] {\dfrac{\matrix{ }}{ {{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{{\mathsf{id}}}}}\Rightarrow{{\color{Maroon}{u}}}} }} \]

As an exercise, define the n-ary sequencing tactical \({\tau;[\vec{\tau}]}\) such that it yields a valid tactic under the meaning explanation propounded here.

Conclusions and Further Directions

One immediate extension would be to consider a proof-term assignment to the logic of goals and tactics, which corresponds to the extension of LCF to LCF with validations.

There are also a number of other plausible extensions which present themselves. We have only considered the goals which correspond directly with the judgements \(J\in\mathbf{J}\) of our underlying logical theory. It should be possible to enrich the structure of goals with a free Heyting algebra, e.g. where at the meet of goals \(u\land v\), a tactic must be applicable to both goals, yielding the union of the subgoals generated in each case.

If goals were endowed with a suitable preorder, it would also be conceivable to introduce “modalities” on tactics, validating a rule like the following: \[ {\dfrac{\matrix{ {\vert_{{{\color{MidnightBlue}{u}}}}\, {{{{\color{MidnightBlue}{u}}}\Vdash{{\color{MidnightBlue}{\tau}}}\Rightarrow{{\color{Maroon}{\vec{w}}}}}\ \ ({{{\color{MidnightBlue}{u}}}\leq{{\color{MidnightBlue}{v}}}})}} }}{ {{{\color{MidnightBlue}{v}}}\Vdash{{\color{MidnightBlue}{\square\,\tau}}}\Rightarrow{{\color{Maroon}{\vec{w}}}}} }} \]

To my mind, the open-ended meaning explanations for goals and tactics in Modernized LCF clarify the design space for proof refinement logics, and offer a number of interesting directions for further research. This post is based on joint work with Darin Morrison.

  1. Following Martin-Löf, I mean “category” in the philosophical sense, not in the category-theoretic sense.