Meta-programming and Sort Constraints
Meta-programming and Sort Constraints
The meta-programming features of BOBJ go outside its hidden order
sorted equational logic, by providing certain functions that manipulate terms
as if they were defined by an equational theory of terms; these features could
be made logical, or more precisely, meta-logical, by providing a reflective
equational theory of BOBJ within BOBJ. Among other things, BOBJ's
meta-programming functions support the definition and use of sort
constraints, a feature of order sorted algebra for defining subsorts by
predicates, in such a way that they can be executed by term rewriting. The
BOBJ specifications in Section 1 use the meta-programming function
~setsort~
, which sets the sort of a term given as one
argument to a subsort that is given as a second argument, and then returns the
resulting term. BOBJ also supports the syntax of membership equational logic,
as a convenient way to declare sort constraints, and translates this syntax
into code that uses ~setsort~
. Membership equational
logic is a variant of order sorted logic developed by Jose Meseguer, and used
in the Maude language. BOBJ has two other meta-programming functions,
~sort~
and ~sort*~
, which respectively
return the sort name of a term given as an argument, and the sort name of the
reduced form of the term given as an argument; these names are of sort
Id
, from the builtin module QID
.
The first example is a bounded stack, which overflows if a given bound is
exceeded. Here stacks are created with the sort Stack?
, which is
then lowered to the subsort Stack
if the bound is not exceeded.
The equation that does this in the first version exploits retracts, another
powerful feature from order sorted algebra. The second version is very
similar, but does not use retracts explicitly. The third version uses the
membership equational logic syntax; note that the show
command
displays the translated version of its membership declaration, which is the
same as that given in the first specification. Note also that the equation
expressing the sort constraint in each example is non-terminating; however,
BOBJ can detect and avoid such simple rewriting loops, instead of just failing
to terminate. Each specification is subjected to exactly the same set of test
cases, and Section 2 gives the output that they produce.
Section 3 gives a different example, in which the even numbers are defined
by a sort constraint, again using the syntax of membership logic. Here the
test cases use ~sort~
and ~sort*~
to
examine the sorts of terms; note that the module QID
must be
loaded in order for these meta-terms to parse. The output is given in Section
4, and from it one can see that the behavior differs from that of "real" sort
constraints and membership declarations, because the sort of a term is lowered
only when there is another operation that requires it to be of the lower sort,
by taking advantage of the fact that this creates a retract. Thus, the sort
constraint equation is not applied at the top of a term. However, our
examples show that we still get the essential power of sort constraints, and
membership logic, in the cases where it is really useful.
Section 5 gives a final example, the theory of categories, where there is a
sort constraint that requires the source of one morphism to agree with the
target of another in order for them to be composable. For those who don't
know (or don't like) categories, a similar example based on graphs is also
given.
1. Specifications for Bounded Stack
***> file: /groups/tatami/bobj/examples/bstack.bob
*** bounded stack with sort constraints
bth STACK is sorts Stack Stack? .
subsort Stack < Stack? .
pr NAT .
let bound = 3 .
op empty : -> Stack .
op push : Nat Stack -> Stack? .
op length_ : Stack? -> Nat .
op top_ : Stack -> Nat .
op pop_ : Stack -> Stack .
op overflow : -> Stack? .
var N : Nat . var S : Stack . var S? : Stack? .
eq top push(N,S) = N .
eq pop push(N,S) = S .
eq length empty = 0 .
eq length push(N,S?) = 1 + length S? .
eq r:Stack?>Stack(S?) = ~setsort~(Stack, S?) if length S? < bound .
eq push(N, S?) = overflow if 1 + length S? >= bound .
end
red length(push(2,push(1,push(0,empty)))).
red push(0,empty).
red push(1,push(0,empty)).
red r:Stack?>Stack(push(0, empty)).
red top(push(0,empty)).
red top(push(1,push(0,empty))).
***> the sort constraint is NOT satisfied in the following:
red push(2,push(1,push(0,empty))).
red push(3,push(2,push(1,push(0,empty)))).
red top(push(2,push(1,push(0,empty)))).
red top(push(3,push(2,push(1,push(0,empty))))).
bth STACK is sorts Stack Stack? .
subsort Stack < Stack? .
pr NAT .
let bound = 3 .
op empty : -> Stack .
op push : Nat Stack -> Stack? .
op length_ : Stack? -> Nat .
op top_ : Stack -> Nat .
op pop_ : Stack -> Stack .
op overflow : -> Stack? .
var N : Nat . var S : Stack . var S? : Stack? .
eq top push(N,S) = N .
eq pop push(N,S) = S .
eq length empty = 0 .
eq length push(N,S?) = 1 + length S? .
eq length overflow = 1 + bound .
eq push(N, S) = ~setsort~(Stack, push(N, S)) if 1 + length S < bound .
eq push(N, S?) = overflow if 1 + length S? >= bound .
end
red length(push(2,push(1,push(0,empty)))).
red push(0,empty).
red push(1,push(0,empty)).
red r:Stack?>Stack(push(0, empty)).
red top(push(0,empty)).
red top(push(1,push(0,empty))).
***> the sort constraint is NOT satisfied in the following:
red push(2,push(1,push(0,empty))).
red push(3,push(2,push(1,push(0,empty)))).
red top(push(2,push(1,push(0,empty)))).
red top(push(3,push(2,push(1,push(0,empty))))).
***> version with membership syntax
bth STACK is sorts Stack Stack? .
subsort Stack < Stack? .
pr NAT .
let bound = 3 .
op empty : -> Stack .
op push : Nat Stack -> Stack? .
op length_ : Stack? -> Nat .
op top_ : Stack -> Nat .
op pop_ : Stack -> Stack .
op overflow : -> Stack? .
var N : Nat . var S : Stack . var S? : Stack? .
eq top push(N,S) = N .
eq pop push(N,S) = S .
eq length empty = 0 .
eq length push(N,S?) = 1 + length S? .
eq length overflow = 1 + bound .
mb S? : Stack if length S? < bound .
eq push(N, S?) = overflow if 1 + length S? >= bound .
end
show .
red length(push(2,push(1,push(0,empty)))).
red push(0,empty).
red push(1,push(0,empty)).
red r:Stack?>Stack(push(0, empty)).
red top(push(0,empty)).
red top(push(1,push(0,empty))).
***> the sort constraint is NOT satisfied in the following:
red push(2,push(1,push(0,empty))).
red push(3,push(2,push(1,push(0,empty)))).
red top(push(2,push(1,push(0,empty)))).
red top(push(3,push(2,push(1,push(0,empty))))).
2. Output for Bounded Stacks
awk% bobj
\|||||||||||||||||/
--- Welcome to BOBJ ---
/|||||||||||||||||\
BOBJ version 0.9.209 built: Thu Nov 21 11:50:07 PST 2002
University of California, San Diego
Fri Nov 22 13:34:08 PST 2002
BOBJ> in sc
==========================================
***> file: /groups/tatami/bobj/sc.bob
==========================================
bth STACK
==========================================
reduce in STACK : length push(2, push(1, push(0, empty)))
result NzNat: 3
rewrite time: 186ms parse time: 5ms
==========================================
reduce in STACK : push(0, empty)
result Stack?: push(0, empty)
rewrite time: 7ms parse time: 2ms
==========================================
reduce in STACK : push(1, push(0, empty))
result Stack?: push(1, push(0, empty))
rewrite time: 18ms parse time: 2ms
==========================================
reduce in STACK : r:Stack?>Stack(push(0, empty))
result Stack: push(0, empty)
rewrite time: 9ms parse time: 1ms
==========================================
reduce in STACK : top push(0, empty)
result Zero: 0
rewrite time: 0ms parse time: 2ms
==========================================
reduce in STACK : top push(1, push(0, empty))
result NzNat: 1
rewrite time: 25ms parse time: 3ms
==========================================
***> the sort constraint is NOT satisfied in the following:
==========================================
reduce in STACK : push(2, push(1, push(0, empty)))
result Stack?: overflow
rewrite time: 7ms parse time: 3ms
==========================================
reduce in STACK : push(3, push(2, push(1, push(0, empty))))
result Stack?: overflow
rewrite time: 7ms parse time: 5ms
==========================================
reduce in STACK : top push(2, push(1, push(0, empty)))
result Nat: top r:Stack?>Stack(overflow)
rewrite time: 13ms parse time: 4ms
==========================================
reduce in STACK : top push(3, push(2, push(1, push(0, empty))))
result Nat: top r:Stack?>Stack(overflow)
rewrite time: 10ms parse time: 5ms
==========================================
bth STACK
==========================================
reduce in STACK : length push(2, push(1, push(0, empty)))
result NzNat: 3
rewrite time: 4ms parse time: 4ms
==========================================
reduce in STACK : push(0, empty)
result Stack: push(0, empty)
rewrite time: 8ms parse time: 1ms
Warning: non-termination corrected
==========================================
reduce in STACK : push(1, push(0, empty))
result Stack: push(1, push(0, empty))
rewrite time: 39ms parse time: 2ms
Warning: non-termination corrected
==========================================
reduce in STACK : r:Stack?>Stack(push(0, empty))
result Stack: push(0, empty)
rewrite time: 8ms parse time: 1ms
Warning: non-termination corrected
==========================================
reduce in STACK : top push(0, empty)
result Zero: 0
rewrite time: 1ms parse time: 2ms
==========================================
reduce in STACK : top push(1, push(0, empty))
result NzNat: 1
rewrite time: 11ms parse time: 15ms
Warning: non-termination corrected
==========================================
***> the sort constraint is NOT satisfied in the following:
==========================================
reduce in STACK : push(2, push(1, push(0, empty)))
result Stack?: overflow
rewrite time: 5ms parse time: 3ms
==========================================
reduce in STACK : push(3, push(2, push(1, push(0, empty))))
result Stack?: overflow
rewrite time: 12ms parse time: 4ms
==========================================
reduce in STACK : top push(2, push(1, push(0, empty)))
result Nat: top r:Stack?>Stack(overflow)
rewrite time: 12ms parse time: 4ms
==========================================
reduce in STACK : top push(3, push(2, push(1, push(0, empty))))
result Nat: top r:Stack?>Stack(overflow)
rewrite time: 7ms parse time: 6ms
==========================================
***> version with membership syntax
==========================================
bth STACK
==========================================
dth STACK is
protecting NAT .
sorts Stack Stack? .
subsorts Stack < Stack? .
var S : Stack .
var S? : Stack? .
op empty : -> Stack .
op bound : -> NzNat .
op overflow : -> Stack? .
op push : Nat Stack -> Stack? .
op length _ : Stack? -> Nat [prec 15] .
op top _ : Stack -> Nat [prec 15] .
op pop _ : Stack -> Stack [prec 15] .
eq bound = 3 .
eq top push(N, S) = N .
eq pop push(N, S) = S .
eq length empty = 0 .
eq length push(N, S?) = 1 + (length S?) .
eq length overflow = 1 + bound .
cq r:Stack?>Stack(S?) = ~setsort~(Stack, S?) if (length S?) < bound .
cq push(N, S?) = overflow if (1 + (length S?)) >= bound .
end
==========================================
reduce in STACK : length push(2, push(1, push(0, empty)))
result NzNat: 3
rewrite time: 4ms parse time: 4ms
==========================================
reduce in STACK : push(0, empty)
result Stack?: push(0, empty)
rewrite time: 4ms parse time: 1ms
==========================================
reduce in STACK : push(1, push(0, empty))
result Stack?: push(1, push(0, empty))
rewrite time: 15ms parse time: 2ms
==========================================
reduce in STACK : r:Stack?>Stack(push(0, empty))
result Stack: push(0, empty)
rewrite time: 8ms parse time: 1ms
==========================================
reduce in STACK : top push(0, empty)
result Zero: 0
rewrite time: 1ms parse time: 9ms
==========================================
reduce in STACK : top push(1, push(0, empty))
result NzNat: 1
rewrite time: 21ms parse time: 2ms
==========================================
***> the sort constraint is NOT satisfied in the following:
==========================================
reduce in STACK : push(2, push(1, push(0, empty)))
result Stack?: overflow
rewrite time: 6ms parse time: 4ms
==========================================
reduce in STACK : push(3, push(2, push(1, push(0, empty))))
result Stack?: overflow
rewrite time: 8ms parse time: 5ms
==========================================
reduce in STACK : top push(2, push(1, push(0, empty)))
result Nat: top r:Stack?>Stack(overflow)
rewrite time: 16ms parse time: 46ms
==========================================
reduce in STACK : top push(3, push(2, push(1, push(0, empty))))
result Nat: top r:Stack?>Stack(overflow)
rewrite time: 11ms parse time: 5ms
BOBJ> q
Bye.
awk%
3. Specification for Even Numbers
***> file: /groups/tatami/bobj/examples/even.bob
*** even natural numbers via sort constraint
dth EVEN is
sorts Nat Even .
subsort Even < Nat .
op 0 : -> Even .
op s_ : Nat -> Nat .
op _ mod2 : Nat -> Nat .
op _ div2 : Even -> Nat .
var N : Nat . var E : Even .
eq 0 div2 = 0 .
eq (s s E) div2 = s (E div2) .
eq 0 mod2 = 0 .
eq (s 0) mod2 = s 0 .
eq (s s N) mod2 = N mod2 .
mb N : Even if N mod2 == 0 .
end
open EVEN + QID .
red ~sort~(0) .
red ~sort~(s 0).
red ~sort*~(s 0) .
red ~sort~(s s 0) .
red ~sort*~(s s 0) .
red 0 div2 .
red (s 0) div2 .
red (s s 0) div2 .
red (s s s 0) div2 .
close
4. Output for Even Numbers
awk% bobj
\|||||||||||||||||/
--- Welcome to BOBJ ---
/|||||||||||||||||\
BOBJ version 0.9.210 built: Fri Nov 22 14:09:23 PST 2002
University of California, San Diego
Fri Nov 22 14:15:20 PST 2002
BOBJ> in even
==========================================
***> file: /groups/tatami/bobj/examples/even.bob
==========================================
dth EVEN
==========================================
open EVEN + QID
==========================================
reduce in EVEN + QID : ~sort~(0)
result Id: 'Even
rewrite time: 103ms parse time: 13ms
==========================================
reduce in EVEN + QID : ~sort~(s 0)
result Id: 'Nat
rewrite time: 0ms parse time: 2ms
==========================================
reduce in EVEN + QID : ~sort*~(s 0)
result Id: 'Nat
rewrite time: 13ms parse time: 1ms
==========================================
reduce in EVEN + QID : ~sort~(s (s 0))
result Id: 'Nat
rewrite time: 1ms parse time: 2ms
==========================================
reduce in EVEN + QID : ~sort*~(s (s 0))
result Id: 'Nat
rewrite time: 2ms parse time: 1ms
==========================================
reduce in EVEN + QID : 0 div2
result Even: 0
rewrite time: 8ms parse time: 1ms
==========================================
reduce in EVEN + QID : (s 0) div2
result Nat: r:Nat>Even(s 0) div2
rewrite time: 38ms parse time: 1ms
==========================================
reduce in EVEN + QID : (s (s 0)) div2
result Nat: s 0
rewrite time: 1ms parse time: 1ms
==========================================
reduce in EVEN + QID : (s (s (s 0))) div2
result Nat: r:Nat>Even(s (s (s 0))) div2
rewrite time: 3ms parse time: 2ms
==========================================
close
BOBJ> q
Bye.
awk%
5. Category and Graph Theory Specifications
***> file: /groups/tatami/bobj/examples/cath.bob
*** theory of categories with a sort constraint
th CATH is sorts Mor Mor? Obj .
subsort Mor < Mor? .
ops (d0_) (d1_) : Mor -> Obj .
op _;_ : Mor Mor -> Mor? [assoc] .
vars M M0 M1 M2 : Mor .
mb (M1 ; M2) : Mor if d1 M1 == d0 M2 .
op id_ : Obj -> Mor .
var O : Obj .
eq d0 id O = O .
eq d1 id O = O .
eq d0 (M0 ; M1) = d0 M0 .
eq d1 (M0 ; M1) = d1 M1 .
eq (id d0 M); M = M .
eq M ; id d1 M = M .
end
open .
ops a b c : -> Obj .
ops f g : -> Mor .
eq d0 f = a .
eq d1 f = b .
eq d0 g = b .
eq d1 g = c .
red f ; g . *** should have sort Mor
red g ; f . *** should have sort Mor?
close
*** theory of paths in a graph with a sort constraint
th PATH is sorts Node Edge Path Path? .
subsort Edge < Path < Path? .
ops (d0_) (d1_) : Path -> Node .
op _;_ : Path Path -> Path? [assoc] .
vars P P0 P1 P2 : Path .
mb (P1 ; P2) : Path if d1 P1 == d0 P2 .
op id_ : Node -> Path .
var N : Node .
eq d0 id N = N .
eq d1 id N = N .
eq d0 (P0 ; P1) = d0 P0 .
eq d1 (P0 ; P1) = d1 P1 .
eq (id d0 P); P = P .
eq P ; id d1 P = P .
end
open .
ops a b c : -> Node .
ops f g : -> Edge .
eq d0 f = a .
eq d1 f = b .
eq d0 g = b .
eq d1 g = c .
red f ; g . *** should have sort Path
red g ; f . *** should have sort Path?
close
6. Output for Category and Graph Theories
awk% bobj
\|||||||||||||||||/
--- Welcome to BOBJ ---
/|||||||||||||||||\
BOBJ version 0.9.210 built: Fri Nov 22 14:09:23 PST 2002
University of California, San Diego
Sat Nov 23 19:48:56 PST 2002
BOBJ> in cath
==========================================
***> file: /groups/tatami/bobj/examples/cath.bob
==========================================
th CATH
==========================================
open
==========================================
ops a b c : -> Obj
==========================================
ops f g : -> Mor
==========================================
eq d0 f = a
==========================================
eq d1 f = b
==========================================
eq d0 g = b
==========================================
eq d1 g = c
==========================================
reduce in CATH : f ; g
result Mor: f ; g
rewrite time: 151ms parse time: 1ms
Warning: non-termination corrected
==========================================
reduce in CATH : g ; f
result Mor?: g ; f
rewrite time: 3ms parse time: 2ms
==========================================
close
==========================================
th PATH
==========================================
open
==========================================
ops a b c : -> Node
==========================================
ops f g : -> Edge
==========================================
eq d0 f = a
==========================================
eq d1 f = b
==========================================
eq d0 g = b
==========================================
eq d1 g = c
==========================================
reduce in PATH : f ; g
result Path: f ; g
rewrite time: 5ms parse time: 1ms
Warning: non-termination corrected
==========================================
reduce in PATH : g ; f
result Path?: g ; f
rewrite time: 2ms parse time: 1ms
==========================================
close
BOBJ> q
Bye.
awk%
To the BOBJ Examples homepage
To Tatami project homepage
Maintained by Joseph Goguen
Last modified: Sat Nov 23 20:30:39 PST 2002