This section gives an overview of features of Nuprl which bear on the proposal. We explain the role of a typed language, comment on the foundational theories Nuprl supports, describe the tactic-style logic engine and the special editors and library mechanism.
working mathematics
The language of working mathematics is richly
typed, starting with the numerical types: natural numbers
, integers
, rationals
, reals
, and complex numbers
. Cartesian products consist of ordered pairs, as in
, pairs of
integers and naturals. Functions are typed according to the types of
their domain and range as in
, the type of mappings of
integers to rationals.
In its natural extent, this language includes non-numerical types
such as Propositions and in metamathematics there are types of
terms and formulas. The type Proofs is also sensible and
useful, and various combinations produce common notions such as propositional functions over the integers, say
Proposition.
types in programming and computer science
Types play a major role in most modern programming languages. We speak of the strong static typing of Java or polymorphic typing in ML. Classes and modules are also examples of types. The type system of a programming language such as ML bears a strong resemblance to the mathematical types discussed above.
need for rigorous type theory based educational material
Since the trend in mathematics is to appeal to the encoding of types
as sets, there is very little systematic treatment of types in
mathematics textbooks. Consequently, it is not as easy as it should
be to connect mathematics to programming problems which must be stated
in terms of programming language types. This is clear, for example,
even in looking at the definition of a tree or a graph. A typical
mathematics text will define a tree as a finite undirected graph in
which there are no circuits. A programming language like Pascal will
define it as a recursive data type, roughly speaking as:
If graphs are defined set theoretically, then one misses their
polymorphic nature. Leaf can be any type, and there is a long path
connecting a theorem on graphs to programs on trees.
Nuprl theories Nuprl 4 is a generic system in
the sense that it can support any logic whose axioms are expressible
in the type theory language. The present theory organization is a
core type theory with optional axioms. But the students will not
interact with the system at the level of axioms or inference rules.
In CS 572, the Formal Methods course using Nuprl, we never had to mention a
primitive rule. This is because users interact with the system at the
level of very high-level derived rules, decision procedures, and proof
building programs called tactics.
Tactics will be discussed in greater detail below, 2.2. But the basic idea is that tactics are programs that decompose proof goals into subgoals in such a way that if the subgoals are provable, then so is the goal. Indeed, users can generally see that if the subgoals are true, then so is the goal. So they operate at a semantic level with little or no concern for the basic rules. The important notion is the collection of tactics. We intend to base most of the interactive course material on a dozen general tactics. We will introduce them gradually and semantically. These play a large role in the course and in the system. For all practical purposes, the only logics we really support are those that the general tactics support.