A Minimal Specification Language

 

 

Walter W. Wilson

 

Computer Sciences Corporation

& The University of Texas at Arlington

wwilson3@csc.com

wilsonww11@msn.com

 

 

 

LOPSTR 2000

July 27, 2000

 



Language Objectives

 

1.  pure specification language

·      what, not how

·      efficiency is ignored

·      transformation is required

 

1.  minimal

·      as small and simple as possible

·      nothing built-in that can be defined

 

1.  meta-language

·      able to imitate other languages and paradigms

 



An Informal Introduction

 

axiomatic language  [1982]

     =  pure Prolog with revised syntax

     +  higher-order generalization  [HiLog]

     +  "string variables"

 

syntax differences:

 

  father(bill,X)  à  (father Bill %x)

 

·      predicate names moved inside parentheses

·      commas replaced with blanks

·      (expression) variables start with %

 

higher-order generalization:

·      predicate names can be expressions, incl. variables

·      variables can represent entire predicates

 



An Informal Introduction (cont.)

 

example "axioms":

 

  (number 0).

  (number (s %))< (number %).

 

  (plus 0 % %)< (number %).

  (plus (s %1) %2 (s %3)<

    (plus %1 %2 %3).

 

example generated expressions:

 

  (number (s (s (s 0))))

 

  (plus (s 0) (s 0) (s (s 0)))

 



An Informal Introduction (cont.)

 

string variables:

·      start with $

·      match zero or more expressions in a sequence

·      simpler list predicate definitions:

 

  (append ($1) ($2) ($1 $2)).

 

  (member % ($1 % $2)).

 

  (reverse () ()).

  (reverse (% $) ($rev %))<

    (reverse ($) ($rev)).

 

example generated expressions:

 

  (append (a) (b c) (a b c))

 

  (member c (a b c))

 

  (reverse (u v) (v u))

 



The Language

 

"axioms" generate "valid expressions"

 

an expression is:

 

     an atom (symbolic constant),

     an expression variable,

     or a sequence of zero or more expressions and

          string variables

 

syntax:

     atoms:  `abc, `+, `X3

     expression variables:  %expr, %x

     string variables:  $str, $1

     sequences:  (), (`M %y), (`xyz () $ (`))

         -- expressions and string variables separated by

                 blanks and enclosed in parentheses

 



The Language (cont.)

 

axiom: a conclusion expression and zero or more

             condition expressions:

 

     conclu < cond1, …, condn.

     conclu.                                      ! a comment

 

axioms generate axiom instances by substitution:

     -- an expression for an expression variable

     -- a string of expressions and string variables

             for a string variable

 

axiom instances generate valid expressions:

     If all conditions of an axiom instance are valid,

     then the conclusion is valid.

 

For example, axioms

 

  (`a `b).

  ((%) $ $)< (% $).

 

generate valid expressions:

 

  (`a `b)

  ((`a) `b `b)

  (((`a)) `b `b `b `b)

     

 



Some Syntax Extensions

 

characters:

 

  'A'  =  (`char (`bit0 … `bit1))

 

character strings:

 

  (… 'abc' …)   =   (… 'a' 'b' 'c' …)

 

  "abc"  =  ('abc')  =  ('a' 'b' 'c')

 

symbols:

 

  abc   =   (` "abc")

 



Higher-Order Examples

 

definition of relations and sets:

 

  % < (valid $1 % $2).

  (valid (father Sue Tom)

         (father Bill Tom)

         (father Jane Bill)).

 

  (%set %elem)<

    (finite_set %set ($1 %elem $2)).

  (finite_set day

    (Sun Mon Tue Wed Thu Fri Sat)).

    ! generates (day Thu)

 

combining valid expressions:

 

  (all_valid).

  (all_valid % $)< % , (all_valid $).

 

  (one_valid $1 % $2)< % .

  (parent %x %y)<

    (one_valid (mother %x %y)

               (father %x %y)).

 



Higher-Order Examples (cont.)

 

representing axioms in expressions:

 

  %conclu < (axiom %conclu $conds),

            (all_valid $conds).

 

  (axiom (sort %1 %2)

           (permutation %1 %2)

           (ordered %2)).

 

  (axiom $axiom)<

    (axiom_set $1 ($axiom) $2).

 

  (axiom_set

 

    ((times % 0 0)

       (number %))

    ((times %1 (s %2) %3)

       (times %1 %2 %x)

       (plus %x %1 %3))

 

    ((length () 0))

    ((length (% $) (s %n))

       (length ($) %n))

 

  ).

 



Higher-Order Examples (cont.)

 

map predicates to sequences of arguments:

 

  ((` ($rel '*')) $nulls)<

    (zero_or_more () ($nulls)).

  ((` ($rel '*')) $argseqsx)<

    ((` ($rel '*')) $argseqs),

    ((` ($rel)) $args),

    (distr ($args) ($argseqs)

                   ($argseqsx)).

 

  (zero_or_more % ()).

  (zero_or_more % (% $))<

    (zero_or_more % ($)).

 

  (distr () () ()).

  (distr (% $) (($seq) $seqs)

               ((% $seq) $seqsx))<

    (distr ($) ($seqs) ($seqsx)).

 

example valid expressions:

 

  (day* (Sat Tue Tue))

  (reverse* ((a b c) () (u v))

            ((c b a) () (v u))).

 



Meta-Language Examples

 

LISP-like expression evaluation:

 

  (finite_set digit "0123456789").

  (index %set %elem %index)<

    (finite_set %set ($1 %elem $2)),

    (length ($1) %index).

 

  (eval (` (%digit)) %value)<

    (index digit %digit %value).

  (eval (` ($digits %digit)) %valuex)<

    (eval (`$digits)) %value),

    (index digit %digit %n),

    (times %value (s (s (s (s (s

                  (s (s (s (s (s

                 0))))) ))))) %10val),

    (plus %10val %n %valuex).

 

  (eval (quote %expr) %expr).

  (eval (%fn $args) %result)<

    (eval* ($args) ($results)),

    (%fn $results %result).

 

example valid expressions:

  (eval (plus 12 (times 4 5)) (s …))

  (eval (reverse (append (quote (a b))

      (quote (c)))) (c b a))

 



Meta-Language Examples (cont.)

 

procedural language example (from original paper):

 

  (function factorial (N) is

     variables I FACT ;   ! local vars

   begin

     I := 0 ;

     FACT := 1 ;

     while I < N loop

       I := I + 1 ;

       FACT := FACT * I ;

     end loop ;

   end factorial return FACT).

 

  ! add axioms for language definition

 

example valid expression:

 

  (factorial (s (s (s 0)))

      (s (s (s (s (s (s 0)))))))

 



What This Language Does Not Have

 

1. non-logical operations

 

2. built-in predicates

 

3. built-in inequality

-- define inequality between character bit atoms,

         then between characters,

         then between character strings and symbols,

         and finally between expressions containing symbols

 

4. negation

     -- define negative predicates  (ex. "not_member"),

         or define negation-as-failure for encoded axioms

 

5. assert/retract -- a set of axioms is static

 

6. input/output -- defined by interpretation

 



Defining Programs by Interpretation

 

Defining a program with valid expressions:

 

  (program <input> <output>)

 

The input/output expressions are interpreted as files.

(ex. sequence of lines, each a sequence of characters)

 

Example program to reverse lines in a text file:

 

  (program %input %output)<

    (reverse* %input %output).

 

Interactive program:

 

  (program <output1> <input1>

           <output2> <input2>

           … )

 

-- generate for all possible execution histories!

 



String Variable Elimination

 

String variable unification can have multiple mgu's:

 

     example:  (a $) and ($ a) yield $ = '', 'a', 'a a', …

     -- problem due to "non-tail" string variables, as in ($ a)

 

Eliminating non-tail string variables:

 

  … (..x.. $1 ..y..) …

 

is replaced by

 

  … (..x.. $1x) …      ! new variable

 

with the following condition added:

 

  (APPEND ($1) (..y..) ($1x))

 

Then add these axioms:

 

  (APPEND () ($2) ($2)).

  (APPEND (% $1) %2 (% $3))<

    (APPEND ($1) %2 ($3)).

 

Final transformation:  represent sequences as nested pairs

(analogous to Prolog representation of lists)

 



Conclusions

 

simple language

 

higher-order

 

meta-language

 

defining programs by interpretation

 



Future Work on Transformation

 

do example unfold/fold proofs

 

identify proof patterns

 

incorporate into rules and schemas

 

combine into transformation program

-- handle axioms that are instances of stored patterns

 

continue adding rules and generalizing

-- eventually able to handle most programs?