Skip to main content

Graph Fever Dream

I did not have/remember dreams when I was a young adult, perhaps because I did not sleep enough during that time of my life, but I have gotten pretty good at remembering dreams since then. I am in some dreams, but I am not in others. Many of my dreams are in Japanese, even those that take place at a time when I did not speak Japanese, and even my mother speaks Japanese in such dreams. Some dreams are first person, some are third person (like watching a movie), and others are completely abstract (with no people in them at all). Some dreams are related to my experience and/or thoughts, while others are completely unexpected. Perhaps random neuron firing results in such a wide variety of dreams.

It is extremely common for software developers to dream about their work. When you are focusing on a difficult problem, it makes sense that it is likely to come up in a dream. It is also quite common to gain insight on a problem in a dream, sometimes significant enough to enable progress. Not all such dreams are helpful, of course; some are absurd.

I recently caught a cold from one of my daughters, and there were two nights with high fever. Unable to sleep well, I woke often and remembered many dreams. One has stuck with me. It was one of those abstract dreams with no people in it.

I have been thinking about API design at work, and that is how the dream started. A two-dimensional sparse matrix was created to represent an API, with one dimension representing API methods and the other dimension representing parameter types. It was unclear how to represent return value types. Attempting to make use of the matrix led to frustration, so it was discarded in favor of a directed graph. After a short time, the topic of modeling an API was discarded in favor of mathematical proofs.

The core of the dream was about mapping mathematical proofs using a directed graph. Each axiom, theorem, and hypothesis is a node in the graph, and there are arrows from all axioms, theorems, and hypotheses used to prove a theorem. Such a graph might be useful, and I would be surprised if somebody has not already worked on creating one.

One aspect of the graph that I find interesting is that it is not acyclic. Sometimes there is a set of theorems for which any one of them can be used to prove the others. This is a topic that we have discussed in the Software Foundations study group!

For example, the law of excluded middle comes up quite often. Coq is based on the calculus of constructions, where proofs are implementations of theorems, à la the Curry-Howard isomorphism. The law of excluded middle (p ∨ ¬p) therefore only holds for propositions that are decidable.

The law of excluded middle is closely related to other theorems such as the principle of double negation (p ↔︎ ¬¬p) and (half of) De Morgan’s laws (¬(p ∧ q) ↔︎ ¬p ∨ ¬q). Any of these theorems can be used to (easily) prove the others. For example, if working with propositions that are known to be decidable but not easily proved decidable, one could take the law of excluded middle as an axiom and easily prove the principle of double negation and De Morgan’s laws. Alternatively, one could take the principle of double negation as an axiom and use it to prove the others, etc. Such relations between theorems produce cycles in the graph.

Author

Travis Cardwell

Published

Tags