선언적 최적화를 통한 최적화의 최적화: egglog를 이용한 수학적 최적화 내 고차 함수 (Higher-Order Functions) 최적화

우리는 단순 타입 $\lambda$-calculus (simply typed $\lambda$-calculus)에 기반한 내부 표현을 가진 수학적 모델러인 JijModeling 2에서 수학적 최적화에 대한 egglog의 두 가지 적용 사례를 제시합니다. 첫째, 우리는 고차 함수 (higher-order functions)로 표현된 수학적 모델의 $\LaTeX$ 출력을 개선하기 위해 egglog를 사용합니다. Python의 컴프리헨션 (comprehensions)은 $\textsf{map}$, $\textsf{flat_map}$, $\textsf{filter}$와 같은 스트림 연산 (stream operations)으로 디슈가링 (desugared)되는데, 이러한 항 (terms)들을 직접 출력하면 부자연스러운 수학적 표기법이 생성됩니다. 우리는 고차 항 (higher-order terms)을 extit{엔슈가링 (ensugaring)}함으로써 컴프리헨션 구문을 재구성하며, 임시 변수 재바인딩 (temporary variable rebindings)을 최소화하기 위해 사용자 정의 비용 모델 (custom cost model)과 함께 등식 포화 (equality saturation)를 사용합니다. 둘째, 우리는 EGRAPHS '25에서 발표된 이전의 egg 기반 접근 방식을 확장하여, extit{제약 조건 탐지 (constraint detection)}를 위한 선언적 엔진으로서 egglog를 사용합니다. egglog의 Datalog 스타일 규칙을 사용하면 외부 Rust 오케스트레이션 (orchestration) 코드 없이도 다단계 탐지 로직을 직접 표현할 수 있습니다. 우리는 extit{Henkin-like constants}를 사용하여 매개변수화된 제약 조건을 인코딩하고, egglog 팩트 (facts)를 통해 서브텀 (subterms) 및 인덱스 (indices)에 대한 부수 조건 (side conditions)을 전파합니다. 마지막으로, 동일한 엔슈가링 절차가 포화 (saturation) 전의 대규모 도메인 집합 조건 (large domain-set conditions)을 줄여준다는 것을 보여주며, 수 분이 걸리거나 종료되지 않던 문제적인 탐지 사례를 단 몇 초로 단축시킵니다. 이러한 주제들을 통해, 우리는 egglog의 산업적 적용 사례를 제공하고, 수리 논리학 (mathematical logic)의 아이디어를 사용하여 제약 조건을 전파하는 기법을 입증하며, egglog 프로그램에서 실질적인 성능을 얻기 위해 egglog 규칙의 extit{전제 조건 (premises)}을 최적화하는 것의 중요성을 보여주고자 합니다.