# 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

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.

## 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.

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