-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Add support for inductively defined functions #8878
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Conversation
|
Given the constraints on the definition, I'm wondering if this should be its own syntax. E.g. Main goal is to avoid confusion around the lack of generality in the definition. If it is envisioned that this will become more general, the current design might be the right way to go. (And by confusion, I mean that this makes it look like normal programming language recursion expectations are supported.) |
|
The goal is definitely to become more general over time. The thinking was that if we fail to solve for a base case, we could tell the user to write things in a particular form that is known to work, but first we'd try to handle any recursive RHS. |
|
We are likely to merge #8877 before this, so consider using the new APIs to simplify visitors/mutators here. I see two here: |
Following substantial discussion with Andrew Adams and Alex Reinking, I have implemented a first draft of their idea of inductively defined functions. A full description is in src/Inductive.h. This pull includes correctness and error tests. Please suggest any additional changes I need to make. The basic idea is to have pure functions that are defined with self-references, e.g. f(x) = select(x <= 0, input(0), input(x) + f(x - 1)), which allows for optimizations that are currently impossible to do with reduction domains.