Ok, if we disallow cycles of outermost function calls, then it seems the trees are indeed infinite only in one direction. Here’s a half-baked idea then: 1) interpret every path from node to root as a finite word 2) interpret the tree as a grammar for recognizing these words 3) figure out if equivalence of two such grammars is decidable. For example, if each tree corresponds to a regular grammar, then you’re in luck because equivalence of regular grammars is decidable. Does that make sense?
Yeah, that makes sense. And off the top of my head, it seems like they would indeed be regular grammars—each node in the tree would be a state in the finite state machine, and then copies of the tree would produce loops in the state transition graph. Symbols on the edges would be the argument names (or indices) for the inputs to atomic operations. Still a few i’s to dot and t’s to cross, but I think it works.
Ok, if we disallow cycles of outermost function calls, then it seems the trees are indeed infinite only in one direction. Here’s a half-baked idea then: 1) interpret every path from node to root as a finite word 2) interpret the tree as a grammar for recognizing these words 3) figure out if equivalence of two such grammars is decidable. For example, if each tree corresponds to a regular grammar, then you’re in luck because equivalence of regular grammars is decidable. Does that make sense?
Yeah, that makes sense. And off the top of my head, it seems like they would indeed be regular grammars—each node in the tree would be a state in the finite state machine, and then copies of the tree would produce loops in the state transition graph. Symbols on the edges would be the argument names (or indices) for the inputs to atomic operations. Still a few i’s to dot and t’s to cross, but I think it works.
Elegant, too. Nice solution!
I’m actually not sure it’s a regular grammar. Consider this program:
Which gives the tree
The path from any 1 to the root contains a bunch of minuses, then at least as many pluses. That’s not regular.
So it’s probably some other kind of grammar, and I don’t know if it has decidable equivalence.