Extended Axiomatic Language
Using the Complement of a Valid Expression Set for Specification
back to Axiomatic Language Home Page
Axiomatic language is a powerful formalism for defining recursively enumerable
sets of hierarchical symbolic expressions. When one specifies a recursively
enumerable set, one is simultaneously specifying the complement of that set,
which may not be recursively enumerable. This complement set may be useful
for specification. This web page defines "extended axiomatic language",
which uses this complement set to define new valid expressions and
effectively provides a form of negation.
1. Extended Axiomatic Language -- A Preliminary Definition
We will refer to the original language as "basic axiomatic language" and
the set of generated expressions as "basic valid expressions". The term
"complementary expression" will refer to an expression that has no instance
that is a valid expression. Thus if our set of basic axioms consists
of just the identical expressions axiom,
(== % %).
then (== a a) and (== (b %) (b %))
are basic valid expressions,
and (== a b) and (== (%1 x) (%2 y))
are complementary expressions,
but (== %1 %2)
is neither valid nor complementary
since some instances are valid and some are not.
A "complementary axiom" is one that has one or more "complementary conditions", denoted by a tilde after the condition expression:
conclu < ..., cond~, ....
A set of "extended axioms" consists of basic and complementary axioms and
generates a set of "extended valid expressions". The conclusion of an
extended axiom instance is an extended valid expression if all the
"positive" conditions are extended valid expressions and all the
complementary conditions are complementary expressions. Note that the set
of complementary expressions (defined from just the basic axioms) remains
fixed as the extended valid expressions are generated. Note also that the
set of extended valid expressions includes the basic valid expressions
as a subset.
Extended axiomatic language makes it easier to define negative predicates:
! some basic axioms:
(member % ($1 % $2)). ! member of a sequence
(reverse () ()). ! reverse of a sequence
(reverse (% $seq) ($rev %))< (reverse ($seq) ($rev)).
(sequence ($)). ! set of sequences
! some complementary axioms:
(not_member %x %seq)< (sequence %seq), (member %x %seq)~.
! not a member of a sequence
(not_palindrome %)< (sequence %), (reverse % %)~.
! sequences that are not palindromes
Extended axiomatic language also lets us define the set of all atoms
and an inequality relation between distinct atoms, which is not built-in:
(atom %)< (sequence %)~. ! set of atoms
(/=atoms %1 %2)< (atom %1), (atom %2), (== %1 %2)~. ! distinct atoms
These relations can be defined in basic axiomatic language,
but not as concisely or completely.
See the Calculator Program for an example
of using extended axiomatic language to define error handling.
2. Extended Axiomatic Language -- Generalized
One observation about the above preliminary definition is that we might want to make use of the complement of the extended valid expressions. A natural generalization of the above definition is to let the "complementation" process that is applied to the basic valid expressions be applied to the extended valid expressions to define a new "level" of extended valid expressions. We refer to the set of basic valid expressions and their complement as "level 0" or EAL0. The EAL0 complementary expressions match the complementary conditions in complementary axioms as described above to generate the "level 1" or EAL1 valid expressions and their complement. This process could be repeated to define levels 2,3,....
The relationships of the different levels of extended axiomatic language
can be shown by the following bar graphs that partition the complete
set of ground expressions (i.e., expressions without variables)
into those that are valid and those that are complementary.
Non-ground expressions (those with variables) are valid/complementary
if all their instances are valid/complementary, respectively, or they may
be neither valid nor complementary if instances are both.
For level 0 extended axiomatic language (basic axiomatic language) the
partition of ground expressions into valid (EAL0v) and complementary
(EAL0~) can be represented as follows:
______________0____________________________________________________
|______EAL0v___|______EAL0~_________________________________________|
The complementary expressions EAL0~ applied to the extended axioms yields
the level 1 extended valid expressions and their complement:
______________0_____________________1______________________________
|________________________EAL1v_______|____EAL1~_____________________|
(The numbers above the bar show the successive partitions.)
As stated above, the level 1 extended valid expressions EAL1v include the
basic valid expressions EAL0v:
EAL1v ⊇ EAL0v (EAL1~ ⊆ EAL0~)
We now apply the complementary expressions EAL1~ to our extended axiom set
to yield level 2 extended valid expressions and their complement:
______________0____2________________1______________________________
|__________EAL2v____|______EAL2~____________________________________|
Our set of level 2 valid expressions EAL2v is still a superset of the basic
valid expressions EAL0v:
EAL2v ⊇ EAL0v (EAL2~ ⊆ EAL0~)
Since the complementary expressions EAL1~ that generate EAL2v are a subset
of the EAL0~ expressions that generate EAL1v, we have
EAL2v ⊆ EAL1v (EAL2~ ⊇ EAL1~)
Now we apply the complementary expressions EAL2~ to our extended axiom set
to yield level 3 extended valid expressions and their complement:
______________0____2__________3_____1______________________________
|____________________EAL3v_____|____EAL3~___________________________|
Since the EAL2~ expressions that generate EAL3v are a superset of the EAL1~
expressions that make EAL2v, we have
EAL3v ⊇ EAL2v (EAL3~ ⊆ EAL2~)
Since the EAL2~ expressions are a subset of the EAL0~ expressions,
we have
EAL3v ⊆ EAL1v (EAL3~ ⊇ EAL1~)
We continue with the level 4 extended expressions defined from EAL3~:
______________0____2___4______3_____1______________________________
|_______________EAL4v___|____EAL4~__________________________________|
Since EAL3~ is a subset of EAL2~, we have
EAL4v ⊆ EAL3v (EAL4~ ⊇ EAL3~)
and since EAL3~ is a superset of EAL1~, we have
EAL4v ⊇ EAL2v (EAL4~ ⊆ EAL2~)
It appears that the valid expression sets for the even-numbered levels
EAL0v, EAL2v, EAL4v, ..., are non-decreasing and bounded from above by the
odd-numbered levels EAL1v, EAL3v, ...,
which are non-increasing.
We now give a proof of this property.
Let i0 be some even level number and let i1,i2,... represent
level numbers i0+1,i0+2,....
Our inductive hypothesis is that the following relations hold:
________________0____2_________1___________________________
EALi2v ⊆ EALi1v (EALi2~ ⊇ EALi1~)
EALi2v ⊇ EALi0v (EALi2~ ⊆ EALi0~)
As shown above,
these relations are true when i0 = 0, so the base case is satisfied.
Letting level i3 = i2+1 be defined from complementary expressions EALi2~,
we get:
________________0____2______3__1___________________________
EALi3v ⊇ EALi2v (EALi3~ ⊆ EALi2~)
-- since EALi2~ ⊇ EALi1~
EALi3v ⊆ EALi1v (EALi3~ ⊇ EALi1~)
-- since EALi2~ ⊆ EALi0~
Now we define level i4 = i2+2 expressions from the complementary expressions
EALi3~:
________________0____2__4___3__1___________________________
EALi4v ⊆ EALi3v (EALi4~ ⊇ EALi3~)
-- since EALi3~ ⊆ EALi2~
EALi4v ⊇ EALi2v (EALi4~ ⊆ EALi2~)
-- since EALi3~ ⊇ EALi1~
But these are the same relations as our induction hypothesis when we let
i0 = i0+2, so the relations are true for all even i0.
We formally define extended axiomatic language as the limit of the
even-numbered levels as i0 goes to infinity. This would be a fixed
point in the sense that if EALv is this limit, then applying the
EAL complementation step twice will produce the same set of (even level)
valid expressions.
We can illustrate the levels of extended axiomatic language with some
examples.
[Example 1]
Suppose our set of extended axioms consists of just
this single complementary axiom:
P < P ~.
Since there are no basic axioms, the set of basic valid expressions EAL0v
is empty:
EAL0v: empty EAL0~: everything
Since the symbol P is in the complementary expression set EAL0~,
our level 1 valid expressions will include P:
EAL1v: P EAL1~: everything except P
Now since P is not in the complementary expression set EAL1~, our level 2
valid expressions will not include P:
EAL2v: empty EAL2~: everything
But this is the same as level 0. Thus the even levels will not contain
P but the odd levels will. And according to our formal definition,
the extended valid expressions will not contain P. This is the
extended axiomatic language solution to the above apparently contradictory
axiom.
[Example 2]
For our next example of extended axiomatic language levels,
consider the following set of axioms:
(num 0). ! basic axioms for set of natural numbers
(num (s %))< (num %).
(even 0). ! 0 is even
(even (s %))< (num %), (even %)~. ! if k not even, k+1 is even
The basic valid expressions include the natural numbers in successor
notation, so these expressions are in all extended valid expression levels
below. We thus limit our analysis
to the 'even' predicate with natural number arguments:
EAL0v: (even 0)
EAL0~: (even k), k>=1
Applying our complementary expressions EAL0~ we get:
EAL1v: (even 0), (even k), k>=2
EAL1~: (even (s 0))
Applying EAL1~ we get:
EAL2v: (even 0), (even (s (s 0)))
EAL2~: (even (s 0)), (even k), k>=3
Applying EAL2~:
EAL3v: (even 0), (even (s (s 0))), (even k), k>=4
EAL3~: (even (s 0)), (even (s (s (s 0)))
Applying EAL3~:
EAL4v: (even 0), (even (s (s 0))), (even (s (s (s (s 0)))))
EAL4~: (even (s 0)), (even (s (s (s 0))), (even k),k>=5
Each successive even-numbered level adds an 'even' expression with another
even number. The limit defines the even predicate for all even numbers,
so this, along with the 'num' predicate,
is the set of extended valid expressions.
[Example 3]
For our last example of extended axiomatic language levels, we will
combine an arbitrary set of basic axioms with a single
complementary axiom that defines a predicate for complementary
expressions:
<some basic axioms>
(~ %)< % ~. ! ~ is predicate for complementary expressions
We use the symbol consisting of just the tilde character ~ as the
name of the predicate for complementary expressions.
(This predicate name is just an arbitrary symbol and is distinct from
the use of tilde after a complementary condition.)
We let 'b' represent the set of basic valid expressions
generated by the basic axioms.
For this example, none of the basic valid expressions will include
the predicate ~.
Our level-0 extended axiomatic language valid expressions are just
the b expressions:
EAL0v: b -- the set of basic valid expressions
(none of which are of the form (~ expr))
To help define expression sets, we will use the symbol % to denote
the set of all expressions and the symbol * to represent all
expressions except those involving the complementary predicate (~ expr).
We will also use + and - to denote set union and difference.
Thus the set of all expressions % can be partitioned into those
those not including and those including the complementary predicate:
% = * + (~ %) -- partition of set of all expressions
* = atoms + () + (%) + (not~ %) + (% % % $)
-- all expressions except those of form (~ %)
-- $ represents set of all strings, so
(% % % $) is set of all sequences of length >=3
atoms = % - ($) -- set of all atoms
not~ = % - ~ -- set of all expressions other than the tilde symbol
We can now express the level-0 complement expressions as follows:
EAL0~: everything but b
: % - b -- all expressions except b valid exprs
: {* + (~ %)} - b -- partitioning the set of expressions
: *-b + (~ %) -- (b has no expressions of form (~ expr))
-- *-b is complement of b except for the (~ expr) exprs
Applying our complementary expressions EAL0~, we get level 1:
EAL1v: b + (~ {*-b + (~ %)})
b + (~ *-b) + (~ (~ %))
EAL1~: % - {b + (~ *-b) + (~ (~ %))}
{* + (~ %)} - b - (~ *-b) - (~ (~ %)))
* - b + (~ %) - (~ *-b) - (~ (~ %))
*-b + (~ {% - *-b - (~ %)})
*-b + (~ {* + (~ %)} - *-b - (~ %))
*-b + (~ {* - *-b} + (~ {% - %}))
*-b + (~ b)
Applying EAL1~ we get:
EAL2v: b + (~ {*-b + (~ b)})
b + (~ *-b) + (~ (~ b))
EAL2~: % - {b + (~ *-b) + (~ (~ b))}
{* + (~ %)} - b - (~ {*-b - (~ b)})
*-b + (~ {% - *-b - (~ b)})
*-b + (~ {* + (~ %)} - *-b - (~ b))
*-b + (~ {* - *-b} + (~ % - b))
*-b + (~ b) + (~ (~ {* + (~ %)} - b))
*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ %)))
Applying EAL2~:
EAL3v: b + (~ {*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ %)))})
b + (~ *-b) + (~ (~ b)) + (~ (~ (~ *-b))) + (~ (~ (~ (~ %))))
EAL3~: % - {b + (~ *-b) + (~ (~ b)) + (~ (~ (~ *-b))) + (~ (~ (~ (~ %))))}
{* + (~ %)} - b - (~ *-b - (~ b - (~ *-b - (~ %))))
*-b + (~ % - *-b - (~ b - (~ *-b - (~ %))))
*-b + (~ b + (~ % - b - (~ *-b - (~ %))))
*-b + (~ b + (~ *-b + (~ % - *-b - (~ %))))
*-b + (~ b + (~ *-b + (~ b - (~ % - %))))
*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ b)))
Applying EAL3~:
EAL4v: b + (~ {*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ b)))})
b + (~ *-b) + (~ (~ b)) + (~ (~ (~ *-b))) + (~ (~ (~ (~ b))))
EAL4~: % - {b + (~ *-b) + (~ (~ b)) + (~ (~ (~ *-b))) + (~ (~ (~ (~ b))))}
*-b + (~ % - *-b - (~ b - (~ *-b - (~ b))))
*-b + (~ b + (~ % - b - (~ *-b - (~ b))))
*-b + (~ b + (~ *-b + (~ % - *-b - (~ b))))
*-b + (~ b + (~ *-b + (~ b + (~ % - b))))
*-b + (~ b + (~ *-b + (~ b + (~ *-b + (~ %)))))
*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ b))) + (~ (~ (~ (~ *-b))))
+ (~ (~ (~ (~ (~ %)))))
Based on the pattern of EALv0,2,4, we conjecture that the complete set
of extended valid expressions will be:
b + (~ *-b) + (~ (~ b))
+ (~ (~ (~ *-b))) + (~ (~ (~ (~ b))))
+ (~ (~ (~ (~ (~ *-b))))) + (~ (~ (~ (~ (~ (~ b))))))
... ...
This needs an induction proof, of course.
3. Examples
This section gives examples showing the usefulness of extended axiomatic
language for specification.
Section A uses the predicate for the set of complementary
expressions to define the "plain vanilla
meta-interpreter" for extended axiomatic language.
Section B defines universal and existential quantification for valid
expressions and uses it to define the set of "valid clauses".
3.A. Complementary Expression Predicate
Example 3 of Section 2 above introduced the complementary expression
predicate ~ that states that
its argument is a complementary expression:
(~ %comp)< %comp ~. ! complementary expression predicate
Combined with the axioms of Section 1 above,
we get the following extended valid expressions:
(~ (== a b))
(~ (== (a %a) (b %b))) -- all instances are valid
(~ (atom ($))) -- all instances are valid
(~ (~ (== x x)))
(~ (~ (~ (== a b))))
(~ (~ (~ (~ (== x x)))))
You will note that these satisfy the pattern of the set of
extended valid expressions for Example 3, above.
Using the ~ predicate for complementary conditions we can represent a
set of extended axioms as data in a single expression,
i.e., the "plain vanilla meta-interpreter":
(axiom_set
((== % %))
((sequence ($)))
((atom %) (~ (sequence %)))
((/=atoms %1 %2) (atom %1) (atom %2) (~ (== %1 %2)))
).
(axiom $axiom)< (axiom_set $axioms1 ($axiom) $axioms2).
(all_valid). ! all expressions in list are valid
(all_valid %expr $exprs)< %expr , (all_valid $exprs).
%conclu < (axiom %conclu $conds), (all_valid $conds).
Some other higher-order forms involving complementary expressions that may
be useful are as follows:
! all~ - all expression in list are complementary
(all~).
(all~ %~expr $~exprs)< %~expr ~, (all~ $~exprs)).
! one~ - (at least) one expression in list is complementary
(one~ $1 %~expr $2)< %~expr ~.
! exactly_one~ - exactly one expression is complementary (the rest are valid)
(exactly_one~ $v1 %~expr $v2)< %~expr ~, (all_valid $v1 $v2).
! exactly_one_valid - exactly one expression is valid (the rest complementary)
(exactly_one_valid $~1 %valid $~2)< %valid , (all~ $~1 $~2).
Note that we could have written (~ %~expr) instead of
the complementary condition %~expr ~ in these axioms.
3.B. Quantification on Encoded Expressions
Extended axiomatic language allows us to define a form of quantification
on valid expressions. We can assert, for example, that all instances
of an expression are valid. To do this we will use (non-variable) ground
symbols to represent real variables. Symbols beginning with # and & will
represent expression and string variables, respectively. To
represent actual symbols beginning with # and &, we will prepend an
underscore _. To represent symbols _#.. and _&.., we prepend
another _, etc. The utility file
enc_inst.eax uses
extended axiomatic language to define the following predicate that
maps an encoded expression (with {_}#.. and {_}&.. symbols) to
a real expression instance:
(enc_inst <enc_expr> <real_inst>)
<enc_expr> -- an expression with encoded variables
<real_inst> -- corresponding expression with real variables
(possibly instantiated)
#... -- symbol representing an expression variable
_#... -> #... -- symbols representing symbols
__#... -> _#... ... with leading _ removed
...
&... -- symbol representing a string variable
_&... -> &...
__&... -> _&...
...
some example valid expressions:
(enc_inst (== # #) (== (a $) (a $)))
(enc_inst (append1 (&) # (& #)) (append1 ($) % ($ %)))
(enc_inst (symbols: _#a _&b ___#c) (symbols: #a &b __#c)) -- no vars
Our quantification definitions involve quantification over
all the variables in an encoded expression.
We first define the predicate 'E' which asserts that
its encoded expression argument has a real instance that is a valid
expression:
! E - there exists an instance that is valid
(E %enc)< (enc_inst %enc %inst), %inst . ! (a)
An example valid expression would be (E (== #a #b))
since the instance (== c c) is valid.
Similarly, we can define predicate 'E~' which asserts that an instance
is complementary:
! E~ - there exists an instance that is complementary
(E~ %enc)< (enc_inst %enc %inst), %inst ~. ! (b)
An example valid expression would be (E~ (== #a #b))
since the instance (== c d) is complementary.
Using the complement of the 'E' and 'E~' predicates, we can define
universal quantification:
! A - all instances are valid
! (no instance is complementary)
(A %enc)< (E~ %enc)~. ! (c)
! A~ - all instances are complementary
! (no instance is valid)
(A~ %enc)< (E %enc)~. ! (d)
Some example valid expressions are (A (== (&) (&)))
and (A~ (== (a #) (b #))).
A "valid clause" is a conclusion and zero or more conditions, just like
an axiom, that has the property that if we add it to the set of axioms,
no new valid expressions are generated. The valid clause is thus
"implied" by the set of axioms. Some example valid clauses given the
above axioms are as follows:
(== (a %) (a %)).
(num (s (s %))< (num %).
Using these quantification predicates along with some higher-order forms
we can define a predicate for the set of valid clauses:
! enc_valid_clause - encoded expression represents a valid clause
(enc_valid_clause %enc_conclu $enc_conds)< ! (e)
(A (one_valid %enc_conclu (~ (all_valid $enc_conds)))).
! -- An "encoded" clause is valid if
! for all instances of the encoded variables,
! either the conclusion is valid or the conjunction of
! the conditions is complementary.
! example encoded valid expressions generated:
! (enc_valid_clause (num (s (s #))) (num #))
! (enc_valid_clause (== (a &1) (a &2)) (== (&1) (&2)))
! valid_clause - set of valid clauses (with real variables)
(valid_clause $clause)< (enc_valid_clause $enc_clause), ! (f)
(enc_inst ($enc_clause) ($clause)).
! example valid expressions:
! (valid_clause (num (s (s 0))) (num 0)) -- valid because conclu valid
! (valid_clause (num (s (s a))) (num a)) -- valid because cond not valid
! (valid_clause (num (s (s %))) (num %)) -- valid because all insts valid
Valid clauses can be used to state assertions about a set of axioms
as a way to check a specification.
For example, an addition predicate should be commutative, else we have an
error:
Error! < (valid_clause (== %3a %3b) (plus %1 %2 %3a)
(plus %2 %1 %3b))~.
If any instance of the valid clause condition is not valid, then the 'Error!'
symbol is generated as a valid expression and that indicates the addition
predicate has an error.
The above quantification axioms also generate valid expressions that
represent nested quantification.
For example, the statement that "for all X, there exists a Y equal to X"
is represented by the valid expression:
(A (E (== #x _#y))) (g)
Axiom (a) above first generates valid expressions such as
(E (== a #y)) and (E (== (b c) #y)).
In fact, all instances of (E (== % #y)) are
generated as valid expressions. Thus, using axiom (c) we get the valid
expression (g). Note that the existential variable #y must be encoded
with a leading underscore _.
Another example of nested quantification uses the following basic axiomatic
language predicate '<=len' which says that the first argument sequence has
length less than or equal to that of the second argument sequence:
! <=len - first argument sequence length <= second argument length
(<=len () ($)).
(<=len (%1 $1) (%2 $2))< (<=len ($1) ($2)).
The statement "there exists an expression (namely the empty sequence) that
has length <= that of all other sequences" is represented by the
following valid expression:
(E (A (<=len #x (_&y)))) (h)
Axiom (c) above generates the valid expression
(A (<=len () (&y))). Combining this
with axiom (a) gives the valid expression (h).