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