Directed spaces and types#
Joint work with Jin Xing Lim, Liang Ze Wong, Georgios Piliouras.
There is a concept of Directed Spaces. Since Types can be thought of as Spaces, the question is what kind of additional information we would need to construct such a Type (e.g. for undirected types, we can construct these types using identity types as additional information).
I am interested in the study of directed types because of computer-assisted theorem proving. In theorem proving, suppose we have a proposition/type Q that we are trying to prove, and we have a lemma that \(P\rightarrow Q\). Then we can apply this lemma, and attempt to prove P instead. However, it is possible that Q is true/inhabited but P is not.
The situation here is different from proving equalities using a given set of rewrite rules. In the case of equalities, if we have an equality \(Q=Q'\) that we want to prove, and we have a rewrite \(P \leftrightarrow Q\), then \(Q=Q'\) is true if and only if \(P=Q'\) is true. For the proof of equalities, we have Knuth-Bendix theory to help us. For the proof of propositions or the construction of terms of types, such a symmetric theory may not be as well-suited.
The directed path types in directed types (as opposed to path types for undirected types) will satisfy reflexivity (\(x\rightarrow x\)) and transitivity (if \(x\rightarrow y\) and \(y\rightarrow z\), then \(x\rightarrow z\)) but not symmetry (if \(x\rightarrow y\), then \(y\rightarrow x\)). This is similar to the case of judgments in logical frameworks, although that is not surprising because logical frameworks formalize the deduction of judgments. The more interesting question is how the design of logical frameworks is influenced by the nature of directed types.
More specifically, let some universe \(U\) of types be the space that we are studying. The points of this space are propositions and types. We have a directed path from some \(T\) to \(T'\) if there exists a lemma \(T \rightarrow T'\). Let \(\textbf{1}\) be the unit type, which is a terminal object in the space of types. We say that a type \(T\) is inhabited if there is a function \(\textbf{1} \rightarrow T\). Unpacking this definition, \(T\) is inhabited if it is an inductive type (i.e. a basic defined type), an axiomatic type (i.e. assumed to be inhabited), or connected from an inhabited type by a directed path (i.e. if \(T\) is inhabited and \(T \rightarrow T'\), then \(T'\) is inhabited). Let \(T^*\) be the type for which we are constructing a term. The goal is to construct a directed path from \(\textbf{1}\) to \(T^*\).
Unlike the story of equality proofs and rewrite rules, we do not get critical pairs since the paths are directed, unless we have equivalences \(T \leftrightarrow T'\). However, one issue is that of unification. Let \(S, T\) be two types that unify. If one of the definitions in \(S\) is unfolded, the new expression \(S'\) may no longer unify with \(T\).
In fact, I would argue that equivalence is the only issue standing in the way of efficient proof automation. The unfolding of definitions is a form of equivalence. The beta or eta conversion of terms is another form of equivalence. Reflections between propositional predicates and boolean predicates are also equivalences, as are if-and-only-if statements. Given a lemma \(P \rightarrow Q\), every equivalence \(Q \leftrightarrow Q'\) gives rise to another equivalent lemma \(P \rightarrow Q'\). Given a goal \(T x\), every Leibniz’s equality \(x=x'\) gives rise to an equivalent goal \(T x'\). These equivalences lead to a profusion of lemmas needed for proof automation and time wasted in running through them for potential proofs. Therefore, we need to return to the Knuth-Bendix algorithm for a way to construct normal forms for these equivalences, so that fewer lemmas need to be checked during proof automation. From the point of view of finding directed paths through a space, we are using equivalences to reduce the size of the space by homotopy, so that the path search will be more efficient.
As a case study, consider the solution of systems of polynomial equations with real coefficients. Suppose we are interested in finding out if a particular system has any real roots. This is analogous to the more general question of whether a type is inhabited. We could simply find all the complex roots, and check if any of them are real. However, this depends on the assumption that the equation \(x^2+1 = 0\) has a root \(i\). We can think of this assumption as an axiom that the type \(\{ x \in k\vert x^2+1 = 0 \}\) is inhabited, where \(k\) is our base field. With this axiom, we get an equivalence (up to Nullstellensatz) between polynomial systems and sets of points in complex space, which then makes it easy for us to check in particular if there are any real roots. However, the work required to extend the axiom that \(x^2+1=0\) has a root, to this equivalence between systems and sets, is called the Fundamental Theorem of Algebra. The proof of the theorem is not straight-forward - if we only consider algebraic proofs (with just a little bit of basic real analysis), the proof is an exercise in Galois Theory. Thus, if we were working on a particular polynomial system and found ourselves needing the axiom to complete the proof, it is not merely enough to add this axiom to the proof engine and hope that future proofs will automatically learn how to use it. We need to extend the axiom into an equivalence for our polynomial systems, so that the proof space of directed paths can be simplified drastically.
Directed spaces are related to \((n,r)\)-categories, and in particular, \(\infty\)-categories. Directed spaces give rise to streams and coinductive types, which contain more structure and fit nicely with categorical considerations. It makes sense to view directed types through the lens of coinductive types and their corresponding identity types.
Directed spaces are naturally related to posets (partially ordered sets) where the partial order satisfies reflexivity and transitivity but not symmetry.
Directed types are related to goal trees, where root represents the main goal, and the leaves represent subgoals which, when inhabited, would imply that the main goal is inhabited