Thank you! It looks very impressive.
Has anyone tried to get it to talk itself out of the box yet?
I see. In that case does the procedure for defining points stay the same, or do you need to use recursively enumerable sets of opens, giving you only countably many reals?
Wait, but rational-delimited open intervals don't form a locale, because they aren't closed under infinite union. (For example, the union of all rational-delimited open intervals contained in (0,√2) is (0,√2) itself, which is not rational-delimited.) Of course you could talk about the locale generated by such intervals, but then it contains all open intervals and is uncountable, defeating your main point about going from countable to uncountable. Or am I missing something?
I'm actually not sure it's a regular grammar. Consider this program:
f(n) := n+f(n-1)
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.
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?
Then isn't it possible to also have infinite expansions "in the middle", not only "inside" and "outside"? Something like this:
f(n) := f(g(n))
g(n) := g(n+1)
Maybe there's even some way to have infinite towers of infinite expansions. I'm having trouble wrapping my head around this.
I don't understand why the second looks like that, can you explain?
Not sure I understand the question. Consider these two programs:
f(n) := f(n)
f(n) := f(n+1)
Which expression trees do they correspond to? Are these trees equivalent?
I just thought of a simple way to explain tensors. Imagine a linear function that accepts two numbers and returns a number, let's call it f(x,y). Except there are two ways to imagine it:
Linear in both arguments combined: f(1,2)+f(1,3)=f(2,5). Every such function has the form f(x,y)=ax+by for some a and b, so the space of such functions is 2-dimensional. We say that the Cartesian product of R^1 and R^1 is R^2, because 1+1=2.
Linear in each argument when the other is fixed: f(1,2)+f(1,3)=f(1,5). Every such function has the form f(x,y)=axy for some a, so the space of such functions is 1-dimensional. We say that the tensor product of R^1 and R^1 is R^1, because 1*1=1.
In this case the tensor product is lower dimensional than the Cartesian product. But if we take say R^3 and R^3, then the Cartesian product will be R^6 and the tensor product will be R^9, because it will have separate coefficients a_(ij)*x_i*y_j.