Synthetic Philosophy and Deductive Engineering
The purpose of this and several subsequent tasks is the formal specification of the SPaDE system. The required specification begins by following the structure of the formal specifications of ProofPower support for HOL, adapting as necessary to the particular needs of the SPaDE system.
For that reason, the first five tasks correspond to the five ProofPower documents in the spc001.pp–spc005.pp sequence, which will be recast as a series of specifications specific to SPaDE written in ProofPower HOL (SML) embedded in github markdown.
It is envisaged that the one formal specification document commissioned by this task description will be produced in stages, since these are the first formal specifications to be assigned to autonomous agents in the SPaDE development and it is not yet clear what agents will have the necessary skills, or what needs to be supplied to the agent to facilitate the work. It is also likely that the full detail in this task description will also appear in stages as the specification evolves.
Two theories come before this one. The SPaDE root theory (tltd002.md) supplies the prelude and the consistency mechanism. The theory of T-expressions (tltd004.md) supplies the free algebra on which abstract syntax is built. Because the SPaDE specifications will in due course be moved from the SPaDE github repository to any early SPaDE native repository, and the details of the core logic and theory will vary from those in ProofPower, we need to take some care to ensure that the essential elements of the logical context in which the specifications are developed on ProofPower can be conveniently reproduced in the native environment.
Initially it is proposed that the work under this task description be conducted in the following stages (after the SPaDE root theory has sufficiently progressed):
Each stage will be prescribed in a separate section below, but the commissioning of work need not wait on the completion of all the sections. It is likely that the first two sections will be commissioned before the detailed requirements for the later sections are fully specified.
The first stage in the production of this specification is the formulation of a generic theory of abstract syntax. It is used for the HOL terms in the specification of HOL. Later it is used when onboarding knowledge or data expressed in some other language, such as Lean: the semantics of that notation are rendered in HOL, and the syntax is this generic one.
spc001.pp–spc005.pp are reference for that work. None of them survives intact. The deductive system remains the same. The way it is expressed is more constructive, explicit, and executable (in particular the representation of inference rules as relations is to be replaced by functions, the partial nature is captured by returning “T” whenever the inference would otherwise fail). The inference rules are written so that SPaDE can prove a derived rule sound and then run it. Those derived rules are the earliest reflective self-improvement.
Every formal specification in HOL opens the theory it is creating with new_SPaDE_theory, defined in tlcd002.md. The call names the theory, its parent, and any further parents. The procedure removes any previous version of the theory before creating it, so a repeated check succeeds whether or not the theory is already present. With the dependencies maintained, a change to one specification causes the makefile to re-check that specification and the specifications that depend on it.
The theory name is brief and suggestive of its nature or role. Correspondence with the document name is not required. The name is not that of an spc theory. Naming and the theory listings are in ampd012.md.
A document derived from a ProofPower source, or from krdd004.md, acknowledges that source. ProofPower checks well-formedness. Correctness is a further, more intelligent check.
The generic abstract syntax starts from the packing and unpacking of null-terminated byte sequences in Encoding and Decoding NTBS and Related Data Types. That account replaces the coding method in spc001 in a way that is less sensitive to features of the language.
A constructor of the language takes strings as arguments. Each string is converted to an NTBS. Those NTBS are concatenated. A code is added (as an NTBS) at the front to identify the construction and then the NTBS sequence is concatenated to yield a byte (char) sequence (STRING) which is the representation of the constructed phrase (TYPE, TERM or larger structure in the SPaDE repository). That code may be the name of the constructor (e.g. “Mk_app”).
The result is a SPaDE specification in markdown, with the HOL in sml fences, stripped to .sml by docs/tlci001.mkf. It is part of SPaDE. The spc documents and retro/ remain reference and bootstrap.
This task is undertaken on its own branch and worktree, as in ampd004.md. A local worker receives that worktree alone, mounted for the task as specified in ampd010.md. It may read the sources named in the architect role card and change only the formal target and its directly related build entries.
The worker must run the stated document-generation and ProofPower validation commands before proposing completion. Those commands are to be made reproducible in this worktree before the task is assigned autonomously; the existing document makefile strips sml fences but is not yet a ProofPower runner for a new architectural script. The worker does not merge its result.
The specification of HOL is built on this abstract syntax. Architectural material in kr/ is input. The likely outcome is a new specification in docs/ which supersedes it. Specifications in kr/ written for HOL4 are not the form of the new architectural HOL.
Subsequent task description will address various other ways in which SPaDE will differ from ProofPower, in advancing to a full specification of the SPaDE repository, and the primitive HOL inference rules.
For that reason, the first five tasks correspond to the five ProofPower documents in the spc001.pp–spc005.pp sequence, which will be recast as a series of specifications specific to SPaDE written in ProofPower HOL (SML) embedded in github markdown.
It is envisaged that the one formal specification document commissioned by this task description will be produced in stages, since these are the first formal specifications to be assigned to autonomous agents in the SPaDE development and it is not yet clear what agents will have the necessary skills, or what needs to be supplied to the agent to facilitate the work. It is also likely that the full detail in this task description will also appear in stages as the specification evolves.