🚀 go-pugleaf

In article <2554@randvax.UUCP> narain@randvax.UUCP (Sanjai Narain) writes:
|Of course, the difficulty of reasoning about non-deterministic algorithms
|depends upon the algorithm. What I said was that by expressing these
|in logic, one can reason about them the same way as one reasons about
|other sentences in logic. For example, it is quite easy to show that
|the following non-deterministic program:
|
|	subset([],[]).
|	subset([U|V],Z):-subset(V,Z).
|	subset([U|V],[U|Z]):-subset(V,Z).
|
|will compute exactly 2**n subsets of a set of length n (represented as
|a list), and whose complexity is O(2**n) SLD-resolution steps.

I don't understand. I don't expect this program to terminate for the
query

	subset(X,1)

so perhaps it is not so easy to show? Or if so, how?

	Tom