Fast Unital Ring Accumulation

Stream: Is there code for X?

[Schrodinger ZHU Yifan]

I wonder if we can find a proper place to do such optimizations (The idea may be stupid :D).

1) Detect if a function f is an operation on some unital semiring structure $(R, +, \times, 0, 1)$. Say f : Nat -> Nat.
2) f is proven to be total.
3) The base cases of f is known. e.g. f(0) = 1, f(1) = 1.
4) The only non-basic case is in the form $f(n) = \sum_{i = 1}^k a_if(n - k)$ (we can set a limit of such dependence window)

Then we can transform such recursion into a loop and thus solve it in $O(n)$ or even a transition matrix such that solvable in $O(\log n)$.

[Trebor Huang]

Note that Nat is not a ring. If you meant unital semiring, then I can prove that f is the identity, thus it would be trivial.

[Eric Wieser]

I don't understand step 1; how do you tell if $f : \N \to \N$ is a ring morphism without evaluating it on infinitely many Nats?

[Schrodinger ZHU Yifan]

Trebor Huang said:

Note that Nat is not a ring. If you meant unital semiring, then I can prove that f is the identity, thus it would be trivial.

sorry updated.

[Schrodinger ZHU Yifan]

I am not sure why f is id. fibonacci function should be one of such f. Perhaps I missed something in the above description.

[Eric Rodriguez]

Schrodinger ZHU Yifan said:

I am not sure why f is id. fibonacci function should be one of such f. Perhaps I missed something in the above description.

1 = fib(0+0) ≠ fib 0 + fib 0 = 2

[Schrodinger ZHU Yifan]

Eric Wieser said:

I don't understand step 1; how do you tell if $f : \N \to \N$ is a ring morphism without evaluating it on infinitely many Nats?

no, the compiler never proves it but knows in advance.

[Schrodinger ZHU Yifan]

Eric Rodriguez said:

Schrodinger ZHU Yifan said:

I am not sure why f is id. fibonacci function should be one of such f. Perhaps I missed something in the above description.

1 = fib(0+0) ≠ fib 0 + fib 0 = 2

Ah, I see. Should I just drop endomorphism? f is just a self loop.

[Schrodinger ZHU Yifan]

Actually, I tried to generalize it but may have stated it wrongly. There must be some other restrictions like R should be discrete. For now, maybe one should just think about (Nat, +, *, 0, 1).

[Schrodinger ZHU Yifan]

Or other integral types.

[Eric Rodriguez]

Can you write the explicit conditions you want your functions to obey?

[Schrodinger ZHU Yifan]

Sure. I will come up with more details when I am available.

[Siddharth Bhat]

There is a general theory of such optimizations, going by the name of “scalar evolution” or “chains of recurrences” in the compilers literature. Here is a repo with some formalization and links to the literature: https://github.com/bollu/scev-coq