New Implementation of Mark2
Here is the SML source of the new
implementation.
Facilities of the old implementation which are not present in the new
but which are seldom if ever used at present are user-defined
precedence and the "functional programming" features (these features
have since been added, but are still not often used).. A major aim of
the reimplementation is the installation of a more efficient system
for keeping track of different kinds of dependencies, which, it is
hoped, will allow reaxiomatization, redefinition, and theorem export
facilities to be made usable in practice (this has now been put into
practice for forget and theorem export)
The files for the new version are mirrored in my home directory at the
University of Idaho: the source is "design", the executable is "Watson",
and all the .wat files below are found there, and the corresponding
saved theory files (with extension .sav.wat) have been built there. I
plan to rebuild these each time I upgrade the executable significantly.
The new version is functionally similar but not identical to the current
implementation. There follows a list detailing points of difference:
- dependencies: The prover displays dependencies
in a Mark2 term format as a list. The last element of the list will
be 0, which I use by convention as a list terminator. Dependencies of
0 signal no dependencies on axioms at all. The new version only
records dependencies on axioms which have actually been applied;
embedded theorems in tactics do not induce dependencies, so many
tactics which have extensive dependencies under the old version have
none under this version (but applying the tactic does induce
dependencies as expected). The restriction on the "reprove" command
that it not add dependencies has been removed.
- more dependencies: The prover now records definition
dependencies and "theorem text dependencies". A theorem acquires a theorem
text dependency on another theorem when it calls the other theorem as
a tactic, for example. These dependencies can be viewed by using a
new command "showalldeps" which takes the name of a theorem as a parameter;
normally the prover will only display axiomatic dependencies. It does
now remove superfluous dependencies on definitions, a feature which I
had to remove from the old prover because it caused serious performance
problems.
- strict prefix operators: Although the
overloading of infixes as prefixes with "invisible" left subterms is
still supported, the prover now allows (and takes as the default) the
declaration of strict prefix operators, which have no right subterm.
- case expressions: Case expressions no longer
have an immediate right subterm; you can look at the apparent right
subterm, but you can't do anything to it.
- structural tactics: Since a term like ?x^+?y
does not match a strict prefix expression or a case expression,
structural tactics like LEFT, RIGHT and EVERYWHERE need to be
implemented with cases. RIGHT doesn't work at all anymore on case
expressions; new tactics LEFT_CASE and RIGHT_CASE are provided to
apply theorems to the left and right subterms of the "virtual" right
subterm of a case expression. This is already implemented in
the script structural2.mk2 below.
- more on case expressions: Hypotheses of the
forms true = ?p and ?p (where ?p is not an equation) are now
indistinguishable to the prover, and the tactic interpreter will
convert any hypothesis of the form true=?p to ?p. This has the
further effect that case expressions with the hypotheses true=true
and true=false are automatically collapsed in the same way that
case expressions with hypotheses true and false were already.
- new variables: When the new prover introduces new
variables, it does not necessarily apply the same index to them (this
is just as likely to be caused by rewrites of commonly used tactics).
Also, this prover is less likely to present a new variable as a function
applied to a bound variable.
- special navigation commands: The commands
upto,downtoleft, downtoright, and the dlls family do not have precisely the
same behavior. I have yet to find a script where this made a difference.
One advantage is that the upto command can now be repeated; it does not
check the term where you are.
- alternative rule infixes: Alternative theorem
applications are now represented in a different way. The effect of the
altruleintro and altrevruleintro commands is intended to be the same,
but the appearance of the resulting embedded theorem will be different.
- on-success rule infixes: These infixes (*>, <*) have the
order of their arguments reversed. I don't think that any users other
than myself have used these, but they are found in structural and
typestuff scripts. The change of order was made to bring them
into analogy with the new alternative infixes.
- synthetic abstraction: Synthetic abstraction is
no longer supported. Operators (prefixes or infixes) beginning with a
colon are now free to be used like any other operator.
- error messages: Error messages are generally
more informative.
- saved theory files: These have the extension .sav.wat
and are entirely different in format from the saved theory files of the old
version. These saved theory files are actually scripts. The load and
save facilities are a little slower than the old prover's load and save.
Save files now include additional information, such as what scripts have
been run!
- views and theorem export: The July 1 version
supports theorem export. Use commands declareview x (creates a view
named x which translates predeclared objects to themselves), addtoview
x y z (causes view x to translate y to z) to construct a view.
Generally, setting up a correspondence between axioms will do the
trick (the prover matches axioms to extend views as needed); an
exception exists for operator variables, which do need to be
associated with operator variables in the target theory by the view.
The command "exportthm view target suffix thm" will, if run in the
source theory where theorem thm lives, translate thm and all the
theorems it depends on (if it is a tactic, for example) using the view
"view", and prove these in the remote theory "target" (which needs to
exist on the desktop); the argument "suffix" is used to generate new
theorem names where needed to avoid name collisions. Views are not
saved, but the view and exportthm commands are supported in scripts.
The exportthm command is still rather unstable and may do odd things.
It is, however, reasonably fast!
Find here a Postscript file for the
paper/documentation under construction.
Here are the Watson scripts. Be aware
that Watson and the last release of Mark2 are not perfectly compatible;
scripts to be run with the last release of Mark2 are found below.
Here is the new Watson page
Here is the old Mark2 page.