Remy Goldschmidt
Remy Goldschmidt
Ideally, we could warn the user if the rewriting system they give is known not to be terminating and confluent. There is a sizable amount of research in this direction:...
- [ ] `TermIndex` - [ ] `Perfect` - [ ] `Mergeable` - [ ] `Removeable`
- [ ] `TermIndex` - [ ] `Perfect` - [ ] `Mergeable` - [ ] `Removeable`
In many parts of this library, we take callbacks as input, mainly as a way of avoiding intermediate allocations and to allow equality saturation to be an "anytime" algorithm. We...
Using the techniques described in [_From Conditional to Unconditional Rewriting_ by Grigore Roşu](http://fsl.cs.illinois.edu/pubs/rosu-2004-wadt.pdf), we should be able to convert a conditional TRS (term-rewriting system) into an unconditional TRS, allowing us...
Our term indexing data structures could be useful for other Haskell projects, such as Hoogle or Idris or Agda. We should put them in a separate package, ideally with not...
It seems like it would be quite useful (e.g.: for implementing perfect sharing) to maintain the graph of strongly-connected components of a PEG/EPEG while we build up the graph. The...