Improve Symex's computation model and implement "leap branch" much more efficiently by using these traversal computations. We also implement some basic utilities (e.g. symex-index and symex-height) using traversal computations instead of in an ad hoc way.
Symex's computation model is fold-like in the sense that the results (e.g. moves made) are accumulated in sequence, tree-structured in the sense that failed explorations as part of traversal execution are not included in the final result, and monadic in the sense that the basic "move" object can be lifted into any kind of composable computation (e.g. list concatenation to produce the sequence of moves in the traversal, or vector addition to get the total height traversed, or counting the number of occurrences of a certain term, or constructing a string describing the traversal, etc. -- basically any composable thing that we are interested in deriving from the underlying sequence of moves). While formerly this was present in spirit, it wasn't actually used very much and consequently also wasn't very robust. This PR adds many fixes to make it usable and reliable.
Other changes:
add a new loop form for conditional recursion (potentially could be unified with circuit down the line)
make traversal execution tail-recursive as that is easier to reason about and possibly more memory-efficient
[x] In contributing, I relinquish any copyright claims on my contribution and freely release it into the public domain in the simple hope that it will provide value.
(Why: The freely released, copyright-free work in this repository represents an investment in a better way of doing things called attribution-based economics. Attribution-based economics is based on the simple idea that we gain more by giving more, not by holding on to things that, truly, we could only create because we, in our turn, received from others. As it turns out, an economic system based on attribution -- where those who give more are more empowered -- is significantly more efficient than capitalism while also being stable and fair (unlike capitalism, on both counts), giving it transformative power to elevate the human condition and address the problems that face us today along with a host of others that have been intractable since the beginning. You can help make this a reality by releasing your work in the same way -- freely into the public domain in the simple hope of providing value. Learn more about attribution-based economics at drym.org, tell your friends, do your part.)
Summary of Changes
Improve Symex's computation model and implement "leap branch" much more efficiently by using these traversal computations. We also implement some basic utilities (e.g.
symex-indexandsymex-height) using traversal computations instead of in an ad hoc way.Symex's computation model is fold-like in the sense that the results (e.g. moves made) are accumulated in sequence, tree-structured in the sense that failed explorations as part of traversal execution are not included in the final result, and monadic in the sense that the basic "move" object can be lifted into any kind of composable computation (e.g. list concatenation to produce the sequence of moves in the traversal, or vector addition to get the total height traversed, or counting the number of occurrences of a certain term, or constructing a string describing the traversal, etc. -- basically any composable thing that we are interested in deriving from the underlying sequence of moves). While formerly this was present in spirit, it wasn't actually used very much and consequently also wasn't very robust. This PR adds many fixes to make it usable and reliable.
Other changes:
loopform for conditional recursion (potentially could be unified withcircuitdown the line)Public Domain Dedication
(Why: The freely released, copyright-free work in this repository represents an investment in a better way of doing things called attribution-based economics. Attribution-based economics is based on the simple idea that we gain more by giving more, not by holding on to things that, truly, we could only create because we, in our turn, received from others. As it turns out, an economic system based on attribution -- where those who give more are more empowered -- is significantly more efficient than capitalism while also being stable and fair (unlike capitalism, on both counts), giving it transformative power to elevate the human condition and address the problems that face us today along with a host of others that have been intractable since the beginning. You can help make this a reality by releasing your work in the same way -- freely into the public domain in the simple hope of providing value. Learn more about attribution-based economics at drym.org, tell your friends, do your part.)