Definition
Exhaustive enumeration is a method of computation or proof in which one solves a problem by systematically considering every element of a finite search space.
Given a finite set , a computable function , and some operation or predicate depending on the values of , one can compute all values of by enumerating the elements of : and forming the finite table:
Any computable operation on this finite table can then be evaluated directly. In this way, a problem about a function is reduced to a problem about a finite list of values.
Terminology
This method is known by several names depending on emphasis:
- Exhaustive enumeration: Listing all cases
- Exhaustive search: Searching for an element satisfying a condition
- Brute-force computation: Algorithmic emphasis
- Finite case analysis: Proof-theoretic emphasis
- Tabulation: Representing a function extensionally by its values
Truth Tables
Truth tables are a standard example. To decide whether a propositional formula is a tautology, one enumerates all possible assignments of truth values to its variables, evaluates the formula under each assignment, and checks whether the result is true in every case.
General Principle
Exhaustive enumeration applies whenever the relevant input space is finite and effectively enumerable. Its usefulness comes from the fact that over a finite domain, a function can be represented by the finite table of its values. Questions about the function can often be answered by inspecting this table.
A typical schematic form:
Enumerate , compute for each , and aggregate the resulting finite family:
If the aggregation step is computable on finite data, then the whole procedure is computable.
Limitations
The important caveat is that finiteness of makes the graph of finite, but it does not make an arbitrary meta-level operation on computable. What exhaustive enumeration provides is a finite representation of the relevant data; any further computation still depends on having an effective method for processing that finite representation.