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?