数理最適化向け埋め込み型領域特化言語 JijModeling 2 におけるプログラミング言語理論の応用について
2K Views
March 05, 26
スライド概要
PPL 2026 で石井が登壇した際のスライドです。JijModeling 2 におけるプログラミング言語理論の応用について述べています。
株式会社Jijは、数理最適化・量子技術の専門家が集い、開発プラットフォームJijZeptをグローバルに提供するスタートアップです。
関連スライド
各ページのテキスト
数理最適化向けEDSL JijModeling 2 における プログラミング言語理論の応用について Mar. 9. 2026 石井大海、清水太朗、寺村俊紀 Slides Available
JijModeling の概要 4
JijModeling = 数理最適 モデラー Python EDSL 化 5
数理最適 とは？ 数理最適化問題：不等式で表された複数の制約条件の下で、与えられた目的 関数（実数値）を最大化または最小化する決定変数の割り当てを求める問題 例（ナップザック問題）：N 個の物品について、各物品の価値 vi と重さ wi が与え られる。ナップザックの耐荷重 W を越えない範囲で、価値の総和を最大化せよ。 化 6
数理最適 とは？ 数理最適化問題：不等式で表された複数の制約条件の下で、与えられた目的 関数（実数値）を最大化または最小化する決定変数の割り当てを求める問題 例（ナップザック問題）：N 個の物品について、各物品の価値 vi と重さ wi が与え られる。ナップザックの耐荷重 W を越えない範囲で、価値の総和を最大化せよ。 制約条件 化 6
数理最適 とは？ 数理最適化問題：不等式で表された複数の制約条件の下で、与えられた目的 関数（実数値）を最大化または最小化する決定変数の割り当てを求める問題 例（ナップザック問題）：N 個の物品について、各物品の価値 vi と重さ wi が与え られる。ナップザックの耐荷重 W を越えない範囲で、価値の総和を最大化せよ。 目的関数 制約条件 化 6
数理最適 とは？ 数理最適化問題：不等式で表された複数の制約条件の下で、与えられた目的 関数（実数値）を最大化または最小化する決定変数の割り当てを求める問題 例（ナップザック問題）：N 個の物品について、各物品の価値 vi と重さ wi が与え られる。ナップザックの耐荷重 W を越えない範囲で、価値の総和を最大化せよ。 • 入力データ：W, N, vi, wi 目的関数 • 現実の制約に即して決まるパラメータ 制約条件 化 6
数理最適 とは？ 数理最適化問題：不等式で表された複数の制約条件の下で、与えられた目的 関数（実数値）を最大化または最小化する決定変数の割り当てを求める問題 例（ナップザック問題）：N 個の物品について、各物品の価値 vi と重さ wi が与え られる。ナップザックの耐荷重 W を越えない範囲で、価値の総和を最大化せよ。 • 入力データ：W, N, vi, wi 目的関数 制約条件 • 現実の制約に即して決まるパラメータ • 決定変数：xi ∈ {0,1} • 変数毎にバイナリ・離散・連続変数など 定義域・上下界を設定（ソルバの要請） • 個数は入力から確定する必要がある 化 6
JijModeling の概要 • JijModeling: 汎用数理最適化モデラー Python EDSL (Rust 製) • モデラー：最適化問題を定式化するツール • JijModeling 1 は社内外で数年に渡り実社会の大規模問題（数 万〜数十万パラメータ）に日々実務適用 • PyPI から無償で利用可能 • 最適化問題の抽象構文木表現の情報を活用 • 総和記号なども形式的に表現し、モデル定義と入力データ （プレースホルダ）を分離（特許第 7034528 号） • 再利用のためにモデルと入力を分離するモデラーは幾つかある が、より踏み込んだAST情報の活用はJijModeling の特徴 • JM1既存機能[4, 24]：LaTeX数式出力、制約検出、問題変換 • JM2の新機能：型検査、高階関数による添字表現 7
JijModeling の概要 • JijModeling: 汎用数理最適化モデラー Python EDSL (Rust 製) • モデラー：最適化問題を定式化するツール • JijModeling 1 は社内外で数年に渡り実社会の大規模問題（数 万〜数十万パラメータ）に日々実務適用 • PyPI から無償で利用可能 • 最適化問題の抽象構文木表現の情報を活用 • 総和記号なども形式的に表現し、モデル定義と入力データ （プレースホルダ）を分離（特許第 7034528 号） • 再利用のためにモデルと入力を分離するモデラーは幾つかある が、より踏み込んだAST情報の活用はJijModeling の特徴 • JM1既存機能[4, 24]：LaTeX数式出力、制約検出、問題変換 • JM2の新機能：型検査、高階関数による添字表現 N−1 ∑ i=0 wi ⋅ xi の抽象構文木 7
ナップザック問題の定式化例と数式出力 • JijModeling 2 でナップザック問題を定式化した例 • 右側は Jupyter Notebook などで problem を表示させると自動で出力される数式出力の結果 @jm.Problem.define("Knapsack",sense=MAXIMIZE) def problem(prb: jm.DecoratedProblem): v = prb.Float(ndim=1) N = prb.DependentVar(v.len_at(0)) w = prb.Float(shape=(N,)) W = prb.Float() x = prob.BinaryVar(shape=(N,)) problem += problem.Constraint( "weight", jm.sum(w[i] * x[i] for i in N) W) problem += jm.sum(v[i] * x[i] for i in N) = < 8
JijModeling の特徴：OMMX 形式へのコンパイラ • データを入力し、具体的なインスタンスへとコンパ イルされてはじめてソルバで解けるように JijModeling Compile • OMMX: JIJ が開発しているオープンソースの数 理最適化向けデータ交換形式 OMMX • Adapter を介しソルバを切り替え可能 • JijModeling ＝ 高レベルな数理最適化問題の表現か らOMMXメッセージへのコンパイラ OMMX instance の表現（Protobuf） Input • インスタンスは数理最適化向けデータ交換形式 OMMXメッセージ[8, 23] として表現 JijZept Solver OpenJij SCIP Solvers Qamomile Gurobi 9
➡︎ プログラミング言語としての JijModeling 2 • JijModeling 2 = 型付λ-計算ベースの全域言語 • Python を表層言語として使えるが、処理系自体は独立 • 決定変数やプレースホルダは自由変数として表現 • 構文木の定式化：Locally Nameless[2] +Trees that Grow[13] による構文木の共通化とメタデータの両立 • 評価器： Call-by-Value でHOAS ベースの中間表現 定義 へ評価、 OMMX Message へ抽出 10
本講演の内容 • 本講演は1月に公開した次世代版 JijModeling 2 のPL理論的な背景について 1. 数式出力とPython 内包表記との脱糖・加糖 2. egglog による制約検出の定式化 3. 数理最適化向け型システムの設計 ★ いずれもJijModeling 1の「構文木の情報を活用する」設計思想を推し進め、 プログラミング言語の段階まで昇華して可能に 11
話題1：数式出力と内包表記への「加糖」 14
JijModeling 2 以前・以後の総和記号 15
JijModeling 2 以前・以後の総和記号 • JijModeling 1 では、添え字に当る不自然な Element オブジェクトが必要（不評） JijModeling 1 N = jm.Placeholder("N") i = jm.Element("i", belong_to=N) x = jm.BinaryVar("x", shape=(N,)) jm.sum([(i, i % 2 0)], x[i]) = = 15
JijModeling 2 以前・以後の総和記号 • JijModeling 1 では、添え字に当る不自然な Element オブジェクトが必要（不評） • JijModeling 2 では、map/filter などの高階関数を導入し、添え字は束縛変数として定式化 JijModeling 1 JijModeling 2 N = jm.Placeholder("N") i = jm.Element("i", belong_to=N) x = jm.BinaryVar("x", shape=(N,)) prb = jm.Problem("Test") N = prb.Length("N") x = prb.BinaryVar("x", shape=(N,)) jm.sum(N.filter(lambda i: i % 2 0) .map(lambda i: x[i]) ) jm.sum([(i, i % 2 0)], x[i]) = = = = 15
JijModeling 2 以前・以後の総和記号 • JijModeling 1 では、添え字に当る不自然な Element オブジェクトが必要（不評） • JijModeling 2 では、map/filter などの高階関数を導入し、添え字は束縛変数として定式化 • Python デコレータを使って構文解析し、Python の内包表記を使った直感的な記述が可能に • デコレータ＝Python関数・クラス定義を引数に取る高階関数により、関数の返値でオ リジナルの定義を置き換える Python の言語機能 • Python の関数objの持っている生ソースコード情報をパーズし、構文木を書き換え JijModeling 1 N = jm.Placeholder("N") i = jm.Element("i", belong_to=N) x = jm.BinaryVar("x", shape=(N,)) jm.sum([(i, i % 2 0)], x[i]) JijModeling 2 @jm.Problem.define("Test") def prb(prb jm.DecoratedProblem): N = prb.Length() x = prb.BinaryVar(shape=(N,)) jm.sum( x[i] for i in N if N % 2 0 ) = = = = 15
• 脱糖：一部の関数呼び出しに現れる内 包表記を flat_map / map / filter を使 いPython 構文木レベルで脱糖 • 脱糖規則は標準的なもの jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 規則 = 16 = ➡︎ 内包表記の脱糖と数式出力
• 脱糖：一部の関数呼び出しに現れる内 包表記を flat_map / map / filter を使 いPython 構文木レベルで脱糖 • 脱糖規則は標準的なもの jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 規則 jm.sum( N.filter(lambda i: i % 2 0) .flat_map(lambda i: M.map(lambda j: (i, j))) .map(lambda i, j: x[i] * t[i, j])) = = = 16 = ➡︎ 内包表記の脱糖と数式出力
• 脱糖：一部の関数呼び出しに現れる内 包表記を flat_map / map / filter を使 いPython 構文木レベルで脱糖 • 脱糖規則は標準的なもの jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 規則 😰 脱糖後をそのまま数式出力するとユー ザにとっては意味がわからない jm.sum( N.filter(lambda i: i % 2 0) .flat_map(lambda i: M.map(lambda j: (i, j))) .map(lambda i, j: x[i] * t[i, j])) = = = 16 = ➡︎ 内包表記の脱糖と数式出力
• 脱糖：一部の関数呼び出しに現れる内 包表記を flat_map / map / filter を使 いPython 構文木レベルで脱糖 • 脱糖規則は標準的なもの jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 規則 😰 脱糖後をそのまま数式出力するとユー ザにとっては意味がわからない 🤔 問題：高階関数を含む数式をどうユー ザに読みやすく数式に変換する？ jm.sum( N.filter(lambda i: i % 2 0) .flat_map(lambda i: M.map(lambda j: (i, j))) .map(lambda i, j: x[i] * t[i, j])) = = = 16 = ➡︎ 内包表記の脱糖と数式出力
• 脱糖：一部の関数呼び出しに現れる内 包表記を flat_map / map / filter を使 いPython 構文木レベルで脱糖 • 脱糖規則は標準的なもの jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 規則 😰 脱糖後をそのまま数式出力するとユー ザにとっては意味がわからない 🤔 問題：高階関数を含む数式をどうユー ザに読みやすく数式に変換する？ 💡 内包表記への加糖を考えたらどうか？ jm.sum( N.filter(lambda i: i % 2 0) .flat_map(lambda i: M.map(lambda j: (i, j))) .map(lambda i, j: x[i] * t[i, j])) = = = 16 = ➡︎ 内包表記の脱糖と数式出力
内包表記への「加糖」：構文論的な変換 ~ ]：式から内包表記への加糖 JeK = [e | ES-Comp-Map ~a fresh {| \~ a ~ p 2 e |} = 0 Jmap( p. e, e )K = [ 0 \~ a (Compr) ES-Comp-FlatMap ~a fresh ~ ] e| b fresh ~ {| \~a p 2 e0 |} = ~; ~ ] Jflat_map( p. e, e )K = [ b | 0 ES-Comp-Filter ~a fresh ~0 {| b 2 \~a p |} = 0 • プログラム変換と捉え、内包表記 への加糖を考える 1. 所属関係から内包表記右辺の 文の列への変換 2. 式から内包表記への変換 ~ ] Je0 K = [ e0 | ~ ; let \~a p = e0 ; if \~a e ] Jfilter( p. e, e0 )K = [ e0 | • for 文のたびに新鮮な変数を束縛 ~ ：所属関係から内包表記右辺の文列への加糖 {| p 2 e |} = (Stmt) ES-Stmts-FlatMap ~a fresh ES-Stmts-Map ~a fresh {| ~ p 2 e |} = \~ a 0 0 ~ ; let p = \~a e {| p 2 map( p0 . e, e0 ) |} = ES-Stmts-Filter ~a fresh ~ {| \~a p0 2 e0 |} = {| ~ p 2 e |} = \~ a 0 0 ~0 {| p 2 \~a e |} = ~; ~0 {| p 2 flat_map( p0 . e, e0 ) |} = ~ ; if \~a e; let p = \~a p0 {| p 2 filter( p0 . e, e0 ) |} = ES-Stmts-Fallback {| p 2 e |} = for p in e 🥲 だいぶマシだが、再束縛が多すぎ てまだ読み辛い…… 💡 再束縛を減らすプログラム最適化 だと捉えたらどうか？ 17
内包表記への「加糖」：再束縛の「最適化」 • egglog[22] による等式飽和で実装 • egglog: datalog + e-graph • 論理型のパラダイムで同値性を考慮 しつつコスト最良項を抽出したり factをqueryできる • 規則をグループ分けし、柔軟な実行 制御が可能 (with-dynamic-cost (datatype Stmt (ExprStmt Expr :cost 0) (BelongsTo Expr Expr) (Let Expr Expr :cost 100) (Then Stmt Stmt :cost 1))) (datatype Comprehension (Compr Expr Stmt)) (relation assert (Stmt)) (relation focus (Comprehension)) (relation concludes (Expr)) (rewrite (Then a b) b :when ((= a (Let l l)))) (rewrite (Then b a) b :when ((= a (Let l l)))) (rule ((assert (Let (Var p) (Var e)))) ((union (Var p) (Var e)))) 18
➡︎ 内包表記への「加糖」：再束縛の「最適化」 • egglog[22] による等式飽和で実装 • egglog: datalog + e-graph • 論理型のパラダイムで同値性を考慮 しつつコスト最良項を抽出したり factをqueryできる • 規則をグループ分けし、柔軟な実行 制御が可能 • 概略 • Let 式に高いコストを設定 • 変数は添え字が若いほど低コスト • 束縛式の両辺を union する • 内包表記左辺が単独変数の場合、そ の定義を展開させる規則も 規則 (with-dynamic-cost (datatype Stmt (ExprStmt Expr :cost 0) (BelongsTo Expr Expr) (Let Expr Expr :cost 100) (Then Stmt Stmt :cost 1))) (datatype Comprehension (Compr Expr Stmt)) (relation assert (Stmt)) (relation focus (Comprehension)) (relation concludes (Expr)) (rewrite (Then a b) b :when ((= a (Let l l)))) (rewrite (Then b a) b :when ((= a (Let l l)))) (rule ((assert (Let (Var p) (Var e)))) ((union (Var p) (Var e)))) 18
➡︎ 内包表記への「加糖」：再束縛の「最適化」 • egglog[22] による等式飽和で実装 • egglog: datalog + e-graph • 論理型のパラダイムで同値性を考慮 しつつコスト最良項を抽出したり factをqueryできる • 規則をグループ分けし、柔軟な実行 制御が可能 • 概略 • Let 式に高いコストを設定 • 変数は添え字が若いほど低コスト • 束縛式の両辺を union する • 内包表記左辺が単独変数の場合、そ の定義を展開させる規則も 規則 😄 無事簡潔な数式出力が可能に！ (with-dynamic-cost (datatype Stmt (ExprStmt Expr :cost 0) (BelongsTo Expr Expr) (Let Expr Expr :cost 100) (Then Stmt Stmt :cost 1))) (datatype Comprehension (Compr Expr Stmt)) (relation assert (Stmt)) (relation focus (Comprehension)) (relation concludes (Expr)) (rewrite (Then a b) b :when ((= a (Let l l)))) (rewrite (Then b a) b :when ((= a (Let l l)))) (rule ((assert (Let (Var p) (Var e)))) ((union (Var p) (Var e)))) 18
まとめ：数式出力と内包表記の「加糖」 • JijModeling は強力な数式出力機能を搭載 19
まとめ：数式出力と内包表記の「加糖」 • JijModeling は強力な数式出力機能を搭載 🤔 JM2でサポートした内包表記脱糖後の高階関数をどう 読み易い数式に出力するか？ jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 = = 19
まとめ：数式出力と内包表記の「加糖」 • JijModeling は強力な数式出力機能を搭載 🤔 JM2でサポートした内包表記脱糖後の高階関数をどう 読み易い数式に出力するか？ jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 💡 脱糖の逆「加糖」＋再束縛数の最適化！ = = 19
まとめ：数式出力と内包表記の「加糖」 • JijModeling は強力な数式出力機能を搭載 🤔 JM2でサポートした内包表記脱糖後の高階関数をどう 読み易い数式に出力するか？ jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 💡 脱糖の逆「加糖」＋再束縛数の最適化！ • 名前衝突を避けるため全て再束縛して加糖 = = 19
まとめ：数式出力と内包表記の「加糖」 • JijModeling は強力な数式出力機能を搭載 🤔 JM2でサポートした内包表記脱糖後の高階関数をどう 読み易い数式に出力するか？ jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 💡 脱糖の逆「加糖」＋再束縛数の最適化！ • 名前衝突を避けるため全て再束縛して加糖 • 変数の数・添え字・再束縛の数に関するプログラ ム最適化パスを適用（egglog による等式飽和） • 長くとも 100ms 以内に終わる = = 19
まとめ：数式出力と内包表記の「加糖」 • JijModeling は強力な数式出力機能を搭載 🤔 JM2でサポートした内包表記脱糖後の高階関数をどう 読み易い数式に出力するか？ jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 💡 脱糖の逆「加糖」＋再束縛数の最適化！ • 名前衝突を避けるため全て再束縛して加糖 • 変数の数・添え字・再束縛の数に関するプログラ ム最適化パスを適用（egglog による等式飽和） • 長くとも 100ms 以内に終わる 💡 数式出力をプログラム変換＋最適化と捉えた = = 19
まとめ：数式出力と内包表記の「加糖」 • JijModeling は強力な数式出力機能を搭載 🤔 JM2でサポートした内包表記脱糖後の高階関数をどう 読み易い数式に出力するか？ jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 💡 脱糖の逆「加糖」＋再束縛数の最適化！ • 名前衝突を避けるため全て再束縛して加糖 • 変数の数・添え字・再束縛の数に関するプログラ ム最適化パスを適用（egglog による等式飽和） • 長くとも 100ms 以内に終わる 💡 数式出力をプログラム変換＋最適化と捉えた 😄 ボーナス：最初から filter / map などで書かれたプロ グラムも綺麗な数式で表示されるように！ = = 19
まとめ：数式出力と内包表記の「加糖」 • JijModeling は強力な数式出力機能を搭載 🤔 JM2でサポートした内包表記脱糖後の高階関数をどう 読み易い数式に出力するか？ jm.sum( x[i] * t[i,j] for i in N if i % 2 for j in M ) 0 💡 脱糖の逆「加糖」＋再束縛数の最適化！ • 名前衝突を避けるため全て再束縛して加糖 • 変数の数・添え字・再束縛の数に関するプログラ ム最適化パスを適用（egglog による等式飽和） • 長くとも 100ms 以内に終わる 💡 数式出力をプログラム変換＋最適化と捉えた 😄 ボーナス：最初から filter / map などで書かれたプロ グラムも綺麗な数式で表示されるように！ • 発展：DBに項の型の情報を登録し、添え字の範 囲を ∈ で書くのか上下で範囲を示すのか切替 = = 19
話題2：egglog による制約検出 22
背景：制約検出による求解速度の向上（JijModeling 1） • 例：SOS1/2, One-Hot (単体制約), ... • 一部のソルバはの専用のAPIを提供 😢 実務者は数理最適化の専門家とは限らず、「よ い制約」の存在に気付けない！ 🥹 モデラーが自動で検出してほしい！ 60 求解時間 [sec] • 特定の形式の制約の構造を活かし効率的に最適化問 題を解くアルゴリズムがある 二地区工場配置問題の求解時間 （データは [4] より引用） SOS1検出なし 45 SOS1検出あり 30 15 0 6 12 18 24 30 36 42 48 54 60 入力サイズ 🤯 データ一体型モデラーや OMMX Message からの効率的な検出は困難（組合せ爆発） 🤔 一つのパターンに対し、同値な記述方法を可能な限り全て検出したい 💡 JijModeling 1 では egglog の先行版 egg を用いて等式飽和で検出 [4] 💡 JijModeling 2 では egglog でより宣言的に実装。現状の egglog は束縛変数を第一級で扱え ないが、Henkin 定数を使って個別の束縛変数の情報を伝播するトリックを編み出し解決 23
例：SOS1 制約 • SOS1制約：非負変数の族 {xi} に対する SOS1 制約（Special Ordered-Set i of Type 1）とは、高々一つの xi が非零であることを要求する制約 • • xi がいずれもバイナリ変数の場合、 ∑i xi ≤ 1 と表現できる 一般の非負変数の場合は補助的なバイナリ変数族 {δi}i を導入し、 ∑i δi ≤ 1 ∧ ∀i xi ≤ Miδi と表現できる（但し Mi は xi の上界） • JijModeling 1 では egg でバイナリ変数の SOS1 を検出した後、Rust の世界 に引き戻してから再度 egg で xi ≤ Mi を検出させる必要があった 24
SOS1 検出 with egglog in Action • SOS1 の検出規則： (rule (( (sum conds v[i]) 1) (binary_vars v)) ((sos1 conds v[i]))) (rule ((sos1 conds b[i]) (binary_vars b) ( v[i] (* M[i] b[i])) ( 0 v[i]) ( v[i] M[i])) (sos1 conds v[i])) • モデルの制約追加時に、束縛変数に Nonce をつけて付帯条件を登録しHenkin 定数の役割をさせる = < = < = < = < 25
SOS1 検出 with egglog in Action • SOS1 の検出規則： (rule (( (sum conds v[i]) 1) (binary_vars v)) ((sos1 conds v[i]))) (rule ((sos1 conds b[i]) (binary_vars b) ( v[i] (* M[i] b[i])) ( 0 v[i]) ( v[i] M[i])) (sos1 conds v[i])) • モデルの制約追加時に、束縛変数に Nonce をつけて付帯条件を登録しHenkin 定数の役割をさせる (rule ((< i N)) (( (< i_98 N) x[i] (* M[i] δ[i]))) = < = = < < = < = < 25
SOS1 検出 with egglog in Action • SOS1 の検出規則： (rule (( (sum conds v[i]) 1) (binary_vars v)) ((sos1 conds v[i]))) (rule ((sos1 conds b[i]) (binary_vars b) ( v[i] (* M[i] b[i])) ( 0 v[i]) ( v[i] M[i])) (sos1 conds v[i])) • モデルの制約追加時に、束縛変数に Nonce をつけて付帯条件を登録しHenkin 定数の役割をさせる (rule ((< i N)) (( (< i_98 N) x[i] (* M[i] δ[i]))) (< i_42 N) (= (% i_42 2) 0) ( (sum ((< N i_42) (= (% i_42 2) 0)) δ[i_42]) 1) = < = = < < = < = < = < 25
SOS1 検出 with egglog in Action • SOS1 の検出規則： (rule (( (sum conds v[i]) 1) (binary_vars v)) ((sos1 conds v[i]))) (rule ((sos1 conds b[i]) (binary_vars b) ( v[i] (* M[i] b[i])) ( 0 v[i]) ( v[i] M[i])) (sos1 conds v[i])) • モデルの制約追加時に、束縛変数に Nonce をつけて付帯条件を登録しHenkin 定数の役割をさせる (rule ((< i N)) (( (< i_98 N) x[i] (* M[i] δ[i]))) (< i_42 N) (= (% i_42 2) 0) ( (sum ((< N i_42) (= (% i_42 2) 0)) δ[i_42]) 1) (sos1 ((< N i_42) (= (% i_42 2) 0)) δ[i_42]) ( x[i_42] (* M[i_42] δ[i_42])) (sos1 ((< N i_42) (= (% i_42 2) 0)) x[i_42]) = < = = < < = < = < = = < < 25
egglog による制約検出：まとめ • JijModeling 1 の時点では egg でパターンマッチ mod 同値性を達成[4] • SOS1 の検出で大幅な求解速度向上 • 複数条件の組合せで表現される問題は一旦Rustに戻る必要があり面倒 • JijModeling 2：egglog の論理型プログラミングにより宣言的に解決 • egglog は束縛変数の扱いに難があるが、Henkin定数のトリックで束縛変数間の情報を伝播 • 今後の課題 • 検出速度の改善：個別のHenkin定数の掛け算で組合せ爆発が起きうる。専用のスケジュー ラや履歴スタック機能の利用が必要か • 「Henkin 定数」の正当化：通常の Henkin 定数は ∃x [φ(x)] ⟹ φ(cφ) だが今回の手法で は無条件に φ(cφ) を仮定している • cφ たちはコンパイル時に具体的な値に展開されるため、空でないときのみ評価が起き るので健全性は問題ないはず 26
話題3：数理最適化向けの型システム 29
数理最適化向けの型システムの要請 🤔 数理最適化 Python EDSL 向け型システムはどのようなものであるべきか？ ‣ 決定変数の有無の区別 • 決定変数は添え字に現れてはならない ‣ 数値およびコンテナ型の部分型や演算子オーバーロード • 決定変数には種類がある。これらの間の部分型関係が扱えるべき • 動的言語をホスト言語とすることを念頭に、演算子オーバーロードが扱えるべき ‣ 多次元配列の添え字の検査 • 数万要素ある配列の次元を間違えた結果、二時間後エラー……は防ぎたい ‣ 高階関数のサポート • 内包表記の脱糖が自由に行えるよう、第一級の値として関数を扱える必要がある 30
型システムが持つべき機能 • 前項を踏まえると、型システムは以下の機能を持つことが望ましい • 部分型システム／演算子オーバーロード／限定的な依存型／（高階）関数型 • Xie–Oliverira[21] による適用モードつきの双方向型付け (Let Arguments Go First) でこれらを実装 • 二つのモードの相互再帰： p ` e ) T ：適用／推論モード、 ` e ( T ：検査モード • コードの重複を防ぐ観点から、適用モードと推論モードは統合し、必要に応じて適用文脈が空かを検査 • 採用理由 • 局所性：数理最適化においては変数の型が最初から確定している • 決定変数に型を指定する習慣があり、プレースホルダの型指定にも抵抗が少ないと思われる • λ-抽象の有界性：JijModeling のλ-抽象は、内包表記の脱糖、総和の本体や制約条件の本体の定義、上下界の指定などに限 られ、引数の型が確定している • 適用モードは引数の型から本体を推論させるものであり、活躍の余地が大きい • 多相性が不要：上記と関連し、多相関数の需要がほぼないため、単一化を用いる旨味がない • 拡張性：部分型や演算子オーバーロードなどによる拡張が容易。また、局所性から多くの場合適用（推論）モードのロ ジックを拡張するだけでよく、新機能開発の敷居が低い 🤔 双方向型付けでは、型註釈が必要になるのでは？ 😄 決定変数・プレースホルダの宣言以外に型註釈構文を提供していないが、注釈が必要となった例は現時点でなく、実際に 既存の典型問題（約30種）を問題なく定式化できている 31
推論規則の例
` T type
(Type Formation)
F-T-RangeNat
`e (
F-T-CatLab
Scalarstat
N
` label
` N<e type
` ` type
F-T-TDict
` K total key
` TDict [K , T ] type
(Typing Judgements)
`e,T
T-I-App
p ; ` e2 ) T1
p
p
` p ( T1 ) D
D {p : T1 } ,
✴
p
T-C-ChangeDir
, T1 ` e1 ) T2
p ; ` e ) T0
` e1 e2 ) T
T-I-Abs
p
` T type
` e ) T2
, T1 ` p. e ) T1 ! T2
`e ( T
` T0 4 T
T-C-Abs
` p ( T1 ) D
D {p : T1 } ,
` e ( T2
` p. e ( T1 ! T2
T-I-IterCat
` label
p ; ` iter_catl ( ) ) Set` (T- ?)
` e1 , . . . , en ( T1 , . . . , Tn ) T 0 , D は次で説明するパターンマッチの判断
✴ 部分型関係 ≼ の定義も後述
32
演算子オーバーロード（ad-hoc多相）およびパターンマッチの例 • オーバーロードの解決：入力式の型を検査し、(場合に応じて返値型も含む）「辞書」D を推論する判断 ` e1 , . . . , en ( T1 , . . . , Tn ) D を追加 • パターンマッチも値の割り当て方（デストラクタ）の辞書として表現できるため、同様の機構で実現 (Typing Judgements) `e,T T-P-Tuple T-P-Var ` pi ( Ti ) Di ` (p1 , .. , pn ) ( (T1 ⇥ · · · ⇥ Tn ) ) tupleD1 ,...,Dn ` xi ( T ) (xi : T ) T-P-Array ` pi ( T ~ ` (p1 , .. , pn ) ( T N<n , destructor, D ~ ) Di ) ArrayD1 ,...,Dn destructors for pattern matching ::= | (xi : T ) bind a value of type T as i-th variable tupleD1 ,...,Dn splitting as a tuple | ArrayD1 ,...,Dn | splitting as an array along the first axis 33
代数的な部分型システム
で部分型関係 ≼ を定義
• 型上の部分関数
定義（部分擬束）
• リストや集合のブール演算の型を直感的に定式化できる
• 形式的な交叉・和ではなく、部分関数による定式化はあまり見ない気がする
• 型上の同値関係 ∼
は同値な型を同一視：ℕ<2 ∼ Scalar stat
{0,1} 等
•T ^
課題：既存研究との関連、実装が公理を満たすことの保証、他の定式化
T 0, T _ T 0
(Lattice Operations)
以下を満たす⟨L, ∼ , ∨ , ∧ ⟩ を部分擬束と呼ぶ
1. ∼ は通常の = を拡張するL上の同値関係
2. ∨ , ∧ は部分関数で以下を満たす：
Eq-Ty-SupArr
` T1 ^ T2 ⇠ T
` U1 _ U2 ⇠ U
` (T1 ⇥ · · · ⇥ Tn ) _ (T1 ⇥ · · · ⇥ Tn ) ⇠ (T1 ⇥ · · · ⇥ Tn )
Eq-Ty-InfArr
Eq-Ty-SupScl
` T1 _ T2 ⇠ T
` U1 ^ U2 ⇠ U
µ1 _ µ2 ⇠ µ
↵1 _ ↵2 ⇠ ↵
` Scalarµ↵11 _ Scalarµ↵22 ⇠ Scalarµ↵
` (T1 ⇥ · · · ⇥ Tn ) ^ (T1 ⇥ · · · ⇥ Tn ) ⇠ T ! U
Eq-Ty-SupArray
Eq-Ty-SupSclRng
`e (
Scalarstat
N
N _ ↵ ⇠ ↵0
µ
` Scalarµ↵ _ N<e T⇠^Scalar
T 0 , T ↵_0 T 0
Eq-Ty-SupTDict
` K1 ^ K2 ⇠ K
` T1 _ T2 ⇠ T
` TDict [K1 , T1 ] _ TDict [K2 , T2 ] ⇠ TDict [K , T ]
` i0 ⇠ N<ei0
i ⇠ N<ei
` ei ⇠ ei0
` T1 _ T2 ⇠ T
~
~0
~
` T1 _ T2 ⇠ T 1
(Lattice Operations)
`
T 4 T0
Eq-Ty-SupPDict
` K1 ^ K2 ⇠ K
` T1 _ T2 ⇠ T
` PDict [K1 , T1 ] _ PDict [K2 , T2 ] ⇠ PDict [K , T ]
※論文では TDict/PDictのKの変性が間違っていました
3. ∼ は ∨ , ∧ について合同関係である
このとき x ∧ y ∼ x ⟺ x ∨ y ∼ y が成り立つの
で、 L 上の擬順序関係 ≼ を次で定める：
(Lattice Operations)
x ≼ y ⟺ x∨y∼y
Sub-Sup
` T _ T0 ⇠ T
` T 4 T0
stat 4 dyn,
B4N4Z4R
34
JijModeling の型の宇宙
• 決定変数の有無の区別、モデル記述の簡便性を念頭に取捨選択
type, T , U
• プリミティヴ型：
•
•
種類：binary {0,1}、自然数 ℕ、整数 ℤ 、連続 ℝ
ステージ：決定変数を含まない場合 μ = stat 、含み
得る場合 μ = dyn
Scalar stat
ℕ の部分型。「限定的な依存型」の一つ
• カテゴリーラベル：等値性の比較以外の構造も持たない
「ラベル」。辞書と組み合わせて使う想定（後述）
scalar, ↵
• 真偽値、文字列
• 複合型：ステージは dyn Scalar を含むかで再帰的に定義
• 関数型、タプル、配列、辞書、ストリーム（Set）
stage, µ
function type
|
{T1 Q T2 }
comparison type between T1 and T2
(T1 ⇥ · · · ⇥ Tn )
tuple type
Scalarµ↵
scalar type with stage and domain
|
N<e
natural numbers less than e
|
B
boolean
|
String
string
|
T
Array type
|
SetT
set (stream) of T s
|
[e]
element of set-expression e
|
`
opaque category label `
|
TDict [K , T ]
total dictionary from K to T
|
PDict [K , T ]
partial dictionary from K to T
domain of scalar
|
R
real
|
Z
integer
|
N
natural number
|
{ 0, 1 }
binary (i.e. 0 or 1)
stage of scalar
::=
|
dimspec,
~
::=
|
• タプルと配列によりグラフ構造が表せる
• ストリームは畳み込みの対象
T1 ! T2
|
• ℕ<n: static な自然数 n 未満の自然数全体。
•
|
|
• Scalar μα：種類 α、ステージ μ のスカラー型
type
::=
dyn
dynamic (may contain decision variables)
stat
static (doesn’t contain decision variables)
dimension specification
::=
|
|
N<e
fixed size
?
unknown size
35
JijModeling のコンテナ型 • 多次元配列 T δ1×⋯×δn ：シェイプが確定 している要素 T の多重配列。次元は有 限確定値で、具体的な成分数 δ は入力 データによって指定可能。 例：移動制限のあるTSP • 辞書：整数や文字列、カテゴリーラベ ルのタプルをキーとする連想配列。 • 全 域 辞 書 TDict[K, V ] は 全 て の キーに対して値が与えられる必要 • 部分辞書 PDict[K, V ] の定義域は 部分的でよい • 特に部分辞書で部分的に定義された疎 な構造を表現可能 36
JijModeling のコンテナ型 • 多次元配列 T δ1×⋯×δn ：シェイプが確定 している要素 T の多重配列。次元は有 限確定値で、具体的な成分数 δ は入力 データによって指定可能。 例：移動制限のあるTSP • 辞書：整数や文字列、カテゴリーラベ ルのタプルをキーとする連想配列。 • 全 域 辞 書 TDict[K, V ] は 全 て の キーに対して値が与えられる必要 • 部分辞書 PDict[K, V ] の定義域は 部分的でよい • 特に部分辞書で部分的に定義された疎 な構造を表現可能 都市名間の「順序」は本質的でない カテゴリーラベルで表現！ 36
JijModeling のコンテナ型 • 多次元配列 T δ1×⋯×δn ：シェイプが確定 している要素 T の多重配列。次元は有 限確定値で、具体的な成分数 δ は入力 データによって指定可能。 例：移動制限のあるTSP • 辞書：整数や文字列、カテゴリーラベ ルのタプルをキーとする連想配列。 • 全 域 辞 書 TDict[K, V ] は 全 て の キーに対して値が与えられる必要 • 部分辞書 PDict[K, V ] の定義域は 部分的でよい • 特に部分辞書で部分的に定義された疎 な構造を表現可能 都市名間の「順序」は本質的でない カテゴリーラベルで表現！ 時刻数＝都市数 36
JijModeling のコンテナ型 • 多次元配列 T δ1×⋯×δn ：シェイプが確定 している要素 T の多重配列。次元は有 限確定値で、具体的な成分数 δ は入力 データによって指定可能。 例：移動制限のあるTSP • 辞書：整数や文字列、カテゴリーラベ ルのタプルをキーとする連想配列。 • 全 域 辞 書 TDict[K, V ] は 全 て の キーに対して値が与えられる必要 • 部分辞書 PDict[K, V ] の定義域は 部分的でよい • 特に部分辞書で部分的に定義された疎 な構造を表現可能 都市名間の「順序」は本質的でない カテゴリーラベルで表現！ 時刻数＝都市数 添え字の 混同防止！ 36
JijModeling のコンテナ型 • 多次元配列 T δ1×⋯×δn ：シェイプが確定 している要素 T の多重配列。次元は有 限確定値で、具体的な成分数 δ は入力 データによって指定可能。 例：移動制限のあるTSP • 辞書：整数や文字列、カテゴリーラベ ルのタプルをキーとする連想配列。 • 全 域 辞 書 TDict[K, V ] は 全 て の キーに対して値が与えられる必要 • 部分辞書 PDict[K, V ] の定義域は 部分的でよい • 特に部分辞書で部分的に定義された疎 な構造を表現可能 「部分的にしか繋ってない」 都市を部分辞書で表現！ 都市名間の「順序」は本質的でない カテゴリーラベルで表現！ 時刻数＝都市数 添え字の 混同防止！ 36
Set (ストリーム) 型と Element 型 [e] • 総和総積・最大最小などの畳み込みを行える型として Set 型がある • Set といっているが、順序と重複を許容するストリーム型である • 多次元配列は成分、辞書は値のストリームに相当する Set に自動変換 • 配列は内側の行についてイテレートしたい場合もあるので、rows() により 内側のスライスからなる Set に変換できる • static な自然数 n は「n 未満の static な自然数全体」と同一視 • [e] ≼ T ：Set[T] 型の式 e について、「e の要素」を表す T の部分型 • もう一つの限定的な依存型。辞書の添え字の検査時に主要な役割（後述） • 決定変数の個数は確定する必要があるので TDict で指定する必要がある が、他の PDict の定義域を指定することができる 37
添え字の検査 • 現状：型検査時と評価器は分離されているた め、評価を必要としない範囲のみ検査 ` T type, . . . (Formation Rules) F-TK-RngNat F-TK-CatLab ` N<e type ` N<e total key F-T-CatLab ` ` total key ` [keys(e)] total key ` K total key ` ` type ` e ( Scalarstat N p ; ` e ) TDict [K , T ] F-T-TDict ` label F-T-RangeNat F-TK-TKeys ` label ` N<e type F-T-PDict ` T type ` K partial key ` TDict [K , T ] type ` T type ` PDict [K , T ] type (Typing Rules) `e,T T-I-SubsFull T-I-SubsSub p ; ` e ) T 1 ,..., n ` ei ( `e,T p ; ` e ) T 1 ,..., n Scalarstat N ` ei ( p ; ` e [e1 , .. , en ] ) T T-I-LookupTotal p ; ` e ) TDict [K , T ] p ; ` e [e0 ] ) T k<n Scalarstat N p ; ` e [e1 , .. , ek ] ) T k+1 ,..., n (Typing Rules) ` e0 ( K T-I-LookupPartial T-C-KeysApprox p;`e ) T p ; ` e ) PDict [K , T ] ` e0 ( [keys(e)] p ; ` e [e0 ] ) T ` e ( SetT ` e ( [keys(e0 )] ※更に、像を取るスライスによる添え字の規則もあり（判断図の形で書くにはやや複雑） 38
添え字の検査 • 現状：型検査時と評価器は分離されているた め、評価を必要としない範囲のみ検査 • 次元は確定自然数値であるため、添え字 の成分数は厳密に検査（T-I-Subs* / T-ILookup*） ` T type, . . . (Formation Rules) F-TK-RngNat F-TK-CatLab ` N<e type ` N<e total key F-T-CatLab ` ` total key ` [keys(e)] total key ` K total key ` ` type ` e ( Scalarstat N p ; ` e ) TDict [K , T ] F-T-TDict ` label F-T-RangeNat F-TK-TKeys ` label ` N<e type F-T-PDict ` T type ` K partial key ` TDict [K , T ] type ` T type ` PDict [K , T ] type (Typing Rules) `e,T T-I-SubsFull T-I-SubsSub p ; ` e ) T 1 ,..., n ` ei ( `e,T p ; ` e ) T 1 ,..., n Scalarstat N ` ei ( p ; ` e [e1 , .. , en ] ) T T-I-LookupTotal p ; ` e ) TDict [K , T ] p ; ` e [e0 ] ) T k<n Scalarstat N p ; ` e [e1 , .. , ek ] ) T k+1 ,..., n (Typing Rules) ` e0 ( K T-I-LookupPartial T-C-KeysApprox p;`e ) T p ; ` e ) PDict [K , T ] ` e0 ( [keys(e)] p ; ` e [e0 ] ) T ` e ( SetT ` e ( [keys(e0 )] ※更に、像を取るスライスによる添え字の規則もあり（判断図の形で書くにはやや複雑） 38
添え字の検査 • 現状：型検査時と評価器は分離されているた め、評価を必要としない範囲のみ検査 • 次元は確定自然数値であるため、添え字 の成分数は厳密に検査（T-I-Subs* / T-ILookup*） • 各成分ごとの境界検査は、上からの近似 を考えた型検査のみを行っている （T-I-Subs* / T-C-KeysApprox） ` T type, . . . (Formation Rules) F-TK-RngNat F-TK-CatLab ` N<e type ` N<e total key F-T-CatLab ` ` total key ` [keys(e)] total key ` K total key ` ` type ` e ( Scalarstat N p ; ` e ) TDict [K , T ] F-T-TDict ` label F-T-RangeNat F-TK-TKeys ` label ` N<e type F-T-PDict ` T type ` K partial key ` TDict [K , T ] type ` T type ` PDict [K , T ] type (Typing Rules) `e,T T-I-SubsFull T-I-SubsSub p ; ` e ) T 1 ,..., n ` ei ( `e,T p ; ` e ) T 1 ,..., n Scalarstat N ` ei ( p ; ` e [e1 , .. , en ] ) T T-I-LookupTotal p ; ` e ) TDict [K , T ] p ; ` e [e0 ] ) T k<n Scalarstat N p ; ` e [e1 , .. , ek ] ) T k+1 ,..., n (Typing Rules) ` e0 ( K T-I-LookupPartial T-C-KeysApprox p;`e ) T p ; ` e ) PDict [K , T ] ` e0 ( [keys(e)] p ; ` e [e0 ] ) T ` e ( SetT ` e ( [keys(e0 )] ※更に、像を取るスライスによる添え字の規則もあり（判断図の形で書くにはやや複雑） 38
添え字の検査 • 現状：型検査時と評価器は分離されているた め、評価を必要としない範囲のみ検査 • 次元は確定自然数値であるため、添え字 の成分数は厳密に検査（T-I-Subs* / T-ILookup*） • 各成分ごとの境界検査は、上からの近似 を考えた型検査のみを行っている （T-I-Subs* / T-C-KeysApprox） • 課題： ` T type, . . . (Formation Rules) F-TK-RngNat F-TK-CatLab ` N<e type ` N<e total key F-T-CatLab ` ` total key ` [keys(e)] total key ` K total key ` ` type ` e ( Scalarstat N p ; ` e ) TDict [K , T ] F-T-TDict ` label F-T-RangeNat F-TK-TKeys ` label ` N<e type F-T-PDict ` T type ` K partial key ` TDict [K , T ] type ` T type ` PDict [K , T ] type (Typing Rules) `e,T T-I-SubsFull T-I-SubsSub p ; ` e ) T 1 ,..., n ` ei ( `e,T p ; ` e ) T 1 ,..., n Scalarstat N ` ei ( p ; ` e [e1 , .. , en ] ) T T-I-LookupTotal p ; ` e ) TDict [K , T ] p ; ` e [e0 ] ) T k<n Scalarstat N p ; ` e [e1 , .. , ek ] ) T k+1 ,..., n (Typing Rules) ` e0 ( K T-I-LookupPartial T-C-KeysApprox p;`e ) T p ; ` e ) PDict [K , T ] ` e0 ( [keys(e)] p ; ` e [e0 ] ) T ` e ( SetT ` e ( [keys(e0 )] ※更に、像を取るスライスによる添え字の規則もあり（判断図の形で書くにはやや複雑） 38
添え字の検査 • 現状：型検査時と評価器は分離されているた め、評価を必要としない範囲のみ検査 • 次元は確定自然数値であるため、添え字 の成分数は厳密に検査（T-I-Subs* / T-ILookup*） • 各成分ごとの境界検査は、上からの近似 を考えた型検査のみを行っている （T-I-Subs* / T-C-KeysApprox） • 課題： • SMT や egglog による踏み込んだ境界検 査（応用済の egglog の利用を検討中） ` T type, . . . (Formation Rules) F-TK-RngNat F-TK-CatLab ` N<e type ` N<e total key F-T-CatLab ` ` total key ` [keys(e)] total key ` K total key ` ` type ` e ( Scalarstat N p ; ` e ) TDict [K , T ] F-T-TDict ` label F-T-RangeNat F-TK-TKeys ` label ` N<e type F-T-PDict ` T type ` K partial key ` TDict [K , T ] type ` T type ` PDict [K , T ] type (Typing Rules) `e,T T-I-SubsFull T-I-SubsSub p ; ` e ) T 1 ,..., n ` ei ( `e,T p ; ` e ) T 1 ,..., n Scalarstat N ` ei ( p ; ` e [e1 , .. , en ] ) T T-I-LookupTotal p ; ` e ) TDict [K , T ] p ; ` e [e0 ] ) T k<n Scalarstat N p ; ` e [e1 , .. , ek ] ) T k+1 ,..., n (Typing Rules) ` e0 ( K T-I-LookupPartial T-C-KeysApprox p;`e ) T p ; ` e ) PDict [K , T ] ` e0 ( [keys(e)] p ; ` e [e0 ] ) T ` e ( SetT ` e ( [keys(e0 )] ※更に、像を取るスライスによる添え字の規則もあり（判断図の形で書くにはやや複雑） 38
添え字の検査 • 現状：型検査時と評価器は分離されているた め、評価を必要としない範囲のみ検査 • 次元は確定自然数値であるため、添え字 の成分数は厳密に検査（T-I-Subs* / T-ILookup*） • 各成分ごとの境界検査は、上からの近似 を考えた型検査のみを行っている （T-I-Subs* / T-C-KeysApprox） • 課題： • SMT や egglog による踏み込んだ境界検 査（応用済の egglog の利用を検討中） • 辞書の像を取る操作の対応 ` T type, . . . (Formation Rules) F-TK-RngNat F-TK-CatLab ` N<e type ` N<e total key F-T-CatLab ` ` total key ` [keys(e)] total key ` K total key ` ` type ` e ( Scalarstat N p ; ` e ) TDict [K , T ] F-T-TDict ` label F-T-RangeNat F-TK-TKeys ` label ` N<e type F-T-PDict ` T type ` K partial key ` TDict [K , T ] type ` T type ` PDict [K , T ] type (Typing Rules) `e,T T-I-SubsFull T-I-SubsSub p ; ` e ) T 1 ,..., n ` ei ( `e,T p ; ` e ) T 1 ,..., n Scalarstat N ` ei ( p ; ` e [e1 , .. , en ] ) T T-I-LookupTotal p ; ` e ) TDict [K , T ] p ; ` e [e0 ] ) T k<n Scalarstat N p ; ` e [e1 , .. , ek ] ) T k+1 ,..., n (Typing Rules) ` e0 ( K T-I-LookupPartial T-C-KeysApprox p;`e ) T p ; ` e ) PDict [K , T ] ` e0 ( [keys(e)] p ; ` e [e0 ] ) T ` e ( SetT ` e ( [keys(e0 )] ※更に、像を取るスライスによる添え字の規則もあり（判断図の形で書くにはやや複雑） 38
型システム：まとめと課題 • 単純型付λ-計算 + 限定的な依存型 + 束論的部分型 + 辞書・配列・ストリーム • 高階関数は束縛変数の表現に必要 • 型推論は双方向型付けの適用モードありの変種 • 数理最適化ドメインとよくフィット：λ-抽象は有界、変数は全て型付、多相型不要 • 変数以外の型註釈構文なしにモデルの記述が出来ている • 拡張性・保守性が高い • 添え字の境界条件のための限定的依存型：ストリームが定めるsubtypeと、有界自然数型 • 課題 • メタ理論（強正規化はエラーを値と思えば明らか、保存補題はconj.） • ステージの一般化：カテゴリカル変数などが入ると今の定式化は破綻し得る • 様相などによる多段階計算のアイデアを使えないか？ • SMTや等式飽和による添え字の境界検査の厳密化 • Python の漸進的型付け機構との動的な連携 39
まとめ 42
まとめ • 数理最適化ドメインへのプログラミング言語理論の応用を紹介した • JijModeling 2 = 数理最適化モデラー Python EDSL (in Rust) ★ 貢献1：高階関数を含むモデルの可読性の高い数式出力を、プログラム変換・最 適化の問題として捉え、内包表記への加糖の手法を提案 • 最適化には egglog[22] による等式飽和+論理プログラミングを利用 ★ 貢献2：「Henkin定数」を用いた egglog ベースの宣言的制約検出 • 今後の課題：高速化、「Henkin 定数」の正当化、Slotted e-Graph ★ 貢献3：数理最適化向け型システム • 限定的な依存型、代数的な部分型システム • 今後の課題：厳格な型検査、漸進的型付けとの相性の研究、メタ理論の確 立、多段階計算の応用？ 43
参考文献（抜粋） [2] Arthur Charguéraud. “The Locally Nameless Representation”. in: Journal of Automated Reasoning 49.3 (Oct. 1, 2012), pp. 363–408. doi: 10.1007/s10817-011-9225-2. url: https://doi.org/10.1007/s10817-011-9225-2. [3] Jana Dunfield and Neel Krishnaswami. “Bidirectional Typing”. in: ACM Comput. Surv. 54.5 (May 2021). issn: 0360-0300. doi: 10.1145/ 3450952. url: https://doi.org/10.1145/3450952. [4] Hiromi Ishii, Taro Shimizu, and Toshiki Teramura. Optimizing Optimizations: Case Study on Detecting Specific Types of Mathematical Optimization Constraints with E-Graphs in JijModeling. Presented at EGRAPHS ’25. 2025. url: https://arxiv.org/abs/2506.06495. [8] JIJ, Inc.. What is OMMX? – OMMX. 2025. url: https://jij-inc.github.io/ommx/en/introduction.html (visited on 03/31/2025). [13] Shayan Najd and Simon Peyton Jones. “Trees that Grow”. in: JUCS - Journal of Universal Computer Science 23.1 (2017), pp. 42–62. issn: 0948-695X. doi: 10.3217/jucs-023-01-0042.eprint: https://doi.org/10.3217/jucs-023-01-0042. url: https://doi.org/10.3217/jucs-023-01-0042. [21] Ningning Xie and Bruno C. d. S. Oliveira. “Let Arguments Go First”. in: Programming Languages and Systems. ed. by Amal Ahmed. Cham: Springer International Publishing, 2018, pp. 272–299. isbn: 978-3-319-89884-1. [22] Yihong Zhang et al. “Better Together: Unifying Datalog and Equality Saturation”. in: Proc. ACM Program. Lang. 7.PLDI (June 2023). doi: 10.1145/3591239. url: https://doi.org/10.1145/3591239. [23] 寺村 俊紀, 清水 太郎, and 石井 大海. “数理最適化の実用化を支援する OMMX のデータ形式標準化の取り組み”. in: 人工知能学会全国 大会論文集. vol. JSAI2025. Slides: https://www.docswell.com/s/Jij_Inc/5YD44V-2025-05-30-jij. 2025, 4P1OS17a04–4P1OS17a04. doi: 10.11517/pjsai.JSAI2025.0_4P1OS17a04. [24] 石井 大海, 清水 太朗, and 寺村 俊紀. “数理最適化モデル記述ツール JijModeling のご紹介”. in: 人工知能学会全国大会論文集. vol. JSAI2025. Slides: https://www.docswell.com/s/Jij_Inc/59VP3V-2025-05-30-jijmodeling. 2025, 4P1OS17a05–4P1OS17a05. doi: 10.11517/ pjsai.JSAI2025.0_4P1OS17a05. 44
御清聴ありがとうございました We Are Hiring! • 休憩時間等にスポンサーブースにいます！議論しましょう！ • JIJ では JijModeling や量子計算向けEDSL Qamomile の開発者を募集しています！ 4
Any Questions? • 数理最適化ドメインへのプログラミング言語理論の応用を紹介した • JijModeling 2 = 数理最適化モデラー Python EDSL (in Rust) ★ 貢献1：高階関数を含むモデルの可読性の高い数式出力を、プログラム変換・最 適化の問題として捉え、内包表記への加糖の手法を提案 • 最適化には egglog[22] による等式飽和+論理プログラミングを利用 ★ 貢献2：「Henkin定数」を用いた egglog ベースの宣言的制約検出 • 今後の課題：高速化、「Henkin 定数」の正当化、Slotted e-Graph ★ 貢献3：数理最適化向け型システム • 限定的な依存型、代数的な部分型システム • 今後の課題：厳格な型検査、漸進的型付けとの相性の研究、メタ理論の確 立、多段階計算の応用？ 46
Appendix 47
➡︎
JijModeling の値中間表現
value, k, v
Back
value
::=
fp
floating-point number
|
>
true
|
|
?
false
p.e
abs
(v1 , ... , vn )
tuple
[. . . [[vij...00 , . . . , vij...0n ], . . .], . . .]
array
|
{k1 ) v1 , . . . , kn ) vn }
dict
v Q v0
comparison
|
f
function
|
n
neutral term
err
error
|
|
|
|
|
|
stream
function, f
function
::=
|
fp
floating-point number
|
xi
decision variable
|
f
negation
|
f + f0
addition
|
f
subtraction
|
multiplication
|
f · f0
f /f 0
division
|
sin f
sine
|
f0
...
• OMMX の目的関数・ 制約条件に抽出される
• 配列・辞書は添え字からの関数として表現する遅延表現
• 数十万要素の配列の clone を避けるため
• ボーナス：疎配列との統一的な扱いも可能
48
➡︎ 内包表記の脱糖規則 ~ C { p } e, ~ ] [e|C (内包表記の脱糖) e0 D-Comp-ForInCons D-Comp-ForIn for p in e Back ~ C ~ for p in e C; {p} e D-Comp-IfCons ~ C ~ if e C; { p } e0 { p } filter( p. e, e0 ) { p0 } e 0 { (p0 , p) } flat_map( p0 . map( p. (p0 , p), e), e0 ) D-Comp-ListComp ~ C ~ ] [e|C { p } e0 map( p. e, e0 ) 49
➡︎ 内包表記加糖：残りの egglog 規則 Back (with-ruleset propagate (rule ((focus (Compr e s))) ((concludes e) (assert s))) (rule ((assert (Then l r))) ((assert l) (assert r))) (rule ((assert (Let (Tuple p) (Tuple e)))) ((union p e))) (rule ((= (Cons p ps) (Cons e es))) ((union p e) (union ps es))) (rule ((= (Tuple ps) (Tuple es))) ((union ps es)))) (rule ((assert (Let (Var p) (Var e)))) ((union (Var p) (Var e))) :ruleset equate-vars) (with-ruleset inline-trailing-assignment (rule ((= let-var (Let (Var p) e)) (assert (Then l let-var))) ((union (Var p) e) (union (Then l let-var) l) (set-cost (Var p) 10000)) ) (rule ((= let-tup (Let (Tuple p) e)) (assert (Then l let-tup))) ((union (Tuple p) e) (union (Then l let-tup) l) (set-cost (Tuple p) 10000)) )) 50
Back
@jm.Problem.define("Restricted TSP")
def problem(prb: jm.DecoratedProblem):
C = prb.CategoryLabel(description="Cities")
N = prb.DependentVar(C.count(), description="Number of cities")
d = prb.Float(dict_keys=(C,C), partial_dict=True,
description="distance between city $c$ and city $c'$")
x = prb.BinaryVar(dict_keys=(N, C),
description=r"$x_{t,i} = 1$ iff city $i$ is visited at step $t$")
prb += prb.Constraint(
"one-time", [jm.sum(x[t, i] for t in N)
prb += prb.Constraint(
"one-city", [jm.sum(x[t, i] for i in C)
prb += jm.sum(
d[i, j] * x[t, i] * x[(t + 1) % N, j]
for t in N for i in C for j in C
)
1 for i in C])
1 for t in N])
=
=
=
51
=
➡︎
制限つきTSPのコード例