OpenTheory Article Format

Overview

An OpenTheory article file encodes a higher order logic theory. Articles take the form of text files using the UTF-8 character set, and contain commands which are processed by a stack-based virtual machine. The result of reading an article is an import list and an export list of theorems. The theory encoded by the article depends on the theorems in the import list, and uses them to prove the theorems in the export list.

Types

The primitive types processed by the virtual machine are:

int

Integers, such as 0, 42 and -5.

string

Strings, such as "foo" and "".

typeOp

Higher order logic type operators, such as bool and list.

type

Higher order logic types, such as α and bool list.

const

Higher order logic constants, such as T and =.

var

Higher order logic term variables, such as x.

term

Higher order logic terms, such as 13 and !x. x.

thm

Higher order logic theorems, such as |- x = x and [x = y, y = T] |- x.

When reading an article file, the virtual machine processes values of type object, which has the following ML-like definition:

Virtual Machine

The virtual machine that reads in an article file is equipped with the following data structures:

• A stack containing values of type object.
• A dictionary mapping keys of type int to values of type object.
• An import list of type thm list.
• An export list of type thm list.

Initially the stack, dictionary, import list and export list are all empty.

The virtual machine reads the article file line by line. Every line in an article file is either a comment line or a command line. A comment line has # as its first character. Comment lines are discarded by the virtual machine. A command line encodes exactly one command of the form below, and is immediately executed. As a result of executing a command, the stack, dictionary, import list or export list may be altered. After a command has been executed it is discarded. When the virtual machine has finished processing all the lines in the article file, the import list and export list of theorems are the result of reading the article (the stack and dictionary are discarded).

Commands

i (an integer i represented in decimal as [-]?[1-9][0-9]*)

Push the object Int i on to the stack.

Stack:		Before:		stack
		After:		Int i :: stack

"n" (a quoted string n)

Push the object Name n on to the stack.

Stack:		Before:		stack
		After:		Name n :: stack

absTerm

Pop a term b; pop a variable v; push the lambda abstraction \v. b.

Stack:		Before:		Term b :: Var v :: stack
		After:		Term (mkAbsTerm (v,b)) :: stack

appTerm

Pop a term a; pop a term f; push the function application f a.

Stack:		Before:		Term a :: Term f :: stack
		After:		Term (mkAppTerm (f,a)) :: stack

call

Pop a name n; pop an object i; push the function call marker Call n; push the input argument i.

Stack:		Before:		Name n :: i :: stack
		After:		i :: Call n :: stack

Note: The object i must not be a Call object.

cons

Pop a list t; pop an object h; push the list h :: t on to the stack.

Stack:		Before:		List t :: h :: stack
		After:		List (h :: t) :: stack

Note: The object h must not be a Call object.

const

Pop a name n; push a constant with name n.

Stack:		Before:		Name n :: stack
		After:		Const (mkConst n) :: stack

constTerm

Pop a type ty; pop a constant c; push a constant term with constant c and type ty.

Stack:		Before:		Type ty :: Const c :: stack
		After:		Term (mkConst (c,ty)) :: stack

def

Pop a number k; peek an object x; update the dictionary so that key k maps to object x.

Stack:		Before:		Int k :: x :: stack
		After:		x :: stack
Dictionary:		Before:		dict
		After:		dict[k |-> x]

Note: The object x must not be a Call object.

error

Push the object Error on to the stack.

Stack:		Before:		stack
		After:		Error :: stack

nil

Push the empty list [] on to the stack.

Stack:		Before:		stack
		After:		List [] :: stack

opType

Pop a list of types l; pop a type operator ot; push a type with type operator ot and arguments l.

Stack:		Before:		List [Type t1, ..., Type tn] :: TypeOp ot :: stack
		After:		Type (mkOpType (ot, [t1, ..., tn])) :: stack

pop

Pop an object from the top of the stack.

Stack:		Before:		x :: stack
		After:		stack

ref

Pop a number k; look up key k in the dictionary to get an object x; push the object x.

Stack:		Before:		Int k :: stack
		After:		dict[k] :: stack

Note: This command reads the dictionary, but does not change it.

remove

Pop a number k; look up key k in the dictionary to get an object x; push the object x; delete the entry for key k from the dictionary.

Stack:		Before:		Int k :: stack
		After:		dict[k] :: stack
Dictionary:		Before:		dict
		After:		dict[entry k deleted]

Note: This command is exactly the same as ref, except that it deletes the entry from the dictionary.

return

Pop a name n; pop an object r; pop objects from the stack up to and including the top function call marker Call m; push the return value r.

Stack:		Before:		Name n :: r :: ... :: Call m :: stack
		After:		r :: stack

Note 1: The object r must not be a Call object.
Note 2: The argument m to the top function call marker should satisfy m = n.

save

Peek a theorem th; add th to the list of theorems that the article will export.

Stack:		Before:		Thm th :: stack
		After:		Thm th :: stack
Export list:		Before:		export
		After:		export @ [th]

Note: This command reads the stack, but does not change it.

thm

Pop a term c; pop a list of terms h; push the theorem h |- c with hypothesis h and conclusion c.

Stack:		Before:		Term c :: List [Term h1, ..., Term hn] :: stack
		After:		Thm ([h1, ..., hn] |- c) :: stack

Note: The hypothesis and conclusion terms only provide a specification of the result theorem—the theorem is constructed using the first one of the following methods that succeeds:

1. Look for the result theorem on the export list of the article.
2. If the current function is a primitive inference rule, the result theorem is proved by simulating the inference using the argument value.
3. Look for the result theorem inside an object on the stack.
4. Assert the result theorem as an axiom, and add it to the import list of the article:

	Import list:		Before:		import
			After:		import @ [[h1, ..., hn] |- c]

typeOp

Pop a name n; push a type operator with name n.

Stack:		Before:		Name n :: stack
		After:		TypeOp (mkTypeOp n) :: stack

var

Pop a type ty; pop a name n; push a variable with name n and type ty.

Stack:		Before:		Type ty :: Name n :: stack
		After:		Var (mkVar (n,ty)) :: stack

varTerm

Pop a variable v; push a variable term with variable v.

Stack:		Before:		Var v :: stack
		After:		Term (mkVarTerm v) :: stack

varType

Pop a name n; push a type variable with name n.

Stack:		Before:		Name n :: stack
		After:		Type (mkVarType n) :: stack

Note: An initial apostrophe is not added to the name.

OpenTheory project standard: article file format version 4, published by Joe Hurd on 26 March 2010.