# 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

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:

·      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

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

(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