Lambda MicroEgg
4 days ago
- Lambda MicroEgg is an egraph supporting well-scoped, alpha-aware binders, built on Max's microegg with added features like higher-order Miller patterns and capture-avoiding substitution.
- It uses lifting techniques to represent contexts, allowing alpha-equivalent terms to hash-cons to the same memory and enabling efficient handling of binders.
- The tool supports both first-order and higher-order applications, with a curried 'app' notation for the latter, showing a performance trade-off.
- Miller patterns are used for higher-order matching, allowing variables to be applied to bound variables, and the implementation restricts them to ordered patterns for simplicity.
- The system demonstrates practical applications like AC saturation, beta reduction, and rewrite rules for summation and map/comp fusion.
- Current limitations include support for only up to 7 variables due to a byte-stolen Id encoding, and the tool is about 3x slower than egg in microbenchmarks.
- The author used AI assistance in development and highlights both excitement and concerns about its impact.