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