back to Axiomatic Language Home Page

A Concise Definition of Axiomatic Language


1. Goals and Main Idea

Axiomatic language has the following goals:

   (1) pure specification – what, not how
   (2) minimal, but extensible – as small as possible
   (3) metalanguage – able to subsume other languages

Axiomatic language is based on the idea that the external behavior of a program – even an interactive program – can be defined by a static infinite set of symbolic expressions that enumerates all possible inputs – or sequences of inputs – along with the corresponding outputs. The language is just a formal system for defining these infinite sets.


2. The Core Language

In axiomatic language a finite set of axioms generates a (usually) infinite set of valid expressions. An expression is

   an atom – a primitive, indivisible element,
   an expression variable,
   or a sequence of zero or more expressions and string variables.

Syntactically, atoms, expression variables, and string variables are represented by symbols beginning with `, %, $, respectively. Sequences have their elements separated by blanks and enclosed in parentheses: (`M %x () $).

An axiom consists of a conclusion expression and zero or more condition expressions:

   conclu < cond1, …, condn.
   conclu.              ! an unconditional axiom

Comments start with an exclamation point.

Axioms generate axiom instances by the substitution of values for the expression and string variables. An expression variable can be replaced with an arbitrary expression, the same value replacing the same variable throughout the axiom. Similarly, a string variable can be replaced by a string of zero or more expressions and string variables. For example, the axiom 
  (`A %x $)< (`B %x %y), (`C $).
has an instance 
  (`A `x `u %)< (`B `x ()), (`C `u %).
by the substitution of `x for %x, () for %y, and the string `u % for $.

Axiom instances generate valid expressions by the simple rule that if all the conditions of an axiom instance are valid expressions, then the conclusion is a valid expression. (By default, the conclusion of an "unconditional" axiom instance is a valid expression.) For example, the axioms 

  (`a `b).
  ((%) $ $)< (% $).
generate the valid expressions (`a `b), ((`a) `b `b), (((`a)) `b `b `b `b), etc.


3. Syntax Extensions

The expressiveness of axiomatic language is enhanced by the addition of some syntax extensions. A single character in single quotes is equivalent to writing an expression that gives the binary code of the character using bit atoms: 

  'A'  ==  (`char (`0 `1 `0 `0 `0 `0 `0 `1))
A character string in single quotes within a sequence is equivalent to writing those characters separately within that sequence: 
  (… 'abc' …)  ==  (… 'a' 'b' 'c' …)
A character string in double quotes represents the sequence of those characters: 
  "ABC"  ==  ('ABC')  ==  ('A' 'B' 'C')
Finally, a symbol that does not begin with one of the special characters ` % $ ' " ( ) is syntactic shorthand for the following expression that gives the symbol as a character string: 
  ABC  ==  (` "ABC")
Here ` is the atom represented by the just the backquote. This convention allows us to define decimal number representation, which is not built-in.

Here are definitions of some list predicates and example generated valid expressions: 

  (concat ($1) ($2) ($1 $2)).   ! => (concat (a b) (c d) (a b c d))
  (member % ($1 % $2)).         ! => (member b (a b c d))
  (reverse () ()).              ! => (reverse (u v) (v u))
  (reverse ($ %) (% $rev))< (reverse ($) ($rev)).
See the language website for more examples.

back to Axiomatic Language Home Page