We have excellent tools to create and edit text (vim, emacs, sublime, etc.). We have pretty good tools to create and edit tabular data (excel, other spreadsheet software). We even have pretty good tools to create and edit diagrams, pictures, and video.

Why don’t we have good tools to create and edit trees and graphs?

Trees and graphs (in the sense of connections between data) are the underpinnings of structured data. Virtually all data can be described in terms of vertices with (possibly directed, labeled, and/or weighted) edges between them. That may not be the best way of presenting it, but it works. For a variety of different types of data, it is indeed best to think in terms of the connections between the data.

Most often this is manifested in trees because our data is often hierarchical in nature. Thus it makes sense to focus on trees. Additionally, many graph structures can be viewed best by analyzing them through the “cross-section” that a tree view provides. This is all fairly abstract, so I think before I go any further I should give an example.

An Example: Constructing Proofs

I write math proofs on a fairly regular basis, and I read them even more often. Naturally, my mind has wandered to thoughts of how a computer could be used to write them more effectively, or at least make them easier to read and understand. The natural first step is first defining exactly what is a proof.

For the purposes of this discussion, a proof is the link between a series of hypotheses and a conclusion, such that if the hypotheses are true then the conclusion is true. I realize that not all proofs are simple implications (if-then), but most (all?) can be reduced to a series of implications. Thus, this is a reasonable characterization. A proof (in the abstract), looks something like this:

Theorem: If A, B, and C, then Z.

Proof: By Theorem T1, A and B implies D. By definition, C and D implies E. By Theorem T2, E and B implies F. Clearly, D and F implies Z.

This looks like a graph structure to me. Here is the structure (in various syntaxes):

Z
- D
-- A
-- B
- F
-- B
-- E
--- C
--- D
---- A
---- B

This is a fairly self-explanatory syntax. Note that there is some duplication since we are trying to project a graph onto a tree.

((A B) (B (C (A B))))

This “lisp-style” representation is compact and emphasizes the fact that the result only depends on A, B, and C, but it obscures some of the intermediate information.

                        A && B
                        ------  (T1)
                   C &&   D
                   -----------  (def)
      A && B  B &&      E
(T1)  ------  ----------------  (T2)
        D   &&       F
      ------------------------
                 Z

This gives more explicit information than the others, and gives it in a more visual way. Thus, it exposes the structure of the data.

There are countless other ways of giving the structure, and we haven’t yet even stepped outside the realm of ASCII. See this site for some more innovative visualizations.

Okay, so if we accept for the moment the hypothesis that proofs are structured data, and that in particular they can be represented well as a tree (or a graph), then it seems like we’re halfway there. After all, computer programs have been manipulating structured data for decades. The question I have is, what program would you use to write out a proof in such a way that it exposes the structure of the proof?

The usual way of writing a proof is in a linear, text-based format. This works well, but it doesn’t expose the structure of the proof, so it can be difficult to understand a proof on first read-through and even harder to get a general feel for the reasoning involved. If we want to write a proof in a tree-based or graph-based format, we need software that can help us. A minute ago I used a text editor to draw several views of a tree. There should be a piece of software that is more suited to drawing trees than a text editor.

Unfortunately, no such software exists. Or at least, not that I can find. If it does exist, please tell me. Seriously, I’d love to find out about it.

I want to be able to construct a proof by starting with “A && B && C” at the top of the screen and “Z” at the bottom. As I start finding things I can prove from A, B, and C, I can start adding nodes. Working backwards from Z, I can start creating different sets of sufficient conditions for Z. Thus, I have a tree growing from the top and a tree growing from the bottom. When they meet, the theorem is proved.

This doesn’t require the software to know anything about proofs or logic. I just need a sufficiently general tree/graph editor.

Another Example: Programming

If proofs aren’t your thing, let’s look at programming. Virtually all programming languages can be reduced to an abstract syntax tree (AST). In the Lisp family, the language is essentially a bare AST. The AST is represented using the parenthesis notation for trees, although it could just as easily be represented in other ways. So, if we had a general tree editor, we could write Lisp code directly in it. If it was a general graph editor then we could make connections between parts of the program that are not syntactically related (for example, connecting all uses of a particular variable or function).

Again, the major functionality here is simply a tree editor. For sure, to actually use this to write a program we would want to have a series of plugins that know that we’re writing Lisp and help us, just like a text editor. But the major functionality is the same as proof-writing – we’re just editing trees.

What I’m Looking For

The software I’m looking for is general purpose software. I’m not looking for a proof editor, nor am I looking for a tree-based programming editor. I’m looking for a platform.

In text processing we have text editors combined with plugins and syntax files and whatnot to create an environment suitable for the task at hand, be that writing a to-do list, writing proofs in LaTeX, writing a blog post, or programming. But the main functionality is that of simply editing text.

Analogously, I envision many plugins and whatnot to help with proof-writing or programming or whatever other tree manipulation we might want to do. But we first need the tree editor. We need a solid, simple program that can simply edit trees.

What would this look like? This is mostly pure speculation at this point, but here’s some ideas I have.

The program consists of a series of frames, each of which displays a (part of a) tree. There are many ways to visualize trees, so each frame may use a different visualization, or they may all use the same one. When a change is made to one frame the others immediately are aware of the change. Navigating through the tree(s) should be easy and quick. A good keyboard-focused mouse-optional interface would be important.

Plugins should be able to define additional visualizations and additional commands. These should include domain-specific ways of interacting with the data, just as commands and syntax highlighting do in text editors.

These ideas come to some extent out of a side project of mine. Phlisped is a graphical programming editor experiment that is on some level just a tree editor with a few extra things slapped on to make it work for programming. Some of my writings on the subject include a brief philosophy post, an announcement (includes screenshots) when I released the code, and a short video demo of a few of its features. In some sense, this would be a re-write, but with a more general purpose.

Conclusion

I haven’t written any code for this. This is really just a statement of a perceived lack. I plan to investigate the issue more, do some design, and see if I can write up a prototype, but I can’t give any guarantees. If only I had more free time…

I am interested, however, in any feedback. In particular, any examples of already-existing programs that fit part or all of this description would be useful. Most tree editing software is domain-specific, but if there are good examples of domain-specific tree editors, I’d love to hear about those as well. Any other feedback is also appreciated.