We present two applications of egglog to mathematical optimization in JijModeling 2, a mathematical modeller whose internal representation is based on simply typed λ-calculus.

First, we use egglog to improve LaTeX output for mathematical models expressed with higher-order functions. Python comprehensions are desugared into stream operations such as map, flat_map, and filter; emitting these terms directly produces unnatural mathematical notation. We reconstruct comprehension syntax by ensugaring higher-order terms and use equality saturation with a custom cost model to minimize temporary variable rebindings.

Second, we use egglog as a declarative engine for constraint detection, extending the previous egg-based approach presented at EGRAPHS ’25. Egglog’s datalog-style rules let us express multi-step detection logic directly, without external Rust orchestration code. We encode parametrized constraints using Henkin-like constants and propagate side conditions on subterms and indices through egglog facts. Finally, we show that the same ensugaring procedure also reduces large domain-set conditions before saturation, turning a problematic detection case from minutes or nontermination into a few seconds.

Through these topics, we want to provide an example of an industrial application of egglog, demonstrate the trick to propagate the constraints using the ideas from mathematical logic, and show the importance of optimizing premises of egglog rules to get practical performance in egglog programs.

Currently working at Software Development Team at JIJ Inc.