At the moment, Rule enforces a depth-first search (left-most outermost) strategy for selecting the next applicable redex. However, it might be useful to allow this to be customised.
From Paul Klint's tutorial:
Various methods are possible for selecting the redex:
- From the top (root) of the term to the bottom or from the leaves to the root.
- From left to right or from right to left.
We will mostly be using a leaves-to-root and left-to right order. This is called the left-most innermost reduction strategy.
Perhaps it would be sensible to also to switch to left-most innermost reduction by default.
At the moment, Rule enforces a depth-first search (left-most outermost) strategy for selecting the next applicable redex. However, it might be useful to allow this to be customised.
From Paul Klint's tutorial:
Perhaps it would be sensible to also to switch to left-most innermost reduction by default.