HOST Implementation Features

Introduction
The features described here are the desired features of a proposed implementation of Higher Order Set Theory. At present this is totally fantastic, but I hope to be progressing the details of the design alongside prototyping activities, and that should help this to evolve towards the achievable.

The two principle design requirements are that:

  1. The system should be suitable for the support of a variety of notations in the context of a single logical foundation.
  2. The system be able to perform, in the context of a proof, efficient symbolic or numerical computations by comparison with tools not based on proof (e.g. Mathematica, Maple).

The LCF Paradigm
The system will be implemented broadly following the LCF paradigm but with some novel features:
  1. Combine the LCF "proof is computation" with "computation is proof" by embedding core standard ML into the object language and implementing evaluation of ML during rewriting in the logical kernel.
  2. The dominant proof flavour is "proof by evaluation".
  3. No TACTICS (in the traditional sense).
  4. Context sensitive domain specific proof automation.

Notational Genericism through Semantic Embedding
Consideration will be given to the ease with which diverse notations can be semantically embedded into HOST. The embedding of SML in the kernel will make this easier because this will make available mutually recursive datatype definitions for abstract syntax. The semantic embedding will also make more convenient definition of semantic functions (using pattern matching) over these syntactic domains. Consideration will also be given to whether special support for languages presented in XML should be provided.

Computational Efficiency
The primary purpose of the semantic embedding of SML in the kernel is to enable evaluation of functions defined in the object language to be done efficiently during proof. This will mean that arithmetic computations involving functions defined in the object language using embedded SML will be evaluated, during the course of proofs, as a part of rewriting, without any performance penalty.

Unfortunately, well behaved arithemetic facilities are at present available only for integers. Floating point arithmetic is not suitable for use in this context. A rational arithmetic package is available for CAML, but this still falls short of the needs for a computationally efficient implementation of classical analysis. Such an implementation will be needed before proof based mathematics can displace less rigorous methods as a practical method of solving real engineering problems.

Huge Powerful Logical MegaKernel
As indicated above, though the primitive logic is quite simple, the logical kernel is much more complex, incorporating the logic of a large subset of core standard ML. Getting this (derived) logic right is the main theoretical challenge in this proposal, and may take some time. Prototyping of the kernel will take place concurrently with this more theoretical work.

At a first cut this is just a problem of devising a routine embedding of a well defined small programming language into higher order set theory, which is rather like a routine rewriting of the semantics (which is currently defined using a structured operational semantics). The benefit from doing this will however be sensitive to how well the embedding is integrated with the rest of the object language. To get a good solution will not be a routine exercise.

HOST is a Mathematical Foundation System,
Are Foundations Necessary?
HOST rationale HOST pedigree HOST features


UP HOME © RBJ created 1997/12/08 modified 1997/12/08