University of Sussex Spring 2021 Informatics
Limits of Computation
Exercises 4
WHILE-programs, WHILE-decidability, WHILE-computability (Lectures 7–9)
1. By writing a WHILE-program, show that A = { 4, 6, 8 } ⊆ D is WHILE-decidable. Test your program by running it in hwhile.
2. Show that any finite set A ⊆ D is WHILE-decidable.
Hint: assume without loss of generality that the finite set has n elements A = { d1, d2, . . . , dn } and write the decision procedure for this A. You can’t run it, of course, until you know what the elements d1, d2, . . . are.
3. Show that, if A ⊆ D is WHILE-decidable then so is the complement of A, that is D\A.
Hint: assume A is WHILE-decidable and thus we have a WHILE- program p that decides A. Now write a WHILE-program q that decides the complement of A. Of course, you can and should use p.
4. Why is any WHILE-decidable set automatically WHILE-semi-decidable.
5. Write a WHILE-program equal that does not use the built-in equal- ity (but can use all other extensions). The program equal takes a list of two trees [l,r] and tests whether the trees are equal, i.e. whether l = r. The function equal can be defined recursively as follows:
equal([nil, nil]) = true
equal([nil, ⟨ l.r ⟩]) = false
equal([⟨ l.r ⟩, nil]) = false
equal([⟨ l.r ⟩, ⟨ s.t ⟩]) = equal([l, s]) ∧ equal([r, t])
Unfortunately WHILE does not provide any recursive features. So your implementation has to traverse both input trees using a
1
while-loop. One way to do this is to generalise the equality test to stacks of pairs of trees represented as a list of pairs of trees:
equalG([]) = true
equalG([[nil, nil], S]) = equalG(S) equalG([[nil, ⟨ l.r ⟩], S]) = false equalG([[⟨ l.r ⟩, nil], S]) = false equalG([[⟨ l.r ⟩, ⟨ s.t ⟩], S]) = equalG([[l, s], [r, t], S])
(If the input list contains more than two trees, those following the first two shall be simply ignored.) One can now define
equal(L) = equalG([L])
The definition of equalG is a so-called tail-recursive definition which means that the recursive call is at the top level, which in turn means, it can relatively straightforwardly be transformed into a while loop like so:
equalG read L {
res:= true;
while L {
X:= hd L;
s := hd X;
t := hd tl X;
if s {
if t { …
} else {
… }
} }
write res
where some bits (represented by . . .) have been left out for you to fill in. Test your program in hwhile.
2