CTM: Exercise 3-14
[ Posted by Urban Hafner ]
The problem
FIFO queues. Consider the FIFO queue defined in section 3.4.4. Answer the following two questions:
(a) What happens if you delete an element from an empty queue?
(b) Why is it wrong to define IsEmpty as follows?
fun {IsEmpty q(N S E)} S==E endMy solution
There is no queue definition in 3.4.4, so I used the worst-case constant-time ephemeral queue because it is represented as a tuple q(N S E).
Consider adding a to the empty queue q(0 X X) using {Insert Q X}. What we get is the new queue q(1 a|E1 E1). Using the definition of IsEmpty from above blocks because the entailment check can’t decide. Deleting an element from the queue returns the queue q(0 E1 E1). Here our IsEmpty works. But it’s of course quite bad when we can use IsEmpty only when we already know that the queue is empty :)
