1. Introduction

      In the programming language PROLOG, one writes software by functionally specifying it in a form of logic [Bowen 79, Kowalski 79].  This paper proposes a language similar to PROLOG in which software is specified by a type of grammar that generates hierarchical expressions.  This language, which is called "axiomatic language", was developed with the following objectives:

1. very high level --  It should be a formalism for functionally specifying software without specifying an implementation -- the programmer tells the computer what to do without telling it how to do it [Wulf 80].  The programmer's task is simplified since the implementation details are assumed by the (intelligent) language processor.  Furthermore, the resulting programs are more comprehendible since they are pure functional specifications without implementation information.

2. minimal and extensible --  It should be a "minimal" language, instead of large and complex, yet capable of defining any computable function in a way that is clear to the human user.  The arguments in favor of simple, elegant languages as opposed to complicated ones have been well stated by computer scientists [Dijkstra 72, Backus 78].  A language that is minimal must of necessity be extensible; that is, those needed capabilities which are not built-in must be easily definable and then as easily usable as if they had been built-in.  Extensibility means that one can reuse previously defined software components in the definition of new software -- an important requirement for improved software productivity.

3. metalanguage --  It should enable one to define arbitrary language constructs, which can then be used as tools in the specification of software.  Different languages have a variety of features suited to different problems.  The ideal language would be one capable of simulating, and thus incorporating the advantages of, any other language.  With such a metalanguage capability, one could not only define any computable function, but one could define it in nearly any way.  The programmer could express a function in whatever formalism that is most suitable by accompanying it with a definition of the syntax and semantics of that formalism.  A language with this property would be general purpose, yet would allow the programmer to define useful specialized language constructs for particular applications.

      PROLOG is a very high level language and is simple and extensible.  Since axiomatic language uses the same basic construct as PROLOG, it shares these properties.  Axiomatic language, however, can also function as a metalanguage, allowing one to define arbitrary syntactic and semantic forms for the specification of software.  This is claimed as its primary advantage over PROLOG.

      Section 2 defines axiomatic language as an abstract formal system and section 3 gives examples of its use and merits.  Section 4 shows how this formal system is interpreted, with programs defined in a more nonprocedural manner than in PROLOG.  Section 5 defines a proper subset of axiomatic language, called primitive axiomatic language, which has the same power, and section 6 gives conclusions.
 

2. Axiomatic Language

      In axiomatic language a function or program is specified by a finite set of "axioms", which generate a (usually) infinite set of "valid expressions", analogous to the way productions in a type-0 grammar generate strings or the way axioms in logic generate theorems.  An "expression" is defined to be

    an "atom" -- an abstract, primitive element,
    an "expression variable",
    or a "sequence" of zero or more expressions or "string variables".

This differs from PROLOG with the addition of string variables and a different hierarchical structure, adopted from functional programming [Backus 78].

      An atom is represented syntactically by a symbol consisting of letters, digits, and special characters: X3, +.  Expression and string variables are represented by symbols preceded by '%' and '$', respectively: %expr, %x, and $str, $1.  A sequence is represented by a string of expressions and string variables, delimited by blanks and enclosed in parentheses: (M %y), (abc () $2 (*)).  It should be mentioned that these syntax details are somewhat arbitrary.

      An axiom consists of zero or more "condition" expressions followed by a "conclusion" expression:

    if <cond1> and <cond2> and ... and <condn> then <conclu>.

where the <cond> are the condition expressions and <conclu> is the conclusion.  If there are no conditions, the axiom is represented '<conclu>.'.  Long axioms may be written in free format over multiple lines to improve readability and a comment may be written on the right side of a line, following a dash.  This syntax can be compared with the corresponding PROLOG syntax:

    <conclu> :- <cond1>, <cond2>, ..., <condn>.

where the conditions come after the conclusion.  The difference is just a minor issue.  The syntax used in this paper is considered more representative of the way people think.

      A finite set of axioms generates valid expressions by first generating an infinite set of axiom "instances" through the substitution of values for the expression and string variables.  Each occurrence of an expression variable in an axiom can be replaced by an arbitrary expression, the same expression replacing the same variable throughout.  Likewise, each string variable can be replaced by a string of zero or more expressions and string variables.  For example, the axiom

  if (A %x) and ($str1 B $str2) then (C $str1 %x $str2).

has an instance

  if (A (%y)) and (* $str B) then (C * $str (%y)).

by the substitution of '(%y)' for %x, '* $str' for $str1, and '' (the null string) for $str2.

      The generation of valid expressions from axiom instances is governed by the simple rule that if all the conditions of an axiom instance are valid expressions, then the conclusion is a valid expression.  By definition, the conclusion of an "unconditional" axiom is automatically a valid expression.  For example, the two axioms

  (a b).                                     -- an unconditional axiom
  if (%expr $str) then ((%expr) $str $str).  -- a conditional axiom

generate the valid expressions (a b), ((a) b b), (((a)) b b b b), ....
 

3. Some Examples

      This section shows how the simple formal system defined above is used to specify functions.  In section 3.1 axiomatic language is used to define natural numbers and their addition and multiplication.  In section 3.2 the very high level nature of axiomatic language is illustrated by using it to define sorting -- not by an algorithm, but by a formal definition of what sorting is.  In section 3.3 axiomatic language is used as a metalanguage to define the syntax and semantics of a small language in which software can be specified.  The examples presented are written in a somewhat "wordy" style to show how axiomatic language can be made self-documenting.

3.1  Natural Number Arithmetic

      One defines a function in axiomatic language by using axioms to generate valid expressions for each combination of arguments and results.  This is illustrated by the familiar inductive definitions of natural number arithmetic.  Natural numbers can be represented by strings of asterisks:

  (() is a natural number).               -- zero is a natural number
  if (($I) is a natural number)           -- if I is a natural number
    then (($I *) is a natural number).    --   then so is I's successor

These axioms generate valid expressions such as '((* * *) is a natural number)', which represents the statement "3 is a natural number".  Note that the symbols 'is', 'a', 'natural', and 'number' are all abstract atoms with no inherent meaning -- they simply serve for self-documentation.  The addition of natural numbers is defined by the following axioms:

  if (%I is a natural number)               -- if I is a natural number
    then (%I plus () equals %I).            --   then I + 0 = I
  if (%I plus ($J) equals ($K))             -- if I + J = K
    then (%I plus ($J *) equals ($K *)).    --   then I + (J+1) = (K+1)

These axioms generate expressions such as '((* * *) plus (* *) equals (* * * * *))', which says that "3 + 2 = 5".  Of course, the mathematical symbols '+' and '=' can be substituted for the words 'plus' and 'equals'.  The multiplication of natural numbers is similarly defined:

  if (%I is a natural number)             -- if I is a natural number
    then (%I times () equals ()).         --   then I * 0 = 0
  if (%I times ($J) equals %K)            -- if I * J = K
  and (%K plus %I equals %L)              -- and K + I = L
    then (%I times ($J *) equals %L).     --   then I * (J+1) = L

The definition of other numeric data types and operations is done in a similar way.  One can also define decimal digit representations for numbers, such as '((3 5) times (1 8) equals (6 3 0))', where the digits are abstract symbols.  As a further convenience, a syntactic rule could be adopted allowing one to write numbers as, for example, '1234', in place of the expression '(1 2 3 4)'.

3.2  Sorting

      As stated earlier, the objective of very high level languages is to allow one to define what a program does without specifying how it does it.  The very high level nature of axiomatic language can be illustrated by the problem of sorting.  There are many algorithms for sorting, but they all deal with how to sort.  In axiomatic language, sorting is defined by formally specifying what it is.  A sort of a sequence of elements can be defined as a permutation of that sequence such that the resulting sequence is ordered in some way.  This is formally stated by the following axiom:

  if (%y is a permutation of %x) and (%y is ordered)
    then (the sort of %x is %y).

The permutation relation for arbitrary sequences is defined as follows:

  (() is a permutation of ()).
  if (($str1 $str2) is a permutation of ($str3 $str4))
    then (($str1 %expr $str2) is a permutation of ($str3 %expr $str4)).

The ordering predicate as it applies to sequences of arbitrary expressions is defined from the binary relation '<=':

  (() is ordered).               -- the empty sequence is ordered
  ((%expr) is ordered).          -- so is a sequence of one expression
  if (($X1.. %Xn) is ordered)    -- if the sequence X1 .. Xn is ordered
     and (%Xn <= %Xn+1)          --    and Xn <= Xn+1
  then (($X1.. %Xn %Xn+1) is ordered).    -- then X1 .. Xn+1 is ordered

The '<=' relation is defined from the '<' relation:

  (%expr <= %expr).          -- an expr is less than or equal to itself
  if (%x < %y) then (%x <= %y).

The '<' relation for natural numbers is defined as follows:

  if (($I) is a natural number)       -- if I is a natural number
    then (($I) < ($I *)).             -- then I < the successor of I
  if (%I < %J) and (%J < %K) then (%I < %K).

      These axioms generate expressions such as '(the sort of ((* * *) () (*)) is (() (*) (* * *)))', which states that the sort of (3 0 1) is (0 1 3).  This definition of sorting is simpler and clearer than any algorithm one could write in a conventional language.  Furthermore, it has the advantage of being "generic".  It automatically applies to any data type for which the '<' relation is defined.  In section 4.1 the sorting of character strings is illustrated.

3.3  Definition of Language Semantics

      Used as a metalanguage, axiomatic language enables one to define the syntax and semantics of arbitrary language constructs, which can then be used as tools in the specification of software.  One can thus express functions and programs in whatever formalism that is most suited to the problem.  One can even define the syntax and semantics of an entire language and then write software in the language.  In this section a small language is defined that allows one to specify functions of natural numbers algorithmically.  As an example, the factorial function is specified by the following algorithm, represented as an unconditional axiom:

  (function FACTORIAL (N) is
      variables I FACT ;             -- list of local variable names
   begin                    -- arguments & local variables are untyped
      I := () ;                 --  = 0
      FACT := (*) ;             --  = 1  (= 0!)
      while I < N loop          -- loop until I = N
         I := I + (*) ;         -- increment I
         FACT := FACT * I ;     -- FACT := I!
      end loop ;
   end FACTORIAL return FACT).     -- since I = N, FACT = N!

The axioms presented below define a language that generates, from this unconditional axiom, valid expressions such as '(FACTORIAL (* * *) equals (* * * * * *))', which states that 3! = 6.  Other natural number functions can be similarly defined in this language using algorithms expressed as unconditional axioms.  The "top level" axiom defining this language is the following:

  if (function %fn_name ($arg_names) is   -- function name, arg names
         variables $loc_names ;           -- local variable names
      begin
         $stmts                           -- algorithm statements
      end %fn_name return $result_expr)   -- result of function
  and (length ($arg_names) = length ($arg_vals))  --pair names & values
  and (executing ($stmts) with vars ($arg_names $loc_names) and initial
        state ($arg_vals $dummy_vals) yields final state %final_vals)
             -- local variables initially have arbitrary dummy values
  and (expr ($result_expr) with vars ($arg_names $loc_names) having
        values %final_vals equals %result)    -- evaluate the result
  then (%fn_name $arg_vals equals %result).   -- generate valid expr

The length predicate used in the above axiom is defined as follows:

  (length () = length ()).
  if (length ($str1) = length ($str2))
    then (length ($str1 %expr1) = length ($str2 %expr2)).

The syntax and semantics of statements are defined by valid expressions of the form "(executing <statements> with vars <variable names> and initial state <variable values> yields final state <variable values>)".  Each name in the sequence of variable names is paired with a corresponding value in the sequence of variable values.  The axioms that generate these expressions are as follows:

-- sequentially executed statements:  <stmts1> <stmts2>

  if  (executing ($stmts1) with vars %names and initial state %vals1
        yields final state %vals2)
  and (executing ($stmts2) with vars %names and initial state %vals2
        yields final state %vals3)
  then (executing ($stmts1 $stmts2) with vars %names and initial state
        %vals1 yields final state %vals3).

-- assignment statement:  <var_name> := <expr> ;

  if (expr ($expr) with vars ($names1 %name $names2) having values
         ($vals1 %old_val $vals2) equals %new_val)
  and (length ($names1) = length ($vals1))  -- pair var name with value
  then (executing (%name := $expr ;) with vars ($names1 %name $names2)
          and initial state ($vals1 %old_val $vals2)
         yields final state ($vals1 %new_val $vals2)).

-- while loop:  while <condition> loop <stmts> end loop ;

  if (expr ($cond) with vars %names having values %vals equals false)
  and (executing ($stmts) with vars %names and initial state %vals1
       yields final state %vals2)  -- make sure skipped stmts are legal
  then (executing (while $cond loop $stmts end loop ;) with vars %names
     and initial state %vals yields final state %vals).  --loop 0 times

  if (expr ($cond) with vars %names having values %vals1 equals true)
  and (executing ($stmts) with vars %names and initial state %vals1
       yields final state %vals2)                          -- loop 1 ..
  and (executing (while $cond loop $stmts end loop ;) with vars %names
       and initial state %vals2 yields final state %vals3)   -- or more
  then (executing (while $cond loop $stmts end loop ;) with vars %names
       and initial state %vals1 yields final state %vals3).  -- ..times
            -- note that loops must terminate to be defined

The syntax and semantics of expressions are defined by valid expressions of the form "(expr <expression> with vars <variable names> having values <variable values> equals <expression value>)".  The axioms are as follows:

--   <expr>  ::=  <expr> + <expr>  |  <term>

  if  (expr ($expr1) with vars %names having values %vals equals %num1)
  and (expr ($expr2) with vars %names having values %vals equals %num2)
  and (%num1 plus %num2 equals %num3)
  then (expr ($expr1 + $expr2) with vars %names having values %vals
          equals %num3).

  if   (term ($term) with vars %names having values %vals equals %num)
  then (expr ($term) with vars %names having values %vals equals %num).

--   <term>  ::=  <term> * <term>  |  <primary>     (similar to <expr>)

--   <primary>  ::=  <name>  |  <constant>

  if (length ($names1) = length ($vals1))   -- pair var name with value
  then (primary (%name) with vars ($names1 %name $names2) having values
          ($vals1 %val $vals2) equals %val).   -- value of a variable

  if (%num is a natural number)
  then (primary (%num) with vars %names having values %vals
          equals %num).

The syntax and semantics of boolean expressions are defined as follows:

--   <boolean_expr>  ::=  <numeric_expr> < <numeric_expr>

  if  (expr ($expr1) with vars %names having values %vals equals %num1)
  and (expr ($expr2) with vars %names having values %vals equals %num2)
  and (%num1 < %num2 equals %true_or_false)
  then (expr ($expr1 < $expr2) with vars %names having values %vals
          equals %true_or_false).
  if (%I < %J) then (%I < %J equals true).         -- definition of ..
  if (%J <= %I) then (%I < %J equals false).       -- .. the < operator
            -- the other relational operators are similarly defined

      It should be evident that any language construct can be defined in this manner, allowing for certain low-level syntax rules such as the space required between tokens.  As a contrast to the conventional language defined here, a portion of Backus' functional programming has been defined.  Axiomatic language compares favorably with other formalisms for defining programming language semantics [see Cleaveland 80, Marcotty et. al. 76, Stoy 77], with the added advantage of being machine executable.  To define the semantics of a language in axiomatic language is to make it available for use.  The programmer thus has the capability to create whatever language tool is desired for a problem.  Axiomatic language is intended to be a single language which can incorporate the features of any other language.
 

      For other examples of how axiomatic language could be used, one should see examples of how PROLOG is used in such applications as AI knowledge representation and problem solving and database definition and queries [Gallaire & Minker 78, Kowalski 79].

      The extensibility of axiomatic language is seen from the way previously defined functions and relations are used to define new ones.  In an actual programming environment using axiomatic language, there would be a large database of axioms defining various functions and features.  Programmers would build upon this existing software by simply combining the axioms of their programs with those in the database.  This is simpler than the linking and calling of subroutines in conventional languages.  Furthermore, axiomatic language is more modular since each axiom is essentially a small module -- a statement of a "truth", the correctness of which is largely independent of the other axioms.
 

4. Interpreting Axiomatic Language

      Axiomatic language has been presented thus far as an abstract formal system capable of defining "pure" functions and relations.  Real computing, however, involves state changes and input/output.  PROLOG has language primitives for this, but in axiomatic language this is achieved simply by interpreting the valid expressions in different ways.  Section 4.1 shows how axiomatic language defines a program that processes an input file to produce an output file and section 4.2 shows how it defines a program that does interactive input/output.

4.1  Processing a File

      This example defines a program which reads an input file of character strings and produces an output file consisting of those character strings sorted alphabetically.  The axioms for sorting given previously are assumed defined.  It is necessary only to define the binary relation '<' on character strings.

      Characters can be represented by atoms with symbols consisting of the character preceded by a single quote: 'A, '3.  The set of characters and their alphabetical ordering is defined by the following axioms:

  (Chars: '  '0 .. '9 'A .. 'Z ... ).     -- desired alphabetical order
  if (Chars: $str1 %char1 $str2 %char2 $str3)    -- definition of < ..
    then (%char1 < %char2).                      -- .. between chars

A character string is just a sequence of character atoms.  The lexicographic ordering of arbitrary sequences of expressions is defined as follows:

  (($prefix) < ($prefix %expr $str)).
  if (%expr1 < %expr2)
    then (($prefix %expr1 $str1) < ($prefix %expr2 $str2)).

These axioms generate valid expressions such as '(('A 'B 'C) < ('A 'B 'D))'.  From these valid expressions the axioms defining sorting generate expressions such as

  (the sort of
      ( ('C '1)  ('Z)  ('A 'B 'C)  () )
   is
      ( ()  ('A 'B 'C)  ('C '1)  ('Z) ))

representing the sorting of the file of strings "C1", "Z", "ABC", "" to produce the file "", "ABC", "C1", "Z".

      The execution of this sorting "program" would consist of the language processor matching the contents of a specified input text file with the unsorted sequence of one of the valid expressions for sorting, and then putting the corresponding sorted sequence into a specified output file.  The details of how one would initiate this procedure are not important here.  In a similar manner one can define programs that process multiple files of arbitrary data types by associating the files with components of valid expressions.  The language processor would find the valid expression that matches the specified input files and from that generate the output files.  Note that there may be multiple valid expressions which match the specified input files.  If so, then one of the valid expressions is selected nondeterministically and the corresponding outputs are produced.  If there is no valid expression matching the specified input files, the execution "aborts".

4.2  Interactive Programs

      Interactive programs are defined by axioms which generate valid expressions for all possible sequences of inputs and outputs.  Consider a program which reads an arbitrary string of characters (terminated by a carriage return) and then types it back in reverse.  If a null string is entered, the program halts.  A particular execution of this program could be represented by the following valid expression:

  (begin                         -- program execution begins
     (input:  'A 'B 'C 'D)       -- user types "ABCD"
     (output: 'D 'C 'B 'A)       -- program echoes "DCBA"
     (input:  'X '  'Z)          -- user types "X Z"
     (output: 'Z '  'X)          -- program echoes "Z X"
     (input:)                    -- user enters a null string
   end)                          -- program halts

This program is defined by the following axioms, which generate valid expressions such as the one above for all possible sequences of inputs the user might type:

  (the reverse of () is ()).                     -- definition of the
  if (the reverse of ($str1) is ($str2))         --   reverse function
    then (the reverse of ($str1 %expr) is (%expr $str2)).

  (begin (input:) end).                    -- definition of the
  if (begin $i/o end)                      -- begin .. end expressions
  and (the reverse of ($str1) is ($str2))
  then (begin (input: %expr $str1) (output: $str2 %expr) $i/o end).

These axioms define input/output sequences containing arbitrary expressions, but only those expressions with characters are considered.

      The above axioms generate abstract expressions that, when interpreted by the language processor, define in a nonprocedural manner a program that does interactive input/output.  At a given instant during the execution of this program, a particular sequence of inputs and outputs has occurred.  From the set of "(begin ... end)" valid expressions, the language processor finds those that have a prefix that matches the inputs/outputs thus far.  The next expression in those valid expressions specifies whether the program should input a string or output a string.  Nondeterministic interactive programs are possible, such as when two "(begin ... end)" valid expressions have different output strings immediately following a common prefix.

      One may also define programs that do not terminate, by adopting the convention of leaving off the "end".  The following program, for example, simply outputs the string "ABC" in an infinite loop.

  (begin).
  if (begin $str)
    then (begin $str (output: 'A 'B 'C)).

      As with the other syntactic details of axiomatic language, the representation of characters used here is arbitrary.  A more convenient syntax could be adopted, such as allowing one to write '(Output: "abcde")' in place of '(Output: 'a 'b 'c 'd 'e)'.
 

5. Primitive Axiomatic Language

      Axiomatic language is intended to be a minimal language, but in fact it is not.  This section defines a proper subset of axiomatic language, called primitive axiomatic language, which has the same power.  Primitive axiomatic language is just "regular" axiomatic language with string variables eliminated and sequences always of length two (called "pairs").  Expressions are thus binary trees with atoms and expression variables as the leaf nodes.  Axioms are defined the same as in regular axiomatic language and the rules for generating valid expressions from axioms likewise correspond.  The same syntax is used for expressions and axioms.

      As an example of primitive axiomatic language, the definition of natural numbers and their addition are presented:

  (Number 0).                    -- zero is a natural number
  if (Number %I)                 -- if I is a natural number
    then (Number (succ %I)).     --   then the successor of I is also

  if (Number %I)                 -- if I is a natural number
    then (Plus ((%I 0) %I)).     --   then I + 0 = I
  if (Plus ((%I %J) %K))                      -- if I + J = K
    then (Plus ((%I (succ %J)) (succ %K))).   -- then I + (J+1) = (K+1)

These axioms generate valid expressions such as '(Plus (((succ 0) 0) (succ 0)))', representing the statement "1 + 0 = 1".  Because of the difficulty of reading deeply nested parentheses, primitive axiomatic language is interesting more for theoretical and implementation purposes than for actual programming.

      It was said earlier that even though primitive axiomatic language is a proper subset of regular axiomatic language, it has the same power.  This can be shown by simulating regular axiomatic language using primitive axioms.  It can also be shown that axiomatic language is equivalent in power to Turing machines, type-0 grammars, and other formalisms for defining the computable functions.  That axiomatic language is as powerful as these other formalisms is easily demonstrated by using it to simulate type-0 grammars.  That axiomatic language is no more powerful than these other formalisms is shown by the fact that an algorithm that simulates axiomatic language can be written in a conventional programming language.  Thus axiomatic language is another distinct formalism for representing the set of computable functions.
 

6. Conclusions

      Axiomatic language is presented as a simple, elegant, and powerful tool for software development.  It would reduce software costs by eliminating the implementation details from software specification and by simplifying and encouraging the reuse of software components through its extensibility.  It allows one to define arbitrary language constructs for the specification of software in optimal ways.  The price for all this is its difficulty of implementation.  To efficiently execute a program from just its functional specification requires considerable intelligence on the part of the language processor.  Currently, primitive axiomatic language has been implemented in a simple fashion.  Future work will be applied to the problem of efficiency.
 
 

Acknowledgements

      The author wishes to thank Bill Buckles and Ted Sparr of the University of Texas at Arlington for their helpful comments.
 
 

References

Backus, John, "Can Programming Be Liberated from the von Neumann Style?", Comm. ACM, August 1978.

Bowen, Kenneth A., "PROLOG", ACM79 Conference Proceedings.

Cleaveland, J. Craig, "Mathematical Specifications", SIGPLAN, December 1980.

Dijkstra, Edsger W., "The Humble Programmer", Comm. ACM, October 1972.

Gallaire, H. and Minker, J., Eds., Logic and Data Bases, Plenum Press, 1978.

Kowalski, Robert A., Logic for Problem Solving, Elsevier North Holland, 1979.

Marcotty, M.; Ledgard, H. F.; and Bochmann, G. V., "A Sampler of Formal Definitions", ACM Computing Surveys, June 1976.

Stoy, Joseph E., Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977.

Wulf, William A., "Trends in the Design and Implementation of Programming Languages", Computer, January 1980.