Recursion with choice rules #12
Comments
stephanzwicknagl
added a commit
that referenced
this issue
Apr 25, 2024
This commit improves the recursion justifier program for showing
correct recursive subgraphs for recursion with choice.
For example, the rule for a loop recursion with choice is as follows:
```
% input rule:
{b(X)} :- b(X-1), a(X).
% justifier rule:
h(n,b(X),(b((X-1)),a(X))) :-
model(a(X));
model(b((X-1)));
@Derivable(b(X)) = 1,
not model(b(X)).
```
The addition is the @Derivable(b(X)) = 1 condition, which is used to
check if the super-node contains the b(X) symbol. If it is in the super-
node, it can be derived. If it is not in the super-node, it cannot be
derived.
Resolves: #12
stephanzwicknagl
added a commit
that referenced
this issue
Apr 30, 2024
Modifying the way in which the node expansion state is stored. This should improve performance. The recrusive subnodes are not stored as a graph, as they are always just a list of nodes chained in one path (order determined by the recursion index). (See #12) The button in the bottom of the row is now fully functional.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The recursion feature doesn't support choice rules. Currently, only a simple path graph is supported as a subgraph.
Idea: Improve the analysis of recursive programs to support a full subgraph, including branching.
The text was updated successfully, but these errors were encountered: