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.

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

an

an

or a

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:

An

Comments start with an exclamation point.

Axioms generate

(`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