## 2 Preliminaries
### Rapid Enumeration of Candidate Theories Over a Language \(\mathcal{L}\)  
Given an alphabet \(\mathcal{A}\) of symbols, such as operators and fields, a language \(\mathcal{L}\) is _recursively enumerable_ if there exists a Turing machine that will enumerate all valid strings in the language [9].  
By the _infinite monkey theorem_[10], the solution can be found--if the constants are limited to rationals--just by enumeration and validation. The goal of this section is to show a way of doing this enumeration in a tractable way that also finds the _most compact theory_.  
**Abstract enumeration.** Think of an alphabet \(\mathcal{A}=[A,B,C,\ldots]\) where any letter can appear once in a sentence and the length of the alphabet is \(n\). This is a simple combinatorial enumeration problem and the solution to the number of sets of size \(m\) (later \(m\) will be relabeled \(q\)) taken from \(\mathcal{A}\) is \(C(n,m)\). However, what if the symbols--letters--in the alphabet have different weights? What if the alphabet is more like \(\mathcal{A}=[A=1,B=1,C=4,D=4,E=4,F=4,G=7,H=7,I=7,J=7,K=4,L=19]\). This can dramatically decrease the enumeration size and the underlying motivation is shown below in the _decoder ring for electrodynamics_.  
The _TheoSea_ enumeration algorithm builds sets of increasing complexity \(q\), where \(q\) is the sum of the alphabet letter weights in a given candiate theory. It can be thought of as a form of depth-first iterative-deepering (DFID) [11] first formalized by [PERSON] in 1985. Optimality flows from a theorem by [PERSON]:  
**Theorem 1**.: _Depth-first iterative-deepening is asymptotically optimal among brute-force tree searches in terms of time, space, and length of solution._  
By length of solution, [PERSON] means the depth of the search where a solution is found. For _TheoSea_ compactness is the sum of the symbol weights along a potential solution branch in the search.  
It is perhaps easiest to think of the algorithm inductively. There is a data structure theos that holds all theorems (sets) of length \(q\) and it is built up from \(q=1\). The base cases are the singleton theories of a given complexity, so for the alphabet \(\mathcal{A}\), we have theos[1] = [A, B] and theos[4] = [C,...] and so on. Therefore, the base cases, such as \(q=1\) are all set; and then for \(q>1\), we use a \(q:l,m\) \"squeeze\". At step \(q\), consider all theories that can possibly be of length \(q\), _marching_\(l\) upward from and \(m\) downward from \(q-1\). The correctness is immediate by Korf 4.2 and the fact that \(q=l+m\) : too short theories are discarded (<\(q\)), and set elements are unique. More details can be found in [2].  
**Performance.** To test the performance, we run an experiment comparing the enumeration of \(\mathcal{A}\) (Fast) with the same set of letters but with unity weights (Slow), with a cutoff at \(q=14\). The total times are \(\text{Fast}=0.006\) s for the weighted \(\mathcal{A}\) above, and \(\text{Slow}=20.1\) s (the machine was a MacBook Pro (Retina, 13-inch, Late 2013) running a 2.8 GHz Intel Core i7 single-threaded using Julia 0.5). A graph is shown in Figure 1: _compactness matters._  
**Decoder ring for electrodynamics.** The underlying motivation was described above and here is the decoder ring; think of the electric and magnetic fields with the \(\mathcal{A}\) assignments of \(A=\mathbf{E}\) electric field, \(B=\mathbf{B}\) magnetic field...  
The Maxwell Equations are expressed in linear combinations of these terms as is described in Section 3.1. The complexity metric is just \(1+\) the number of space-time derivatives taken (Table 1).