Reading material
Pages 70-73.
Additional material
Simplification rules for a stack:
size(nil) ->> 0.
size(push(X, S)) ->> size(S) + 1.
size(error) ->> error.
empty(nil) ->> true.
empty(push(X, S)) ->> false.
empty(error) ->> error.
top(nil) ->> error.
top(push(X, S)) ->> X.
top(error) ->> error.
pop(nil) ->> error.
pop(push(X, S)) ->> S.
pop(error) ->> error.
Simplification rules for a queue:
size(nil) ->> 0.
size(add(X, Q)) ->> size(Q) + 1.
size(error) ->> error.
empty(nil) ->> true.
empty(add(X, Q)) ->> false.
empty(error) ->> error.
first(nil) ->> error.
first(add(X, Q)) ->> if(Q = nil, X, first(Q)).
first(error) ->> error.
drop(nil) ->> error.
drop(add(X, Q)) ->> if(Q = nil, nil, add(X, drop(Q))).
drop(error) ->> error.
Question
Exercise 5.14