This system has a strong, and non-accidental resemblance to the system
for mechanising proofs in Higher Order Logic, HOL. But whereas HOL is a
system for proving mathematical theorems, whose domain of interpretation is
a universe of infinite sets, and, which, in particular, treats each
lambda-expression as denoting a mathematical function, our system deals
with the result of evaluating expressions in SML *restricted to the
functional subset of ML*.

As compared with the work of Boyer and Moore, we are providing a proof-checker, not a proof-finder. However, we would anticipate that it would be possible to incorporate HOL-style conversions, tactics and tacticals to ease the process of generating proofs.

As a consequence of our domain being SML, our proof rules are weaker
than those of HOL. For example, HOL contains a proof rule that allows the
user unconditionally to create the theorem ` |- t = t`
for any well-typed term

So, for example, if `fact` is the factorial function as usually
defined, ` fact = fact ` is not well-typed, and so ` |-
fact=fact` is not admissable as a theorem of our system;
neither is
`fact n = fact n` unconditionally valid in our system,
for it is not the case that the evaluation of ` fact n ` will
terminate normally for a negative integer argument.
In fact, the appropriate theorem
is ` 0<=n |- fact n = fact n `

The prover is implemented in MetaSML [Sheard...] which is derived from SML
by providing a quasi-quotation mechanism. If *e* is an SML
expression of type *t*, then *<e>* is a MetaSML expression
of type *<t>*. Thus the angle brackets `<...>` act to
support a form of quotation, which resembles quasi-quotation in Scheme in
that there is a local escape mechanism, using the tilde operator.

Note that MetaSML's handling of variables that are free in an expression but bound in the environment in which the expression was created avoids a variable capture problem arising from a sequence like the following:

fun twice x = 2*x; (* code to create a theorem about twice *) fun twice f = f(f x) (* code which uses the earlier theorems about twice in the context of the new definition. *)We need to say something about e.g. the status of + in <3 + 4> I've used the term "name" - the "+" is the name of the addition function.

Given this repetoire of proof-rules, and given that a user has the ability to discover (but not change) the fine structure of theorems by using selector functions and patterns of MetaSML, it is possible to build systems which can partially automate the process of proof.

The logically significant components of the *theorem*
data-type are a list of *hypotheses* and a *conclusion*.
The data-type `theorem` might thus concretely be declared as

datatype theorem = Thm of <bool> list * <bool> list;Thus each hypothesis is a MetaSML term of type

H |- tfor the theorem

By a consonantly-typed environment for an expression is meant a mapping from variables to values whose domain includes the free variables of the expression and in which the image of each variable under the map belongs to the type ascribed to that variable by the SML type inference system.

Our proof rules will be sound if they can only generate theorems that satisfy the following data-invariant

We use the notation ` t _{1} ==> t_{2} ` as an abbreviation for

We adopt the HOL convention of capitalising the names of the MetaSML functions which implement proof rules.

For exposition it is convenient to adopt the usual notation for proof rules

thmwhich expresses the fact that_{1}, thm_{2}... thm_{n}______________________ thm

It is a consequence of our concept of soundness that we need more proof rules than HOL. This arises from the fact that the DISCH rule in HOL

g, H |- t ______________ H |- g ==> tis not sound in our system, for

In addition to the proof-rules
there is a set of *axioms* which are pre-created
theorems expressing basic facts about SML, for example that addition over
the `int` type is commutative.

fun halts t = true;Clearly, if we have a theorem

However, this treatment means that we may *not* apply the usual
rules of instantiation. For example, while for any variable `x`
there is a theorem ` |- halts x `, it is not permissable
to substitute an arbitrary expression for `x`. Otherwise, for
example, we could "prove"

|- halts(fact n)Thus, in particular, many of our proof-rules will require extra termination conditions as compared with HOL.

The following basic rules are sound for `halts`:

_____________ |- halts tprovided that

**Justification**
Having no free variables, `t` evaluates without exception in every
consonantly typed environment. From the definition of `halts`,
`halts t` evaluates to `true`. Hence ` halts t`
is universally valid, and so the rule is sound.

For example

HALTS_EVAL <2+3> = |- halts 2+3

_______________ |- halts vprovided that

**Justification**
Any environment whose domain includes `v` is consonantly typed, and
is an environment in which the evaluation of `v` terminates without
exception. From the definition of `halts`,
`halts t` evaluates to `true`. Hence `halts t`
is universally valid and so the rule is sound.

We use ` t _{1}[x:=t_{2}] ` to denote the term

t[xto denote the term_{1}..x_{n}:= a_{1}..a_{n}]

We use the concept of a path to identify a particular sub-expression of an expression.

type path = int list

We write `t[p]` to mean the sub-term of `t`
addressed by the path `p`.
We write `t[p:=t']` to mean the result of replacing the
sub-term of `t` addressed by the path `p` by `t'`.

We write `p[x _{1}..x_{n}]` to denote a pattern whose free variables are

Deduction in of our system could be treated by eliminating patterns from the discourse, translating everything into he lambda calculus. While this approach has the virtue of simplicity, it is achieved at the cost of moving the discourse significantly away form the source language, making it harder for the user to follow what is happening, and also making proofs longer.

There
are three possible cases which arise if we try to match a pattern
`p` against an expression `t`.

- There can never be a match
- There is always a match
- There is sometimes a match.

The idea of a match can then be expressed as

datatype match = Match of (< var > * < val > list) * <bool> listOur approach is thus to define a function

match :-> -> match option

fun BETA (x as <(fn #p => ~(f #p) | ~y) ~a>) = (case match p a of SOME sub => Thm([], < ~x = ~(f a) >) | NONE => BETA <~y ~a>) | BETA _ = error p : ('a,X) pattern f : X substitution -> <'b> match : ('a,'b) pattern -> <'a> -> 'b substitution y : <'a -> 'b>

This requires some care, since it is a consequence of our concept of
*validity* that a definition such as

fun double x = x*2;cannot in general be made into the theorem

|- double x = x*2since in general a function won't terminate. Instead, we introduce rules that allow a definition to be used directly in a proof. For the purposes of explication of the definitional rules, we write a definition

val v = tas

|-Since MetaSML keeps a firm hold on the scope of definitions, the following definitional-substitution rule preserves validity._{DEF}v = t

No problem is raised by recursive definitions. For example

fact 0 = 1 | fact n = n*fact(n-1)is converted into the definition

|-Here the occurrence of_{DEF}fact = fn 0 => 1 | n => n*fact(n-1)

fn...expression is not a free variable but is instead the name of the factorial function.

|-provided_{DEF}v = t , H |- t_{1}___________________________________ H |- t_{1}[p:=t]

As a MetaSML function,
we provide `DEF_RIGHT` with a path to the occurrence of a
name that is to be replaced by its definition, and a theorem in whose
conclusion the replacement is to be done.

In effect, DEF is unfolding the definition of `v`.

|-provided_{DEF}v = t , g,G |- t_{1}___________________________________ g[p:=t], H |- t_{1}

As a MetaSML function we provide DEF_LEFT with a path to the occurrence of a name that is to be replaced by its definition, and a theorem in whose first hypothesis the replacement is to be done.

In particular, we lose the reflexive rule of equality ( ` |- t = t
`). Instead, this has to be proved in every case. It is (perhaps
conditionally) true for combinations of the language primitives, but must
be proved for user-defined functions.

Moreover, the classical *reductio ad absurdam* rule
does not hold. From

not t |- falsewe cannot conclude

Thus we are much more constrained in moving terms from the hypotheses to the conclusions of theorems than we are in HOL. As a consequence, our proof-rules require us to operate on hypotheses as well as conclusions.

The following are our basic rules.

g_{0}...g_{i}...g_{n}|- t __________________________ g_{i},g_{0}...g_{i-1}g_{i+1}...g_{n}|- t

________ t |- t

The soundness of this rule depends upon the fact that our terms are restricted to the functional subset of SML, in which the value of an expression is determined solely by the constant objects (including function closures) embodied in it and by the values that its free variables have in the environment in which it is evaluated.

Hprovided the structural identity t[p] = t_{1}|- t_{1}= t_{1}' H |- t _________________________________________ H_{1}union H |- t[p:=t_{1}']

**Justification**

The first theorem expresses the fact in any environment in which each
expression in H_{1} evaluates to `true`, then t_{1} and
t_{1}' evaluate to equal values in the same environment. The second
theorem expresses the fact that in any environment in which each expression
in H evaluates to `true`, *t* also evaluates to
`true`.
The rule states that in any environment in which all the hypotheses in H_{1} and
H evaluate to `true`, the term *t* with an occurrence of
*t _{1}* replaced by

This rule expresses the fact that objects which SML judges to be equal
are indistinguishable by any SML program. It would not apply to a language
such as Scheme, where it is possible to distinguish between objects that
are structurally equivalent (using `equal?`) and those which are
identical (using `eq?`).

Hprovided t_{1}|- t_{1}= t_{1}' t_{2},G |- t_{3}_________________________________________ t_{2}[p:=t_{1}], H_{1}union H |- t_{3}

**Justification**
Similar to that for SUBST.

H |- t H' |- t' ___________________________ (H - t') union H' |- t

**Justification**
Suppose all the terms of

(H - t') union H'evaluate to

H |- t_{2}_________________________________________ halts t_{1}, (H - {t_{1}}) |- t_{1}==> t_{2}

**Justification**
The theorem `G |- t _{2} `
requires that in any environment in which all the expressions
of H evaluate to

Now suppose we have an environment in which all the expressions of

halts tevaluate to_{1}( H - {t_{1}} )

- t
_{1}evaluates to`true`: hence all the hypotheses in H also evaluate to`true`. Hence t_{2}also evaluates to`true`, and therefore`not`t_{1}`==>`t_{2}evaluates to`true`. - t
_{1}evaluates to`false`:`not t`evaluates to_{1}`true`, and hence by the short-circuit rule for the evaluation of`==>`, t_{1}==> t_{2}evaluates to`true`.

H_{1}|- t_{1}==> t_{2}, H_{2}|- t_{1}__________________________________ H_{1}union H_{2}|- t_{2}

**Justification**

In an environment in which all the expressions of H_{1} union H_{2} evaluate
to `true`, t_{1} will evaluate to `true`. In such an
environment,

thas the same value as t_{1}==> t_{2}

____________________________________________________________ halts tprovided_{2}|- (fn p[x_{1}..x_{n}] => t_{1}|f) t_{2}= t_{1}[x_{1}..x_{n}:= a_{1}..a_{n}]

match p t(that is the match is unconditionally successful)_{2}= SOME(Match([(x_{1},a_{1})..(x_{n},a_{n})],[]))

____________________________________________________________ halts tprovided_{2}|- (fn p[x_{1}..x_{n}] => t_{1}|f) t_{2}= f t_{2}

match p t(that is the match is unsuccessful)_{2}= NONE

____________________________________________________________ halts twhen_{2}, e_{1}...e_{m}|- (fn p[x_{1}..x_{n}] => t_{1}|f) t_{2}= t_{1}[x_{1}..x_{n}:= a_{1}..a_{n}], halts t_{2}, not(e_{1})...not(e_{m}) |- (fn p[x_{1}..x_{n}] => t_{1}|f) t_{2}= f t_{2}

match p t_{2}= SOME(Match([(x_{1},a_{1})..(x_{n},a_{n})],[ e_{1}...e_{m}]))

H |- t ___________________________ halts e, H[v:=e] |- t[v:=e]INSTANTIATE allows us to replace a free variable in a theorem by an expression. However we have to add the additional hypothesis that the evaluation of the expression halts.

**Justification:**

The input theorem says that for
any type-correct mapping from its free variables to values under which all
expressions of H evaluate to `true`, the expression `t` also
evaluates to `true`. Now suppose we have an environment rho under
which
the expression `e` terminates normally, so that `eval rho e`
is defined and

eval rho g[v:=e] = trueThen

eval rho g[v:=e] = eval rho[v:=eval e rho] g = truefor g in G. Hence

eval rho t[v:=e] = eval rho[v:=eval e rho] t = true

We will use axioms subject to the instantiate rule, which, as you will recall, introduces a halting requirement when an expression is substituted for a variable.

members of `int` form an abelian group

I1 |- x+y = y+x I2 |- x+(y+z) = (x+y)+z I3 |- x+0 = x I4 |- x+ (~x) = 0 I5 |- x-y = x+(~y)

members of `int` form an abelian semi-group

I6 |- x*y = y*x I7 |- x*(y*z) = (x*y)*z I8 |- x*1 = x

to complete the ring axioms we have

I9 |- x*(y+z) = x*y + x*z I10 |- x*0 = 0Note that I10 follows from the other axioms.

Note also that these ring axioms are *not* satisfied by any
implementation of SML, for each axiom states that a particular computation
will terminate normally. However, many implementations of SML will raise an
overflow exception when asked, for example, to multiply a million by a
million using integer arithmetic. Even implementations of SML such as
POPLOG SML will run out of heap in attempting to perform computations on
big enough integers.

Our system is complementary to the type-theory of SML. That is sound, but weak. Our system is, in the last analysis, only sound for a mathematically-ideal model of the language, but is logically much more powerful.

I11 x*y = 0 |- x=0 orelse y=0

I12 x<=y, y<=x |- x=y I13 |- x<=x I14 |- x<=y, y<=z |- x<=zAnd to obtain total order, we add:

I15 |- x<=y orelse y<=x I16 |- x<=x+1

However, working with user-defined natural numbers would be clumsy
notationally, so we prefer to treat them as a subset of `int`. With
this approach, the axiom of induction becomes:

INDUCTION_int : (<'a> -> bool) -> theorem -> theorem -> theorem;

H |- p 0 G, p(n) |- p(n+1) ________________________________________________ 0<=n, H |- p(n)It should be noted that this form admits non-standard models of the integers.

The list axioms are

|- halts(x::l) |- [] <> x::l WRONG!!! |- l = [] orelse l = hd(l)::tl(l) |- hd(x::l) = x |- tl(x::l) = l x_{1}::l1 = x2::l2 |- x_{1}=x2 x_{1}::l1 = x2::l2 |- l1=l2

H |- p [] H', p l |- p x::l ______________________________________ H union H' |- p lWhere

Ring(int)Neither can say, for example, that addition is commutative

commutative(op +)We could get round this problem by introducing the notion of a

fun commutative f g f(g 1, g 2) = f(g 2, g 1);

H |- t_{1}= t_{2}_____________________ H |- halts t_{1}

For f in { +,-,*,'<', '<=', '>', '>=',min,max,sign,sameSign,<> }

H_{1}|- halts(t_{1}) H_{2}halts(t_{2}) ______________________________________ H_{1}union H_{2}|- halts f(t_{1},t_{2})

H |- t_{2}<>0 H_{1}|- halts(t_{1}) H_{2}|- halts(t_{2}) _______________________________________________________ H union H_{1}union H_{2}|- halts t_{1}rem t_{2}

fun length [] = 0 | length(x::l) = 1 + length l;

halts length [] |- halts length [] ASSUME halts (fn [] => 0 | x::l => 1+length l) [] |- halts length [] LEFTDEF |- halts [] EVAL halts [] |- (fn [] => 0 | x::l => 1+length l) [] = 0 BETA |- (fn [] => 0 | x::l => 1+length l) [] = 0 MP halts 0 |- halts length [] SUBST_LEFT |- halts 0 EVAL |- halts length [] MPConcluding the base case.

halts(length(x::l)) |- halts(length(x::l)) ASSUME |- halts (x::l) AXIOM halts(x::l) |- (fn [] = 0 | x::l => 1+length l) (x::l) = 1+length l BETA |- (fn x::l => 1+length l) (x::l) = 1+length l MP halts (fn [] => 0 | (fn x::l => 1+length l) (x::l)) |- halts(length (x::l)) LEFTDEF halts(1 + length l) |- halts(length(x::l)) SUBST_LEFT |- halts 1 EVAL |- halts (1+y) SUBST halts length l |- halts length l ASSUME halts length l |- halts(1 + length l) SUBST halts l |- halts(length(x::l)) MP |- halts l INDUCE_LISTQuid Erat Demonstrandum

Proof:
Base Case. We must try and show that `halts([]@b)`. So let's
assume it, and see if we can rid ourselves of the hypothesis.

halts([]@b) |- halts([]@b) ASSUME (1)If we unfold the

halts(fn ([],b) => b | (a::l,b) => a::(l@b) ([],b) |- halts([]@b) DEF_LEFT (2) halts ([],b) |- fn ([],b) => b | (a::l,b) => a::(l@b) ([],b) = b BETA (3)So now we have to show that the expression

|- halts [] EVAL_HALTS (4) |- halts b HALTS_VAR (5) |- halts ([],b) HALTS_PAIR (6)We can now get rid of our halting condition by resolution with (3)

|- (fn ([],b) => b | (a::l,b) => a::(l@b)) ([],b) = b RESOLVE (7)So let's use this equation to simplify the hypothesis of (2).

halts b |- halts([]@b) SUBST_LEFT (8)And now we can trundle (5) into use, to obtain

|- halts([]@b) RESOLVE (9)Which concludes our base case.

**Inductive Step**

halts(x::l@b) |- halts(x::l@b) ASSUME (10) halts( (fn ([],b) => b | (a::l,b) => a::(l@b))(x::l,b)) |- halts(x::l@b) DEF_LEFT (11)And, as before, we'll apply BETA and get rid of the halting condition.

halts(x::l,b) |- (fn ([],b) => b | (a::l,b) => a::(l@b)) (x::l,b) = x::(l@b) BETA (12)But it's a rather more complicated halting condition. No matter, we can use the halting rules for cons and pair-creation.

|- halts x HALTS_VAR (13) |- halts l HALTS_VAR (14) |- halts (x::l) HALTS_CONS (15) |- halts b HALTS_VAR (16) |- halts (x::l,b) HALTS_PAIR (17)Whence, resolution with (12) gets us:

|- (fn ([],b) => b | (a::l,b) => a::(l@b)) (x::l,b) = x::(l@b) RESOLVE (18)We can now substitute back in (11), obtaining

halts(x::(l@b)) |- halts(x::l@b) SUBST_LEFT (19)And use the fact that list-construction halts

halts(l@b) |- halts(l@b) ASSUME (20) |- halts x HALTS_VAR (21) halts(l@b) |- halts(x::(l@b)) HALTS_CONS (22)Resolution now gains us what we need for structural induction:

halts(l@b) |- halts((x::l)@b) RESOLVE (23)So, finally, from induction on (9) and (23) we conclude:

|- halts(l@b) INDUCE_LIST (24)

Proof

halts([]@b) |- length([]@b) = length([]@b) SYMMETRIC (26)By resolution with (9) above

|- length([]@b) = length([]@b) REDUCE (27)Unfolding the right-hand call of

|- length([]@b) = length(fn ([],b) => b | (a::l,b) => a::(l@b)) ([],b)).... Theorem length l = 0 ==> l = [] Proof Base Case [] = [] length [] = 0 sorted a, sorted b |- sorted(merge a b) length(a) + length(b) = 0 |- a = [] |- length(a)>=0 length(a) + length(b) = 0 |- length a + length b = 0 a>c, b>=d |- a+b>c+d x+y = 0, x>=0, y>=0 |- x=0 x>=0 |- x=0 orelse x>0

Note that the *Abstraction* rule of HOL is not present in our
system, because it introduces equality between functions, and this is not
well typed in SML. We could introduce function-equality as a
meta-construct like `halts`, but since we can always express
*f=g* by saying that
*f x _{1}...x_{n} = g x_{1}...x_{n}*
we see no need to introduce this particular meta-construct.

The status of the INST_TYPE rule is not clear.

Using patterns would make life a lot easier.

bnd = matches patt arg, halts arg |- (fn patt => e | rest)arg = e[bnd]matches p1 e1 [] = b1, matches p2 e2 b1 = b2 |- matches p1::p2 e1::e2 b2