🚀 go-pugleaf

# |
# |     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

The SLD-search tree for the query subset([a1,..,an],Z), Z a variable, will
consist of O(2**n) branches. Let this number of branches be F(n).
Then, F(n+1)=2*F(n)+2. This is because the query subset([a1,..,an+1],Z)
yields two branches, each ending in subset([a1,..,an]). Solving this
recurrence yields F(n) = 3*2**n - 2. Correctness can be proved similarly,
in particular, by observing that each statement is a correct fact about
the subset relation.

Sanjai Narain