Everything Is a Program - Chapter 3 - Types

Original post: here.

In the 0th post of this series we provide a definition of a program.

Def. Program - a set of sequences

In the last post (2nd post) we discussed how all properties of programs are also programs. But, if you will notice we nearly contradicted the entire purpose of this series of explaining away everything as a program when we mentioned that you could view hyperproperties not as programs but rather as a set of programs.

In this post, we want to clear up any potential misconceptions and discuss how all collections of objects are also programs. And thus, even a hyperproperty as a set of programs can still be a program itself.

We will discuss "collections of objects" in terms of "Types" since this is the more common terminology found in computational jargon/rhetoric (although theoreticians will often utilize sets) especially by practitioners (i.e. engineers).

You will notice though that our initial definition of a program relies on the existence of the notion of a set. Thus, there is some circularity in our discussion here, but instead of trying to define a mathematical foundations program (as I prefer to not even attempt to integrate Gödel) based on seeing everything as programs, we are merely attempting to framework discussions for artificial biology research.

In artificial biology research we are dealing with systems of such immense complexity that need to be understood bottom-up and constructed from scratch that establishing useful foundational concepts seems to be a hard requirement.

Thus, in this post, we attempt to establish how even the set in our original definition of what a program is, can always be looked at and utilized as a program.

Types

Let's begin by defining what a "Type" is for this discussion.

Def. 5 - Type - a set of terms (objects), for which every term is qualified by some qualifier, and that there is a decidable relationship (qualification) between each term and the Type qualifier.

There is minimal difference between sets and Types. It's looking at the same platonic & esoteric object in two different ways: a collection. However, we will avoid diving into the differences between various set theories and type theories here. It's good enough for the objectives of this piece of writing to simply understand a Type as a formalized view of collections.

We actually introduce a couple of our own theoretical concepts to quicken the pace of our discussion. For example, what is a Type qualifier and how does it qualify the terms of the Type? The qualifier is, simply put, any object. The qualification judgment is said to be up to an interpreter. Each qualification should be thought of as a program which represents an inductive/deductive derivation of the term from the qualifier or vice versa. In other words, a qualification is often what we, as humans, would call a proof (but, perhaps closer to what we would socially call a "story" rather than the much more heavily restricted "mathematical proof").

Thus, the architecture of the theoretical entity we call a Type is a 3-tuple $\langle Q, \Sigma,\Tau\rangle$, where $Q$ is the Qualifier, $\Sigma$ is the set of qualification proofs, and $\Tau$ are the terms.

The decidability property of qualification proofs emphasizes that something (or someone) -- the "interpreter" -- is supposed to run the qualification program/proof and that it is supposed to terminate i.e., it must be decidable by whatever/whomever is running it. This decidability property is what actually makes an object a term of a Type. The interpreter must be able to decide that the particular object is provably of that Type (again where "proof" is left up to the interpreter, but the fact of a decision being made one way or the other is a more 'universal' requirement).

Perhaps, what is most interesting is that every term in a type is a program - they are 1-sequence programs i.e. programs of length 1. But, what is even more interesting is that the type itself is also a program. The Type itself is a set of sequences as defined in the 0th post of this series.

Thus, all terms in a type are single-term sequences. And types are a program composed of a set of single-term sequences.

Contexts

For the sake of our discussion we will mention two important points:

1. All programs can be Typed (and in many different ways), as in program $p$ is a term of Type $T$, commonly written as $p:T$.
2. All programs can be re-defined as a sequence of terms from some set of Types $\Gamma_{t}$.

Def. 6 - We call $\Gamma_{t}$ the Context of the program at time $t$.

We will not explain in detail why here, but noting that a program has a context and that it is only valid for some time (duration) is very important (hint: because a Context can change).

A context can also have certain characteristics that can be useful to define. For example, the Types in a context can share terms or they cannot share terms dependent on the qualifiers and derivations that are utilized.

Thus, we differentiate between Contexts where Types share terms and Contexts where Types do not share terms.

Def. 7 - Well-Typed Context ($\Gamma^{\omega}_{t}$) - The Types in the Context do not share any terms. This includes a lack of any "polymorphic" Types (e.g., Kinds).

Interpreter-Defined Properties

Since, a program can be Typed, we can view the qualifier of the Type that the program is a term of as a subset of the properties of that program.

This can be illustrated simply: if we have a qualifier "all short programs", then all terms qualified would be programs that the interpreter considers (subjectively) to be "short".

This ties back into our discussion on properties as programs. In that post we discussed a much more formal framework where programs are related based on shared sequences. But here, in this post, we are also arguing for an informal methodology of generating properties by allowing properties to be defined and hold up to an interpreter.

But note: an "interpreter" could here be a human, machine architecture, programming language, hardware device, etc. So, while properties, formally defined, provides a shareable (and thus more objective) way to discuss programs, it is not necessarily "wrong" to utilize this subjective framework of interpreter-defined properties for typing programs as well.

There are two basic relationships we will discuss between qualifiers, as a list of some subset of interpreter-defined properties of a program, and programs as the terms that are qualified by that list i.e. programs with said properties.

Of course, these relationships, being between a qualifier and a term, are derivations (i.e. the qualification judgements/stores/proofs).

Def. 8 - Complete Type - all programs $p_{i}:T$ have all the listed properties in the qualifier.

Def. 9 - Exact Type - every program $p_{i}:T$ has only the listed properties in the qualifier.

For example, each of the Types in a well-typed context $\Gamma^{\omega}_{t}$ are always complete, but not necessarily exact.

Def. 10 - Perfectly-Typed Context ($\Gamma^{\phi}_{t}$) - a set of complete and exact Types. Where the list of properties in each Type qualifier is met completely by every program qualified, and those are the only properties of every program qualified.

The possible executions (the sequences) of Turing Programs discussed earlier( could be considered well-typed but not perfectly-typed. There is no set of properties that every possible sequence in a Turing Program satisfies completely and exactly.

Conclusions

We could carry on for pages and pages with this discussion, but this post is not really that important. This is yet another post in this series to provide validity to the reductionist assertion that beginning to frame artificial biology research in terms of "programs" and "programmatic concepts" will be fruitful. And, in fact, it will prove more fruitful than other formalizations.

We have already drawn relationships to phase spaces, phase transitions, and thus general thermodynamics in a prior post on machines.

We have drawn relationships to most of computer science and now foundational mathematics.

The frame of "everything is a program" is proving itself powerful. And we want to soon begin framing actual biology and theoretical biology with what we have been deriving in this series.

Hopefully, you can begin to see where we are headed. But, if not then that is perfectly ok too because we will spell it out as explicitly as possible on this blog and elsewhere.

Put simply, the future of biology and computation are one and the same.

Series

Find the entire series here!