Optimizing Optimizations, Declaratively: Optimizing the Higher-Order Functions in Mathematical Optimization with egglog
For practitioners using mathematical modeling tools, this work demonstrates industrial applications of egglog, showing how to propagate constraints using ideas from mathematical logic and optimize rule premises for practical performance.
The authors applied egglog to mathematical optimization in JijModeling 2, improving LaTeX output by reconstructing comprehension syntax from higher-order terms via equality saturation, and enabling declarative constraint detection with datalog-style rules. The ensugaring procedure reduced problematic detection cases from minutes or nontermination to a few seconds.
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 $\textsf{map}$, $\textsf{flat_map}$, and $\textsf{filter}$; emitting these terms directly produces unnatural mathematical notation. We reconstruct comprehension syntax by \emph{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 \emph{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 \emph{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 \emph{premises} of egglog rules to get practical performance in egglog programs.