University of Sussex Spring 2021 Informatics
Limits of Computation
Feedback for Exercises 4 Dr Bernhard Reus
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.
Answer:
decisionProc read X { switch X {
case 4: result:= true case 6: result:= true case 8: result:= true default: result := false }
}
write result
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.
Answer:
dpF read X switch X case d1: case d2:
{
{
result:= true result:= true
case dn:
default: result := false }
}
write result
Note that in hwhile we can directly inject trees d as tree literals, an extension of pure WHILE (we have not discussed in detail).
1
.
result:= true
One way is to construct them explicitly with cons and nil in WHILE.
Clearly, dpf always terminates. It is also rather obvious that it returns true if and only if, the argument X is equal to one of thedi inA(for1≤i≤n). AndbydefinitionofAthismeans thatdpF(d)=true if,andonlyif,d∈Aforanyd∈D.
Another solution (some students always suggest) would be to convert the set A of binary trees into a list and then run through this list as follows:
test2 read X {
A:= [d1,d2,…,dn]; while A {
Y := hd A; if X=Y {
result := true; A := nil
}
else {A:=tlA }
} }
write result
// loop exit
Again di means the representation of element di ∈ D in a WHILE-program. It is important to understand, however, that the list of elements is not an argument of the decision proce- dure. It is supposed to test membership in this (fixed) set.
In the seminars, students often wanted to make A the parame- ter of the decision procedure, but this is wrong. The decision procedure is for deciding membership in A. Its argument is an arbitrary tree for which we want to know whether it is in A or not!
3. Show that, if A ⊆ D is WHILE-decidable then so is the comple- ment 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.
Answer:
Assume A ⊆ D is decidable. Thus, there is a program p that decides A. This means in particular that p always terminates. Now let us construct a program q that decides D\A, the com- plement of A, as follows:
2
q read X {
Y :=
X;
ifY {
result := false
} else
{
result := true
}
}
write result
We obviously get that q always terminates, since p does. We also see quickly that q (d) = true if, and only if, p (d) ̸= true and therefore d ∈ D\A iff d ∈/ A, which is exactly what we need.
4. Why is any WHILE-decidable set automatically WHILE-semi-decidable.
Answer: Because a decision procedure is automatically a semi- decision procedure by definition. It is one that alsways termi- nates.
5. Write a WHILE-program equal that does not use the built-in equality (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 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])
3
(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 it can relatively straightforwardly be transformed into a while loop like so ….
Answer: See also file equalsG.while on Canvas (program section).
equalG read L {
res := true;
// traverse along the list
while L {
X:= hd L; // first pair of trees
s := hd X;
t := hd tl X;
if s {
if t { // both are not nil so continue
L:= cons [hd s, hd t] cons [tl s, tl t] tl L
}
// snotnilbuttis { res := nil;
L :=nil }
else
}
else { // s nil but it isnt’t
if t { res := nil;
L :=nil
}
else // both s and t are nil
{ L := tl L
} }
} // while }
write res
4