🚀 go-pugleaf

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.

An interesting question is this: why is it that algorithmic knowledge
can be expressed using definite clauses, but not using full first-order
logic (at least in any obvious way)?

Other logics in which one can express algorithmic knowledge are
equational logic, lambda calculus, and combinatory logic.

Sanjai Narain