Proof-Program equivalence in the natural sciences

April 29, 2021

Introduction:

There is a general impression in the computational biology community that theories of computation are both difficult to understand and useless. I believe this situation is partly due to gaps in the general education of computational biologists. This may be filled by motivating theoretical neuroscience from a biological perspective [1] as well as reading a book on the history of computation where each advance is carefully justified.

However, for those computational biologists that would like a short introduction I prepared this article which focuses on insights and intuitions. Starting with function composition, which all scientists are familiar with, I show that proof-program equivalence is a natural consequence. I then show that there is a direct correspondence between this functional approach to computation, from the perspective of a mathematician, and Turing Machines, developed from the perspective of a stored-program computer.

A natural definition of computation:

If we define an approximate bijection between the sequence of mathematical operations \(f = \{f_i\}_{i=1}^n\) of a function \(f\) with \(\text{Dom}(f) = X\) and \(\text{Im}(f)=Y\), such that for any \(x_0 \in X\):

\begin{equation} x_1 = f_1 \circ x_0 \end{equation}

\begin{equation} x_2 = f_2 \circ x_1 \end{equation}

\begin{equation} f \circ x_0 = f_n \circ x_{n-1} \end{equation}

and the sequence of mathematical operations \(g = \{g_i\}_{i=1}^n\) on a system state \(z_0 \in Z\), carried out by an engineered system:

\begin{equation} z_1 = g_1 \circ z_0 \end{equation}

\begin{equation} g \circ z_0 = g_n \circ z_{n-1} \end{equation}

then we say that \(x_n\) is an encoding of \(z_n\), and \(g\) evaluated at \(z_0\) computes the operation \(f\) at \(x_0\).

We note that if the physical operation of the program halts at step \(n\), then the program returns its state at that instant:

\begin{equation} z_n = g_n \circ z_{n-1} \end{equation}

and in this setting, a finite loop is a sequence of functions \(\{f_i\}_{i=1}^n\) where \(n < \infty\) and:

\begin{equation} \forall i,j \in [1,n], f_i \equiv f_j \end{equation}

At this point we may make a couple useful observations:

\(1.\) There are no infinite loops in a physical system as every physical computer runs on a finite amount of energy.

\(2.\) Biological systems address energy constraints via a complex combination of heuristics that are used for estimating the appropriate stopping time. In the real world, energy is a more important resource than time which is at most a proxy measure for energy. In any case, stopping criteria are an approximate solution to the halting problem in the real world [3].

Type theory and proof-program equivalence:

Now, we note that the physical operation \(g_i\) and \(g_{i+1}\) compose with each other only if they share the same units so all physical equations define a type restriction:

\begin{equation} \text{Type}(\text{Im}(g_i)) \equiv \text{Type}(\text{Im}(g_{i+1})) \end{equation}

so \(g = \{g_i\}_{i=1}^n\) defines a path through a space of scientific units which may be modelled as a particular topological space [2].

For concreteness, let’s suppose we would like to perform a back-of-the-envelope calculation to verify the proposition that the total mass of ants is approximately equal to the mass of humans:

\begin{equation} \text{P} := M_{\text{ants}} \approx M_{\text{humans}} \end{equation}

where approximate equality is defined as a difference of less than one order of magnitude:

\begin{equation} \frac{1}{10} \leq \frac{M_{\text{ants}}}{M_{\text{humans}}} \leq 10 \end{equation}

To perform a verification, i.e. the proof, we need a certain number of observables that are measurable(i.e. our assumptions).

\begin{equation} \text{Ant axioms} := \text{Number of ants}, \text{Average mass of an ant} \end{equation}

\begin{equation} \text{Homo sapiens axioms} := \text{Number of humans}, \text{Average mass of a human} \end{equation}

where we have distinct types for number(Integers) and mass(kilograms). It follows that we may define the input:

\begin{equation} z := (N_{\text{ants}}, N_{\text{humans}}, m_{\text{ant}}, m_{\text{human}}) \end{equation}

\begin{equation} g = g_2 \circ g_1 \end{equation}

\begin{equation} g_1 \circ z = \frac{N_{\text{ants}} \cdot m_{\text{ant}}}{N_{\text{humans}} \cdot m_{\text{human}}} \end{equation}

and using Boolean arithmetic we have:

\begin{equation} g_2 \circ g_1 = \text{Bool} \circ (g_1 \circ z \geq \frac{1}{10}) + \text{Bool} \circ (g_1 \circ z \leq 10) \end{equation}

and if we carry out the calculation, we find:

\begin{equation} g \circ z = 1 \end{equation}

So our constructive proof defines a program. It follows that within the realm of scientific computation(a subset of constructive mathematics) the notions of proof and program are equivalent.

Turing machines for simulating physical systems:

The functional perspective that has been introduced so far has been formalised as the Typed Lambda calculus which allows us to reason about the semantics of computation. This perspective is essential because computations are not observer independent. On the other hand, Turing Machines are an equally powerful model of computation that emerge naturally from the perspective of a stored-program computer. They offer a complementary perspective as they allow us to reason about the mechanics of computation from the perspective of a computer. In particular, they allow us to analyse the computational complexity of algorithms. Moreover, a direct correspondence between the two perspectives is relatively simple to establish.

In order to simulate a finite sequence of mathematical operations \(\{f_i\}_{i=1}^n\) applied to \(x_0 \in X\) on a realistic computing device, let’s assume each state transition \(x_n = f_n \circ x_{n-1}\) has a binary encoding, each \(f_i\) has a binary encoding and each state \(x_i \in X\) has a binary encoding. It follows that we may refer to both functions and their variables \(x \in X\) as mathematical symbols.

As all physically realisable computers have a finite amount of memory and at any instant the sequence of operations only depends on the state \(x_{n-1}\) and the function \(f_n\) being applied to it, we may model this process using a length of tape with countably many slots. We may imagine that each state transition is encoded by moving to the right on a finite length of tape and printing a sequence of ones and zeros with blank symbols(\(\emptyset\)) between adjacent encodings of mathematical symbols.

Likewise, in order to define the next state-transition \(f_{n+1} \circ x_n\), the computer must go back by moving to the left in order to replace the previous digits(our symbols) with new ones so the current sequence of symbols is in agreement with the binary encoding of \(f_{n+1} \circ x_n\). (This corresponds to what computer scientists call garbage collection, an automatic form of memory management.)

It follows that we generally need a finite set of mathematical symbols which is a subset of the set of binary sequences with the empty symbol(\(\emptyset\)):

\begin{equation} \Sigma \subset \{0,1\}^* \cup \emptyset \end{equation}

a set of states which in our case is a subset of the set of binary sequences as each state-transition \(f_n \circ x_{n-1}\) is identifiable with a distinct state \(x_n\):

\begin{equation} X \subset \{0,1\}^* \end{equation}

an initial state:

\begin{equation} x_0 \in X \end{equation}

as well as final states i.e. termination criteria for the program:

\begin{equation} \bar{X} \subset X \end{equation}

and our sequence of functions may be replaced by the mechanically-operated transition function:

\begin{equation} \delta : (X \setminus \bar{X}) \times \Sigma \rightarrow X \times \Sigma \times \{\text{Left}, \text{Right}\} \end{equation}

where \(\delta\) is generally a partial function due to the fact that the Halting problem is undecidable. Now, we may make a couple useful observations.

First, given a particular discrete-time dynamical system there exists a Turing Machine which may be used to simulate that system. Second, there are countably many Turing Machines. This means that if we can simulate \(n-1\) discrete-time dynamical systems with \(n-1\) distinct Turing Machines then we may identify the nth Turing Machine with a computer which may be used to simulate any of the \(n-1\) dynamical systems. By induction, there exists a Turing Machine which may be used to simulate all the other Turing Machines.

We may call such a Turing Machine the Universal Turing Machine and we may identify it with the Universe itself which is actively being used to simulate every physical process we observe [6]. In the Universe, garbage collection happens in real time via competition for finite resources.

Discussion:

Some scientists appear to struggle with the notion of an unbounded length of tape. But, I’d like to point out that this is not so different from an arbitrarily large envelope for back-of-the-envelope calculations. More importantly, a good understanding of the Church-Turing thesis is essential for all natural scientists because it defines the epistemic limits of the scientific method itself.

All physical systems at present are modelled within a mathematical framework that is consistent with Peano Arithmetic(PA) for combinatorics and algorithm design, first order logic for mathematical reasoning and proof verification, and a theory of types that is implicitly necessary for physical equations to make sense. This means that human scientists and the models they define operate within the confines of the Church-Turing thesis.

On the other hand, if physicists reasoned within a mathematical framework that was inconsistent with PA then scientific induction would no longer be possible. So they might develop theories but they would not be testable. It follows that if computational neuroscientists build a testable model of the brain, this model must be within the Turing limit. In a very precise sense the limits of our language define the limits of our world, but the language of mathematics is also unmatched in its expressive power as observed by Wigner [4].

In order to transcend these epistemic limits we may need to build more powerful computers using principles of black-hole engineering [5]. In the not-too-distant future, this will allow scientists to use scientific methods that are beyond the Turing-limit and therefore strictly more powerful than the ones we currently use.

References:

\(1.\) Hessameddin Akhlaghpour. An RNA­-Based Theory of Natural Universal Computation. Arxiv. 2020.

\(2.\) The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton University. 2013.

\(3.\) Thomas S. Ferguson. Who Solved the Secretary Problem? Statistical Science, Vol. 4, No. 3 (Aug., 1989), pp. 282-289

\(4.\) Eugene Wigner. The Unreasonable Effectiveness of Mathematics in the Natural Sciences. 1960.

\(5.\) Hajnal Andréka et al. Closed Timelike Curves in Relativistic Computation. 2011.

\(6.\) Aidan Rocke (https://cstheory.stackexchange.com/users/47594/aidan-rocke), Understanding the Physical Church-Turing thesis and its implications, URL (version: 2021-02-22): https://cstheory.stackexchange.com/q/48450

Proof-Program equivalence in the natural sciences - April 29, 2021 - Pauli Space