up

6. IMPLEMENTATION

We provide here a very brief outline of how we propose to implement a support environment using our foundation systems.

Combinators have been used in the implementation of functional programming languages [Tur79a,79b]. The algorithm for reducing combinators is also a proof tactic for theorems in our primitive logic. To prove a putative theorem in our logic, we simply evaluate it. If it evaluates to K. then it is a theorem, and by reversing all the reductions we obtain a proof.

The system used by Turner differs from our sample primitive logic. It does not attempt to reduce all computation to pure combinatory reduction. The combinators are used instead of more traditional methods of passing parameters by maintaining environments. In addition to pure combinators, a combinator graph may include data values from primitive value sets, and primitive operators on such values.

Furthermore, Turner uses more complex combinators than ours. His implementation would not otherwise be sufficiently efficient to be usable for any practical purpose. Even with these combinators and primitive operations combinator implementations of functional languages may be two orders of magnitude less efficient than fully compiled imperative languages.

More recent work on the implementation of combinator reduction systems has shown that the efficiency of implementation can be considerably improved by compiling combinators into machine code [Joh84]. We propose to use combinator graph reduction as an implementation technique for a formal methods development environment (without prejudice to the target execution environment).

In order to achieve reasonable efficiency we will make some adjustments to the primitive combinators to permit an efficient mapping onto the memory of a von-Neumann computer, We will also make provision for the compilation of combinators of arbitrary complexity. This provision will displace the use of built in data types and primitive operations.

We then have a machine which is attempting (and failing) to prove a theorem of our primitive logical formalism. The theorem to be proven is a term (held in a persistent store) part of which is an unbounded structure representing all the data input to the machine (in the manner of a lazy list).

The remainder of the term consists of two main elements. The first is a function which may be regarded either as representing the combined operating system and application development software of the machine or as a derived inference rule, The second may be regarded either as a functional database (as in [Nik85]) containing all the users data, or as a compound proposition expressing the content of the users "knowledge base".

The theorem which the machine is trying to prove is the application of the derived inference rule to the conjunction of the input data with the knowledge base. The theorem proving strategy is essentially reduction of a term of pure combinatory logic to its normal form, (the theorems of our primitive logic are just those terms of pure combinatory logic which are reducible to K).

The hypothesis however has no normal form, and the reduction process results in the generation of an infinite term. The head of this term at any stage in the reduction consists of all the outputs of the system, while the tail represents the knowledge base, the remainder of the input list (new facts), and the operating system (inference rule). All of these are are iteratively updated during the evaluation process, so that the changes to the knowledge base are the effects of the commands occurring in the input list, and the output at the head of the term grows as further information is presented to users.

The implementation of our formal system on this engine will in some respects resemble that of LCF and its variants, with the following modifications.

Firstly the primitive logic is type-free, and hence much simpler, Secondly, the same language will be in use both for metalanguage and object language, resulting in further economies. Also, as previously noted, derived inference rules will be established after the manner of [Boy81], rather than as proof generation algorithms, this is essential to achieving tolerable efficiency in the proof facilities, We will support extensions to the abstract syntax to match the establishment of abstract data types, and will allow flexibilty of concrete syntax as in the Mule system [Nip85].


up home © RBJ dated 86/7/15 HTML 96/6/6 edited 96/6/15