Documents‎ > ‎

Ghilbert Specification

This document is the specification for the Ghilbert proof interchange format. It should be possible to determine whether any given proof file is a valid proof or not based on this specification.

[obviously very rough draft, work in progress, at this point]

File structure

The basic unit of Ghilbert is a proof file. A proof file references a number of interface files as well, via urls in the "import" commands. Validity of a proof can be considered as a boolean predicate over the contents of the proof file, plus a mapping from urls to contents of each interface file. This document contains a great many requirements. All of them must be met for a proof to be considered valid.

Syntax

Each file is composed of a sequence of lines, separated by a line-end consisting of either 0x10 (LF) or 0x13 0x10 (CR LF). If a '#' character appears on a line, that character and any successive bytes are considered to be a comment and ignored for the purpose of validating the file.

The remaining bytes must be ASCII 0x20..0x7E. Any contiguous sequence of characters not including space, '(', or ')' is an identifier.

An S-expression is either an identifier or a sequence consisting of '(', zero or more S-expressions and ')'. Spaces and line breaks separating the components of an S-expression are ignored.

A Ghilbert proof or interface consists of a sequence of commands. Each command consists of an identifier for the command type followed by an S-expression containing the arguments.

Kinds, variables, terms

A basic unit in Ghilbert is a term. Each term has an unambiguous kind. Kinds are introduced in interface files using the kind command. Kinds can also be introduced in proof files using the kindbind command, which binds an existing kind to a new name.

A term can be a binding variable, a term variable, or a list consisting of a term name followed by zero or more arguments, each of which is also a term. The number of arguments must match the definition of the term, as must the kind of each argument.

Freeness

One important concept in Ghilbert's metalogic is freeness of binding variables within a term. Freeness is to be evaluated within a free variable constraint context, which can be modeled as a relation between term variables and binding variables. When such a pair is present in the relation, it means that the binding variable is assumed to not appear free in the term variable.

Each introduction of a term provides a freeness map, which is a relation between binding variables appearing as arguments to the term and variables appearing as arguments to the term. [Alternatively, it is a function from binding variable to list of variables].

Then, the predicate "x can occur free in some term, in a given free variable constraint context" is defined recursively thus. If the term is a binding variable, it is true iff the variable is x. If it is a term variable, it is true iff the pair (x, variable) does not appear in the free variable constraint context. If it is a composite term and the none of the arguments to the term are x, then it is the disjunction of whether x can occur free in any of the subterms. If it is a composite term and one of the arguments to the term is x, then it is the disjunction of whether x can occur free in any of the subterms appearing in the term's freeness map related to x.

Examples [to the extent these are needed, the above language is vague and should be improved. Also refer to testsuite for normative examples]:

var (wff ph ps)
var (nat x y)
term (wff (A. x ph))

Assume a free variable constraint context of (ph x). Then, x is not free in y, ph, (A. x ph), (A. y ph), (A. x ps), (A. y ps). It is free in x, ps, (A. y ps).

tvar (nat A B)
term (wff ([/] A x ph) (x A))

Then, assuming a free variable constraint context of (ph x) (A x), x is not free in ([/] A x ph), ([/] A x ps), ([/] A y ph). It is free in ([/] B x ph), ([/] A y ps).

[What about when more than one of the arguments is x? This seems pathological, but I don't know of anything which forbids it. What does the code say?]

Processing model

This document describes the validity of a proof file in terms of an imperative processing model. This is in fact what a typical implementation will do, but implementations are not restricted to this order or style of processing. There is a global state, consisting of four namespaces (interface, kind, term, and theorem/variable), as well as a local state for each imported interface. Proof files and interface files both contain a sequence of commands, each of which manipulates the state in some way, most often by introducing names into it. The name introduced must not already exist in the namespace. When commands refer to names in the namespaces, they must exist at the point in the processing order at the start of the command - commands may not refer to names they themselves introduce or are introduced by future commands.

The "import" command in proof files starts processing of an interface file, referenced by URL. This creates a new local namespace for the purpose of processing the interface. When the interface introduces kind, term, or theorem names, they are introduced both into the local namespace and also, with optional namespace prefix added, into the global namespace. More details of namespace prefixes are described in the details of the "import", "export", and "param" commands below.

Interface commands

kind

The "kind" command takes a one-element list consisting of the kind name. That name must not already exist in the kind namespace. The command introduces the name into the kind namespace.

var

The "var" command takes a list with one or more identifiers. The first is a valid kind. The remainder are variable names, which must be unique and not already exist in the variable/theorem namespace. The command introduces these identifiers as binding variables of the stated kind.

tvar

The "tvar" command is exactly like the "var" command except that it introduces the identifiers as term variables rather than binding variables.

term

The "term" command takes a two or three element list. The first is a valid kind. The second is a list of identifiers, of which the first is a term name, which must not already exist in the term name namespace and the remainder are distinct variables, the arguments to the term. If the third argument is present, it defines a freeness map. Each element of the freeness map is a list of variables, the first of which is a binding variable. All variables in the freeness map must be present in the list of arguments to the term.

The command introduces the term to the term namespace.

stmt

param

Proof commands


import

var

tvar

kindbind

thm

defthm

export

Comments