Method of and Device for Verifying a Mathmatical Proof

The invention relates to a method of verifying a mathematical proof which is formulated in a typed higher-order language. The fact that a language is a typed higher-order language means that it contains typed terms and that so-called higher-order constructs are used. The language is chosen because it is better suited to the normal mathematical formulations than the so-called first order languages. The latter languages are more frequently used because of their simple structure, but have less power of expression due to limitations to the constructs to be used. An example of such a typed higher-order language and its use is described in L. S. van Benthem Jutting, Checking Landau's "Grundlagen" in the Automath System, Mathematical Centre Tracts, Vol. 83, Amsterdam, 1979. A typed higher-order language is a logic language which is composed of terms, categories of terms being: types, expressions, "ordinary" terms, proofs, propositions, abbreviations, being names for respective other terms; in this respect a variety of categories of terms is permissible. The expression of a term may be, for example a constant, a variable or a function. The terms are linked by constructors indicating relationships between terms. Constructors can indicate arithmetical operations, logic operations, implications and so on. Such a language can be used in order to formulate a mathematical proof, where each of the various parts of the proof is given a name and is included in a hierarchical structure of parts of each time higher order until a name of highest order is given. Such a proof is then formulated in a sequence of lines, each line in the sequence being not lower in the hierarchy than all preceding lines in the sequence. This means: the later line is either higher in the hierarchy or no relationship exists between the two lines.

For the method of verifying a mathematical proof consisting of a number of sub-proofs it is necessary that the following requirements are satisfied for the successive assignment of the abbreviations or lines:

1. A series of verifications must be performed on the "lines";

2. Each "line" is influenced by an environment in which zero or more other "lines" are present which occupy a preceding position in the sequence and hence have a lower level in the hierarchy;

3. The result of the verification of a "line" is determined by all lines in the environment; it is not necessary for all such environmental lines to make also a material contribution to the determination thereof;

4. When all "lines" in the relevant environment are correct, the verification of the relevant line can be executed in a finite number of steps and offer the result "correct" or "error". The period of time required is also finite and depends on the processing speed.

5. However, when one or more "lines" in the relevant environment are not correct, a third result is feasible in that the number of steps required becomes infinitely large, notably because the verification process starts to circulate infinitely long in a loop. The verification of the proof in the sequence of the lines, therefore, always offers a correct answer within a finite period, but because of the large number of steps required this period of time is sometimes unacceptably long.

Among other things, it is an object of the invention to provide a method of accelerating the verification of a mathematical proof formulated in such a language, in which on the one hand the detection of an error is indicated to a user with absolute certainty without giving rise to an infinitely long duration of the method, while on the other hand the complexity remains limited. According to a first aspect, the object in accordance with the invention is achieved in that a method of verifying a mathematical proof formulated in a typed higher-order language is characterized in that the proof is formulated in a first sequence of lines, each line in the sequence not being lower in the hierarchy than any preceding line in the sequence, which method comprises the following steps:

during a distribution process successive sub-sequences of lines are formed from the first sequence of lines;

the distribution process each time assigns a next sub-sequence to an available verification process of a second series of verification processes for the purpose of verification, a verification process receiving not only a sub-sequence assigned thereto but also all preceding sub-sequences in order to abstract from said preceding sub-sequences the type definition of the names occurring in the assigned sub-sequence;

the series of verification processes execute the verifications, a positive verification resulting in a "ready" signal, a negative verification resulting in an "error" signal, and a non-interrupted verification providing neither a "ready" signal nor an "error" signal;

upon reception of an "error" signal, the distribution process delivers a stop signal to all verification processes, but upon reception of an adequate number of "ready" signals, it provides an "OK" signal to a user. The successive assignment of the sub-sequences in sequence to the verification processes must be performed so that, if no verification process is available, i.e. they are all busy, a sequence of consecutive sub-sequences is being processed: thus, no sub-sequence has been skipped. When this condition is satisfied, it is not strictly necessary to adhere to the assignment sequence at the level of the sub-sequence; however, at the level of the series of verification processes it must be maintained.

The invention also relates to a multiprocessor device for executing the method.

Further aspects are recited in the dependent Claims.

The invention will be described in detail hereinafter with reference to some Figures:

FIG. 1 shows a distribution diagram of a device in accordance with the invention;

FIG. 2 shows a diagram illustrating the communication between some processes.

FIG. 3 is Table A, which illustrates the operation of a distribution process.

FIG. 4 is Table B, which illustrates two communication operations of a distribution process;

FIG. 5 is Table C, which illustrates the operation of a verification process.

The description will first explain the Automath system, and subsequently an implementation on a tree structure of stations.

The Automath system will be explained hereinafter. The invention can also be used in an environment of other languages satisfying the same requirements, for example the "Nuprl" system (R. L. Constable et al, Implementing mathematics with the Nuprl proof development System, Englewood Cliffs, 1986). A text in the Automath language consists of a number of lines, each line of the form: C*N:=a:T

Therein, -C- is a set of terms which may, therefore, be empty; this is the set of variables and assumptions, including the one indicating that the type of -a-: type (a)=T. The elements of C are parameters of N. When N is to be used subsequently, these parameters should be inserted. The asterisk separates the assumptions from the remainder of the line.

Furthermore, -N- is a name or abbreviation for the more complex term a, each line introducing a new name N: N can be considered to be a standard proof of an axioma T, a constant of the type T, or a constructor for forming other terms. The use of N as a constructor enables an arbitrary constructor to be defined.

The indication -a- can represent a term, a type, a proposition or a proof of a proposition. If -a- exists, therefore, the abbreviation N can be used. Lines can be used without using -a-, for example, as an introduction of axiomas, constants or variables. A line can thus use a variety of information defined in preceding lines. The described mechanism operates as a compact formulation facility for a and T. A line in the Automath language can thus be considered to be a tableau line: the context C is a series of assumptions; the indication -a- is a term or a proposition, the indication -T- represents the type of -a- or the proposition for which -a- is the proof. The line is correct if the type of -a- is indeed equal to -T-. Tableau lines are described in the article Z. Manna and R. Waldinger, A deductive approach to Program Synthesis, ACM Trans. on Programming Languages and Systems, Vol. 2, (1980), pp. 90-92.

The environment of a line is composed of all preceding lines of which any abbreviation has been used, together with the environments of these preceding lines. The environment of the first line is empty. The text or the proof is correct when each line is correct in relation to its environment. A line -L- is correct if the term a defined in L has a type equal to T. In order to obtain a positive verification result, all lines in the environment themselves must be correct. A correct text in such a typed higher-order language thus represents a proof; the verification of this proof is executed as a series of checks as regards the correctness of a type.

The Automath system verifies proofs written in the Automath language (and analogously for other languages satisfying the cited requirements). A line is verified in that parts of the line are reformulated until the conclusion whether or not the part -a- has the type -T- can be directly drawn. The reformulation can be performed a number of times in succession, if necessary. Reformulation is realized by each time replacing an abbreviation by a usually more extensive representation thereof whose parts have a simpler structure and by transforming the expression obtained into an ordinary or standard form. A term is typed when two conditions are satisfied:

the term must be correctly formed: all constructors have enough, known arguments; variables must be real variables;

all abbreviations used in the construction of the term themselves are typed.

Therefore, a verification as regards typing first of all consists in a check of correct representation, and subsequently rewriting. However, if anywhere in the text a term -a- utilizes an abbreviation of a non-typed term, the rewriting of -a- may require an indefinite number of operations, and hence last an indefinite period of time. The following is an elementary example: assume that the following line occurs in an initial part of an Automath text:

.0.*a:=g(a): type;

therein, -.0.- is an empty set, -g- is a function, and the semicolon does not form part of the actual Automath text. Moreover, this line is incorrect. This error is verified during the sequential verification of the text, thus stopping the verification. In the case of distributed verification, this line is verified in a process other than further lines of the text which are, for example:

type (f)=a->b; the function space with originals in -a- is mapped in -b-;

type c=g(a);

to be proved: type f(c)=b;

in that case, it should actually be proved that

type (c)=a.

Using the knowledge of the first line mentioned, the latter could be expanded an indefinite number of times without giving rise to either correct verification or a distinct error:

type(c)=g(a);

type(c)=g(g(a)); etcetera.

The latter expansion can be blocked, but in a more complex environment it is often impracticable to render such blocking error-free.

FIG. 1 shows a distribution diagram of a preferred device in accordance with the invention. The device is constructed as a hierarchically organized multiprocessor system comprising the sub-processors 20, 22, 24, 26, 28, 30, 32. The first three sub-processors together constitute a distribution processor. The last four sub-processors constitute verification processors. The number of verification processors as well as the width and the depth of the tree of distribution processors are arbitrary per se. The text in the Automath language which is to be verified is received on connection 34. The sub-processor 22 emulates a verification processor vis-a-vis the sub-processor 20. The same holds good for all sub-processors which are lower in the hierarchy, each time vis-a-vis one sub-processor at a next-higher hierarchic level. The sub-processor 22 emulates a distribution processor vis-a-vis the sub-processors 26, 28. The same holds good for all sub-processors which are higher in the hierarchy with respect to a non-empty set of sub-processors at a next lower hierarchic level (if present). A sub-processor may itself be active in a multiprocess operation, for example when use is made of a time multiplex organization. In FIG. 1 each process is then represented by its own block: thus, a priori a given processor may accommodate a distribution process as well as a verification process. The foregoing limits the processing speed to be achieved with respect to a system comprising (even) more sub-processors.

When the sub-processor 20 has received the text, successive sub-sequences of lines are separated therefrom. A first sub-sequence is applied, for example to the sub-processor 22. A second sub-sequence is applied to the sub-processor 24, together with all preceding sub-sequences, so in this case only the first sub-sequence. It may be that no further sub-sequences remain; it may also occur that there is a further sub-sequence. The sub-processors 22, 24 serve to ensure the verification of the first sub-sequence and the verification of the second sub-sequence, respectively. Because they are not arranged at the lowest hierarchic level, they act in the same way as the sub-processor 20. Thus, they form sub-sequences of the second order for supply to the sub-processors 26, 28, 30, 32. Consequently, each of the latter processors receives its own sub-sequence of the second order, together with all preceding sub-sequences of the second or the first order. Furthermore, these four subprocessors are arranged at the lowest hierarchic level, so that they perform the actual verification. The completion of the verification of a sub-sequence is signalled to the next-higher level; thus, the supply of a next sub-sequence is implicitly requested, including further sub-sequences which are not to be verified but which occur previously in the text. Signalling continues as far as higher hierarchic levels until a further sub-sequence is available, which sub-sequence is then applied to the requesting sub-processor, or until no further sub-sequence is available at the highest hierarchic level; the verification is then at least partly complete. When the above request has been made by all sub-processors of the highest level but one without any further sub-sequence becoming available, the verification has been completed and successfully terminated. This is signalled to a user.

When an error is detected during any verification, this error is signalled to all other sub-processors and to the user, via the hierarchic structure, thus terminating the verification.

In this respect FIG. 2 shows an example of a diagram of the communication between a father process 40 and three son processes 42, 44, 46; in this context process and processor may be considered to be identical; the differences occur only at a lower level of the communication protocol.

Between the user (not shown) and the sub-processor of the highest hierarchic level 40 three messages occur:

sequence of lines: the user submits a verification request as regards a supplied sequence of lines;

error: the verification result is negative, possibly provided with a parameter indicating the first line where an error was found;

o.k.: the verification result is positive.

Between a further, arbitrary pair of sub-processors at two directly successive hierarchic levels the following messages occur:

a. transmitted by the higher sub-processor:

receive lines; this is a message containing a further sub-sequence of lines and, in as far as necessary, previous sub-sequences of lines of the Automath text;

stop; this is a message indicating that no further sub-sequences of lines are to be expected, so that in as far as the receiving sub-processor and any subordinate sub-processors are concerned, no further verification need be started; this does not mean that the latter sub-processors must have been stopped, and certainly not that the verification has thus been completed; it is a message which has relevance only for sub-processors which were already finished;

error; this is a message indicating that a verification operation has had a negative result; the latter message means that all sub-processors and subordinate sub-processors can terminate their operation.

b. transmitted by the lower sub-processor;

get new lines; this is a message representing a positive verification result and also a request for the supply of a new sub-sequence of lines for verification, including also any necessary previous sub-sequences in as far as they have not yet been supplied to the revelant sub-processor;

error; this is a message that a verification has had a negative result in any subaltern sub-processor vis-a-vis the revelant connection; this may be one of the sub-processors 42, 44, 46 shown, but also a sub-processor at a still lower hierarchic level; the error signal is thus communicated in the ascending as well as in the descending progression;

finished; this is a message which acts as an acknowledgement of the reception of the previously described "stop" message.

It is to be noted that the described message system represents one of various possibilities, that different aspects thereof can be used in any multiprocess situation in which tasks are subdivided in sub-tasks and the sub-tasks are sent to lower hierarchic levels, and that the present invention does not relate to such a message structure itself.

Table A shows the action of a distribution node. The lines of the action are numbered from 1 to 30. After the start, the variables are declared. Line 2 defines the set of the lines to be verified. Line 3 identifies the father process of the node, for the highest-level process it identifies the user. Line 4 identifies the (one or more) son processes of the node; these may be further distribution nodes or other verification nodes (a mixture is also possible). The father node, if present, is always a distribution node. Line 5 contains a variable varying over the set of sons. Line 6 defines a stop criterion having a binary value. Line 7 shows the reception of the set of lines to be verified, after which the variable S obtains the correct value. According to line 8 each of the son processes is assigned a sub-sequence of the lines to be verified. On line 9 the stop criterion is made false. On line 10 an iterative procedure is started which is terminated only when the stop criterion is true. Line 11 indicates that, when an error signal is received from a father process, all son processes receive an error signal. Line 12 shows that, when an error signal is received from one of the son processes, an error signal is applied to the father process and to all other son processes. The stop criterion is made true on both lines 11, 12. Line 13 states: if a request for the supply of further lines is received from a son process (meaning that the verification is finished, ultimately or not), a next procedure is executed. Line 14: if the set of lines not yet despatched for verification was (or has become) empty, a request for the supply of further lines is made to the father process on line 15. If an error indication is received from the father (line 16), an error message is despatched to all son processes and the stop criterion is locally made true. Line 17: if a sub-sequence of (further) lines is received from the father, this sub-sequence becomes the new set of lines to be verified and a sub-sequence of this set (this may possibly concern the entire remaing set) is assigned to the son process having made the request of line 13. When a stop signal is received from the father process (line 18), the stop criterion is locally made true and applied to the son process that had despatched the request of line 13. For as long as the set has not become empty, the assignment thereof to the son processes is continued. Line 20 is the pendant of the line 16; line 21 is the pendant of the line 13. Line 22 is the counterpart of the line 10. Line 23 illustrates what happens when the condition of line 10 is no longer applicable: the stop criterion has become true (lines 11, 12, 16, 18). For all son processes the following operation is then performed. Line 24: when an error signal is received from the father process, this signal is applied to all son processes. Line 25: when an error signal is received from a son process, this signal is applied to the father process and to all other son processes. When a request for further lines (line 26) is received from a son, a stop signal is applied to this son. When a "ready" signal is received from a son, the set of son processes considered is reduced by this particular son process. When all sons have been dealt with (line 28), a "ready" signal is applied to the father process (line 29), and the execution is terminated (line 30).

Table B shows two communication operations of a distribution process. The first operation is the actual distribution procedure for lines to be verified as stated on the lines 8, 17 in Table A. First a variable S1 is defined, being a sub-set of the set of all lines to be verified. On line 3 this variable is defined as a non-empty sub-set consisting of an initial sequence of lines of the lines to be verified. On line 4 a message representing the set S1 is applied to the son S. On line 5 a new main set, i.e. the remaining lines of the set S, is updated. Line 6 signals the end of the procedure. It is to be noted that the magnitude of the set S1 must be selected on the basis of the actual situation.

Line 7 shows the procedure "distribute error" of the lines 11, 12, 16, 24, 25 in Table A. Line 8 illustrates the action of this procedure: for a current value of s, each time the son having the rank number s receives the error message. Line 9 signals the end of the procedure.

If the distribution process were situated at the highest hierarchic level in the above case, all communication with the hierarchically next-higher distribution process would be dispensed with. In Table A this concerns the following lines: line 3 (instead a signalling "highest level" can take place); line 7 (this can be replaced by signalling the sequence of lines received from the user); line 9 (not applicable); line 15; line 16; line 17 (it is assumed that the sequence of lines to be verified is received in one operation); line 18 (actually, the entire procedure of the lines 14-20 can be formulated more compactly, as follows: supply sub-sequences until the set of lines still to be verified has become empty); line 24; line 29. The lines 7, 25, 29 represent the user interface described with reference to FIG. 2.

Table C illustrates a preferred version of the execution of a verification process. After the start on line 1, the following variables are declared: on line 2 the set of all lines to be verified; on line 3 the father process of the verification node (for example, in the form of an address or identification); on line 4 the boolean already mentioned stop criterion; on line 5 a boolean error message which becomes true when error has been found. Lines 6, 7 render these two variables false. On line 8 a loop commences, which loop is continuously repeated until the stop criterion becomes true. When an error message is received from the father process (line 9), the booleans of lines 4, 5 are both made true. When a stop message is received from the father process (line 10), the stop message is locally made true. When a subsequence of lines is received from the father (line 11), the sequence of lines to be verified is locally made equal to this (sub) sequence received. Lines 12, 13 define the actual verification process: for as long as no error is found, the verification process continue for a finite period of time. The fact that this period of time is finite indeed is not imposed by the contents of the lines 12, 13, but by the structure of the distribution between the processors and the distribution of an error message, if any. The assignment of the subsequences in the correct sequence (this holds good for each distribution process separately) to the son processes (verification processes or subaltern distribution processes) ensures the correctness in a sense that only a finite number of steps will be required for the verification. Line 14 corresponds to line 9. Line 15 starts a procedure in response to the local detection of a negative verification result: an error message is despatched to the father process; moreover, the error message is locally made true; furthermore, the stop message is locally made true. Line 19 terminates the latter procedure. Line 20 terminates the action of line 12. Line 21 terminates the action of line 11. Line 22 indicates that the process, after completion of a sub-task, requests the supply of a new sub-sequence of lines. Line 23 terminates the action of line 8. Line 24 indicates that, if there are no further lines to be verified and the error message is still false, the ready signal is applied to the father. Line 25 terminates the action.