In the study of logic a distinction is made between the logic being studied, the object language, and the language in which the study of the logic is conducted, the metalanguage . In our case the object language is the type theory . Thus far in this book we have conducted the discussion of using a combination of English and mathematics as an informal metalanguage. In this chapter we introduce a formal metalanguage based upon the ML programming language [Gordon, Milner, & Wadsworth 79].
In ML the various parts of the object language---terms, declarations, proofs and rules---are data types. By defining a formal metalanguage we have made concrete the structure and elements of the object language. We can then write ML programs that manipulate objects of the object language. Thus, for example, we can write a program to return the subterms of a term or one that substitutes a term for a free variable in a term. More importantly, we can write ML functions which search for or transform proofs. We can then use such automated proof techniques and theorem--proving heuristics, tactics , while writing proofs.
A tactic is a function written in ML which partially
automates the process
of theorem proving in Nuprl
. In any logic writing a formal proof is a
combination of insightful, interesting steps and tedious ones. Being
required to fill in every detail of a proof distracts one's attention from
the important parts of the proof and can be quite tiresome. The
refinement logic of Nuprl
is no exception to this. Given undecidability, we
cannot hope to fully automate the theorem--proving process. Ideally, then, we
would want the user to enter only the central ideas of a proof and
leave the details to be filled in by the system. Tactics offer a mechanism
whereby a sketch of a proof supplied by the user can often be completed
automatically and many simple proofs can be avoided altogether. Tactics
can also be used to automate more difficult patterns of proofs that occur
frequently so that essentially the same argument need not be repeated;
a tactic for that pattern of proof would be invoked
instead. The uses of tactics are many and need not be restricted to the
above. There is the potential in the tactic mechanism to express any
decision procedure, semidecision procedure or theorem--proving algorithm
which is valid in the Nuprl
logic.
As will be explained in detail below, the implementation of the
metalanguage makes sure that all proofs produced by tactics are
in fact valid
proofs. This makes it impossible to write
or use a tactic that produces an incorrect proof.
In there are predefined tactics that are always available. These include tactics of general use in theorem proving. The user can easily add new tactics that extend the predefined tactics or are specific to the domain of theorems being proved. The next two sections describe two different kinds of tactics: refinement tactics and transformation tactics. This is followed by an introduction to the ML programming language and an explanation of writing simple tactics. Chapter 9 contains a more detailed description of the metalanguage interface and information on writing tactics and examples of more complicated tactics.