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>

… )

-- 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?