[12_throw_away]

> It can also be quite possible to invent structures which are valid but have no valid path to creating them.

I'm curious if you have an example of such a structure?

Pedantically: if, for every valid tree, there exists a bidirectional path to the empty root node, there's always at least one path between all given pairs of valid trees ... albeit one that no developer would ever take.

[Normal_gaussian]

You are quite right to call this out - and quite right in general. With AST verification alone your statement holds strongly.

I was remembering a professor I had who was very into formal verification and had an IDE that would only accept valid programs - however his validity checks were more than just tree based, they involved passing a type check. Which now you've called me on it, is quite definitely beyond valid AST editing.

The base case: if you have a structure with a mandated cyclical reference that doesn't accept a second (e.g. nil) type, you cannot construct it without creating an intermediate invalid program. This doesn't tend to show up if the cyclical reference is all the same type (A1 -> A2 -> A1) because you can often cheat and self reference, but it does if it is different types (A1 -> B1 -> A1). You can't construct an A without a B, which cannot be constructed without an A.

But that's still not a problem you cry! And quite right, you can edit the type itself to remove and re-add the reference.

That is until the type is built into the language, or a library.

[integralid]

OP clarified, but I understood that as a valid tree without a path to empty node. I don't have an example, but with grammar weird enough it sounds plausible. Especially if some form of type checking is involved, as OP mentioned.