Lazy Functional Programming Examples

The following uses circular coinductive rewriting to prove some behavioral equations for infinite streams; such equations arise, for example, in lazy functional programming. Many such examples were treated by Louise Dennis in her Edinburgh PhD thesis, using complex heuristics to find relations that can succeed with explicit coinduction. Here we use only BOBJ's circular coinductive rewriting algorithm, without any human intervention or machine heuristics. Most of these examples are due to Grigore Rosu. Circular coinductive rewriting was able to solve every example from Dennis's thesis that we tried.

The following three specifications are used throughout this page; note that STREAM and ZIP are parameterized, as are some subsequent modules, though others are instantiated with NAT or BOOL. The operation zip splices two streams together, by taking elements from each one alternately.

th DATA is sort Data . end bth STREAM[X :: DATA] is sort Stream . op head_ : Stream -> Data . op tail_ : Stream -> Stream . op _&_ : Data Stream -> Stream . var D : Data . var S : Stream . eq head(D & S) = D . eq tail(D & S) = S . end bth ZIP[X :: DATA] is pr STREAM[X] . op zip : Stream Stream -> Stream . vars S S' : Stream . eq head zip(S,S') = head S . eq tail zip(S,S') = zip(S', tail S) . end

1. Blink

The goal of the following simple example is to show that the infinite stream 0 1 0 1 0 1 ... is the zip of the two streams containing only 0's and only 1's. The behavioral specification of these three streams is followed by the proof, a particularly elegant example of circular coinductive rewriting.

1.1 Source Code

bth BLINK is pr ZIP[NAT] . ops zero one blink : -> Stream . eq head zero = 0 . eq tail zero = zero . eq head one = 1 . eq tail one = one . eq head blink = 0 . eq head tail blink = 1 . eq tail tail blink = blink . end set cred trace on cred blink == zip(zero, one) .

1.2 Output

This output includes the preliminary material, which is not repeated in subsequent examples. Note that the result to be proved is added as rule (C1), which is then proved by coinduction on the cobasis of STREAM, using (C1) itself; this is the essence of circular coinduction. Note also that a second rule (C2) is also added; in effect, it is a lemma which is also proved along with the main assertion. The keyword deduced in the ouput indicates application of one (or both) of these circularities, as opposed to deduced, which means that the proof only used behavioral reduction with equations in the specifications. awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.0033 built: Fri Mar 17 16:55:05 PST 2000 University of California, San Diego Sat Mar 18 21:57:00 PST 2000 BOBJ> in fpl ========================================== ***> lazy functional programming examples ========================================== th DATA ========================================== bth STREAM ========================================== bth ZIP ========================================== bth BLINK ========================================== c-reduce in BLINK : blink == zip(zero , one) using cobasis for BLINK: op head : Stream -> Nat op tail : Stream -> Stream --------------------------------------- reduced to: blink == zip(zero , one) ----------------------------------------- add rule (C1) : blink = zip(zero , one) ----------------------------------------- target is: blink == zip(zero , one) expand by: op head : Stream -> Nat reduced to: true nf: 0 ----------------------------------------- target is: blink == zip(zero , one) expand by: op tail : Stream -> Stream reduced to: tail(blink) == zip(one , zero) ----------------------------------------- add rule (C2) : tail(blink) = zip(one , zero) ----------------------------------------- target is: tail(blink) == zip(one , zero) expand by: op head : Stream -> Nat reduced to: true nf: 1 ----------------------------------------- target is: tail(blink) == zip(one , zero) expand by: op tail : Stream -> Stream deduced using (C1) : true nf: zip(zero , one) ----------------------------------------- result: true c-rewrite time: 371ms parse time: 9ms ==========================================

2. An Iterative Stream

There are (at least) two ways to define a stream x, f(x), f(f(x)), f(f(f(x))), ..., where f is an arbitrary but fixed function from data to data, one obvious definition and another less obvious. We show that these two are equivalent using circular coinduction.

2.1 Source Code

th FDATA is pr DATA . op f_ : Data -> Data . end bth ITER[X :: FDATA] is pr STREAM[X] . op iter1_ : Data -> Stream . var D : Data . var S : Stream . eq head iter1 D = D . eq tail iter1 D = iter1 f D . op mapf_ : Stream -> Stream . eq head mapf S = f head S . eq tail mapf S = mapf tail S . op iter2_ : Data -> Stream . eq head iter2 D = D . eq tail iter2 D = mapf iter2 D . end set cred trace on cred iter1 D == iter2 D .

2.2 Output

========================================== th FDATA ========================================== bth ITER ========================================== c-reduce in ITER : iter1 D == iter2 D using cobasis for ITER: op head _ : Stream -> Data [prec 15] op tail _ : Stream -> Stream [prec 15] --------------------------------------- reduced to: iter1 D == iter2 D ----------------------------------------- add rule (C1) : iter1 D = iter2 D ----------------------------------------- target is: iter1 D == iter2 D expand by: op head _ : Stream -> Data [prec 15] reduced to: true nf: D ----------------------------------------- target is: iter1 D == iter2 D expand by: op tail _ : Stream -> Stream [prec 15] deduced using (C1) : iter2 (f D) == mapf (iter2 D) ----------------------------------------- add rule (C2) : iter2 (f D) = mapf (iter2 D) ----------------------------------------- target is: iter2 (f D) == mapf (iter2 D) expand by: op head _ : Stream -> Data [prec 15] reduced to: true nf: f D ----------------------------------------- target is: iter2 (f D) == mapf (iter2 D) expand by: op tail _ : Stream -> Stream [prec 15] deduced using (C2) : true nf: mapf (mapf (iter2 D)) ----------------------------------------- result: true c-rewrite time: 85ms parse time: 3ms BOBJ> q Bye.

3. Natural Number Stream

We thank Wolfram Schulte for suggesting that we investigate this and the following example, which shows that two defintitions of the stream of all natural numbers are equivalent.

3.1 Source Code

bth NATSTREAM is pr STREAM[NAT] . op nats_ : Nat -> Stream . var N : Nat . var S : Stream . eq head nats N = N . eq tail nats N = nats N+1 . op succ_ : Stream -> Stream . eq head succ S = 1 + head S . eq tail succ S = succ tail S . op nats'_ : Nat -> Stream . eq head nats' N = N . eq tail nats' N = succ nats' N . end set cred trace on cred nats N == nats' N .

3.2 Output

========================================== bth NATSTREAM ========================================== c-reduce in NATSTREAM : nats N == nats' N using cobasis for NATSTREAM: op head _ : Stream -> Nat [prec 15] op tail _ : Stream -> Stream [prec 15] --------------------------------------- reduced to: nats N == nats' N ----------------------------------------- add rule (C1) : nats N = nats' N ----------------------------------------- target is: nats N == nats' N expand by: op head _ : Stream -> Nat [prec 15] reduced to: true nf: N ----------------------------------------- target is: nats N == nats' N expand by: op tail _ : Stream -> Stream [prec 15] deduced using (C1) : nats' (1 + N) == succ (nats' N) ----------------------------------------- add rule (C2) : nats' (1 + N) = succ (nats' N) ----------------------------------------- target is: nats' (1 + N) == succ (nats' N) expand by: op head _ : Stream -> Nat [prec 15] reduced to: true nf: 1 + N ----------------------------------------- target is: nats' (1 + N) == succ (nats' N) expand by: op tail _ : Stream -> Stream [prec 15] deduced using (C2) : true nf: succ (succ (nats' N)) ----------------------------------------- result: true c-rewrite time: 102ms parse time: 14ms BOBJ> q Bye.

4. Fibonnacci Number Stream

This slightly more complex example shows that two definitions of the stream of Fibonnacci numbers are equivalent; two additional circularities are generated during the proof.

4.1 Source Code

dth NAT-FIBO is pr NAT . var N : Nat . op f_ : Nat -> Nat . eq f(0) = 0 . eq f(1) = 1 . eq f(N + 2) = f(N + 1) + f(N) . end bth STREAM-FIBO is pr ZIP[NAT-FIBO] . var N : Nat . var S : Stream . op nats_ : Nat -> Stream . eq head nats N = N . eq tail nats N = nats N + 1 . op mapf_ : Stream -> Stream . eq head mapf S = f head S . eq tail mapf S = mapf tail S . op fib_ : Nat -> Stream . eq fib N = mapf nats N . op add12_ : Stream -> Stream . eq head add12 S = head S + head tail S . eq tail add12 S = add12 tail tail S . op fib'_ : Nat -> Stream . eq head fib' N = f N . eq head tail fib' N = f(N + 1) . eq tail tail fib' N = add12 zip(fib' N, tail fib' N) . end set cred trace on cred fib N == fib' N .

4.2 Output

========================================== dth NAT-FIBO ========================================== bth STREAM-FIBO ========================================== c-reduce in STREAM-FIBO : fib N == fib' N using cobasis for STREAM-FIBO: op head _ : Stream -> Nat [prec 15] op tail _ : Stream -> Stream [prec 15] --------------------------------------- reduced to: mapf (nats N) == fib' N ----------------------------------------- add rule (C1) : mapf (nats N) = fib' N ----------------------------------------- target is: mapf (nats N) == fib' N expand by: op head _ : Stream -> Nat [prec 15] reduced to: true nf: f N ----------------------------------------- target is: mapf (nats N) == fib' N expand by: op tail _ : Stream -> Stream [prec 15] deduced using (C1) : fib' (1 + N) == tail (fib' N) ----------------------------------------- add rule (C2) : fib' (1 + N) = tail (fib' N) ----------------------------------------- target is: fib' (1 + N) == tail (fib' N) expand by: op head _ : Stream -> Nat [prec 15] reduced to: true nf: f (1 + N) ----------------------------------------- target is: fib' (1 + N) == tail (fib' N) expand by: op tail _ : Stream -> Stream [prec 15] reduced to: tail (fib' (1 + N)) == add12 zip(fib' N, tail (fib' N)) ----------------------------------------- add rule (C3) : tail (fib' (1 + N)) = add12 zip(fib' N, tail (fib' N)) ----------------------------------------- target is: tail (fib' (1 + N)) == add12 zip(fib' N, tail (fib' N)) expand by: op head _ : Stream -> Nat [prec 15] reduced to: true nf: (f N) + (f (1 + N)) ----------------------------------------- target is: tail (fib' (1 + N)) == add12 zip(fib' N, tail (fib' N)) expand by: op tail _ : Stream -> Stream [prec 15] deduced using (C2) : true nf: add12 zip(tail (fib' N), add12 zip(fib' N, tail (fib' N))) ----------------------------------------- result: true c-rewrite time: 308ms parse time: 1ms BOBJ> q Bye.

5. Double Negation

We conclude with the simplest example, doubly negating a stream of Boolean values; no additional circularities are generated beyond the initial equation to be proved.

5.1 Source Code

bth NEG is pr STREAM[BOOL] . op neg_ : Stream -> Stream . var S : Stream . eq head neg S = not head S . eq tail neg S = neg tail S . end set cred trace on cred neg neg S == S .

5.2 Output

========================================== bth NEG ========================================== c-reduce in NEG : neg (neg S) == S using cobasis for NEG: op head _ : Stream -> Bool [prec 15] op tail _ : Stream -> Stream [prec 15] --------------------------------------- reduced to: neg (neg S) == S ----------------------------------------- add rule (C1) : neg (neg S) = S ----------------------------------------- target is: neg (neg S) == S expand by: op head _ : Stream -> Bool [prec 15] reduced to: true nf: head S ----------------------------------------- target is: neg (neg S) == S expand by: op tail _ : Stream -> Stream [prec 15] deduced using (C1) : true nf: tail S ----------------------------------------- result: true c-rewrite time: 98ms parse time: 3ms ==========================================

To BOBJ examples homepage
To Tatami project homepage

Maintained by Joseph Goguen
Last modified: Sun Aug 17 19:17:06 PDT 2003