I was a little confused by the case of substitution where you have > 1 box. It seems that this notation each substituted value is freely chosen at each box, rather being chosen once and duplicated across each box. That is, to use your own example, a(x,x)^{*,x} gives all the binary trees rather than the complete binary trees, and is equivalent to a(x, y)^{*,x}^{*,y}.
Yes! Substitution is freely chosen at each box, and it has to be, since the complete binary trees don't form a regular tree-language. Note that your examples leave x's at the leaves, which have to be replaced (via x-concatenation) by a's (or the empty tree-word, if we're allowing that)
22:50 doesn't that mean the language won't contain the empty tree? which I think should be accepted by the automaton would it make sense to instead define the kleine star over x as 1. formally add the character x 2. compute the set of (recursive) x-concatenations of whatever's in the parentheses 3. add the empty tree and remove any tree that contains x's
23:50 also, I find it interesting that because L1 is the complement of L0, we could just spell out the recursive formula for L0, and leave L1 defined simply as Σ*/L0 - I think this would be well defined, with words belonging to L0 being proven so with recursion, and words in L1 being proven so with corecursion (finding no inconsistencies in it being L1 should prove that it's L1)
My intuition is that concatenating the empty tree onto a leaf should remove that leaf, so you could just concatenate with the empty tree at the end instead of "a" to turn the single x from the Kleene star base case into the empty tree. We then just need to add a symbol for the empty tree singleton language to the possibilities for regular expressions. Adding in the empty tree greatly simplifies a lot of regular expressions: the set of all trees with alphabet {"a"} becomes ( a(x,x) )^{*,x} concatenated over x with the empty tree. The issue is that there don't seem to be any good sources on binary tree automata: I'm trying my best to adapt what is available on ranked tree automata, in which case the empty tree isn't particularly natural and so is omitted entirely, as opposed to the binary tree case where it is natural. As to whether the empty tree should be accepted by an automaton, just like with word automata it's a question of if the start state (or #) is an accept state or not.
I'm not really familiar with lambda calculus, but if I understand your question correctly: A tree with one "variable" (one occurrence of the temporary variable for concatenating into) is called a "context" and is really only relevant for the pumping lemma (and the Myhill-Nerode theorem, as we'll see). Note that the temporary variable occurs multiple times in some of the regular expression examples at the end.
I was a little confused by the case of substitution where you have > 1 box.
It seems that this notation each substituted value is freely chosen at each box, rather being chosen once and duplicated across each box.
That is, to use your own example, a(x,x)^{*,x} gives all the binary trees rather than the complete binary trees, and is equivalent to a(x, y)^{*,x}^{*,y}.
Yes! Substitution is freely chosen at each box, and it has to be, since the complete binary trees don't form a regular tree-language. Note that your examples leave x's at the leaves, which have to be replaced (via x-concatenation) by a's (or the empty tree-word, if we're allowing that)
22:50 doesn't that mean the language won't contain the empty tree? which I think should be accepted by the automaton
would it make sense to instead define the kleine star over x as
1. formally add the character x
2. compute the set of (recursive) x-concatenations of whatever's in the parentheses
3. add the empty tree and remove any tree that contains x's
23:50 also, I find it interesting that because L1 is the complement of L0, we could just spell out the recursive formula for L0, and leave L1 defined simply as Σ*/L0 - I think this would be well defined, with words belonging to L0 being proven so with recursion, and words in L1 being proven so with corecursion (finding no inconsistencies in it being L1 should prove that it's L1)
My intuition is that concatenating the empty tree onto a leaf should remove that leaf, so you could just concatenate with the empty tree at the end instead of "a" to turn the single x from the Kleene star base case into the empty tree. We then just need to add a symbol for the empty tree singleton language to the possibilities for regular expressions.
Adding in the empty tree greatly simplifies a lot of regular expressions: the set of all trees with alphabet {"a"} becomes ( a(x,x) )^{*,x} concatenated over x with the empty tree.
The issue is that there don't seem to be any good sources on binary tree automata: I'm trying my best to adapt what is available on ranked tree automata, in which case the empty tree isn't particularly natural and so is omitted entirely, as opposed to the binary tree case where it is natural.
As to whether the empty tree should be accepted by an automaton, just like with word automata it's a question of if the start state (or #) is an accept state or not.
Huh, so are regular expressions on trees basically linear lambda terms?
I'm not really familiar with lambda calculus, but if I understand your question correctly: A tree with one "variable" (one occurrence of the temporary variable for concatenating into) is called a "context" and is really only relevant for the pumping lemma (and the Myhill-Nerode theorem, as we'll see). Note that the temporary variable occurs multiple times in some of the regular expression examples at the end.