Formurae

Formurae は、Egison のテンソル添字記法で書いた偏微分方程式を Formura の stencil programへ変換し、 MPI・temporal blocking付きC codeを生成するための実験的な言語処理系です。

表層言語の拡張子は .fme です。数式の意味と離散化を分離し、次の4段で処理します。

model.fme
  └─ formurae-pre ──> model.egi
                    └─ Egison ──> model.feir
                                      └─ formurae-post ──> model.fmr
                                                         └─ Formura ──> C

• formurae-pre は構文、scope、宣言、source mapを検査し、Egison normalization unitを生成します。
• Egison はuser definition、tensor/index algebra、analytic differentiationを評価し、canonical FEIRを出力します。
• formurae-post はplacement、stencil、補助field、storageを決め、Formura programを生成します。
• Formura は配列、loop、MPI通信、temporal blockingを含むC codeを生成します。

純粋な数学演算子はEgisonにだけ定義されます。grad、divg、curl、hessian、lap、 d、hodge、δ、Δ_Hの解析的な部分は、callbackやcomponent loopを含まない短いEgison関数です。 具体的な差分係数や格子offsetをEgisonの演算子定義へ混ぜません。

user tensor operatorも同じ経路です。例えば次のwithSymbolsを出た自由な下添字は、Egisonでは 添字を省略したtensor軸になります。省略軸には既存の明示添字とは異なるfreshな下添字が補われ、 formurae-preは関数名や本体からresult varianceのsignatureを推論・付与しません。EgisonがRHSを評価した後、 宣言済みのequation targetまたはindexed localへ値を格納する時点で、targetが要求するshape、logical variance、dfOrderと実際の値を照合します。degree-zero covariant tensor targetへ代入する場合に限り、 構造的index completionがcompatibleなanonymous down軸をtargetの下添字へ対応付けます。anonymous down軸を up targetとして読み替えることはできず、form targetではdfOrderを保持します。

def gradLike u = withSymbols [i] (∂_i u)
field q_i
step:
  q' = gradLike u

したがって、E_i + gradLike uのanonymous軸が既存のiへ暗黙に統合されることはありません。 この式では両者は別の軸です。同じ軸で合成する意図は、 withSymbols [i] (E_i + (gradLike u)..._i)のようにcall siteで下添字を明示できます。

pure user operatorの本体は1行に限定されません。=の次をindentすると、Egisonのlet、lambda、 match、withSymbols、generateTensorを含む式blockをそのままnormalizationへ渡せます。 1行の本体とこのようなrich bodyは、どちらもEgisonが通常の式として評価します。Formuraeはuser definitionの式構造や計算履歴を検査してresult signatureを付けません。評価結果がfield equation またはindexed localへ格納されるときだけ、上記のtarget metadata照合を行います。

def chooseByDimension X =
  let apply := \f x -> f x
      choose := match dimension = 3 as bool with
        | #True -> \Y -> 2 * Y
        | #False -> \Y -> Y
   in apply choose X

dimension、coordinates、volume、epsilon、metric、inverseMetricはmodelのambient Egison環境にあり、ユーザ定義とFormurae.*標準演算子はこれらを直接参照します。 そのためユーザがcontext引数を渡す必要はありません。metric gを宣言すると、同じ実計量を 共変なg_i_j（whole viewはg_#_#）と反変なg~i~jから参照できます。宣言名を使わない canonical viewはmetric_i_j / metric_#_#とinverseMetric~i~jです。反変なviewは、次のように varianceが見えるindexed equation/localで直接使います。

metric scale [1, 1 + x]
metric g

field A_i
field X~i

step:
  X'~i = withSymbols [j] (g~i~j . A_j)
  A'_i = withSymbols [j] (g_i_j . X~j)

この明示的な計量縮約を正準な書き方とし、flat / sharpはFormuraeのpublic operatorとして 提供しません。関数headへ結果添字を書く構文もありません。

ambient名とmetric gの宣言名はfield、parameter、user definition、definition parameter、 step-level let / localでは予約されます。Egison expression block内の局所letやlambdaだけは 通常のlexical scopeに従います。

最小例

mode collocated
dimension 3
axes x, y, z

param κ = 1.0
param dt = 0.1*dx*dx

field u : scalar

init:
  u = gauss(i*dx,j*dy,k*dz)

step:
  u' = u + dt * κ * Δ u

Δはmode collocatedのcanonical scalar Laplacianです。精度に依存しないため、 4次精度へ変更するときも別の数学演算子を定義せず、model-level profileを追加します。

discretization collocated derivative 2 centered accuracy 4

EgisonはgeometryのないΔ uを二階のFieldJetへ正規化し、formurae-postが4次精度を満たす最小半径2の compact 5点stencilをexact rational coefficientで導出します。一階wide stencilを二重適用しません。

微分の意味

通常の∂は解析微分です。

∂_x (u * u)          -- Egison: 2 * u * FieldJet(u,{x:1})

未知の解析微分則を0とみなすことはなく、Egisonの∂/∂がerrorにします。 混合偏微分はcanonicalなmulti-indexへまとめられます。

式全体を先に格子上で評価してから差分したい保存形では、微分式をbackquoteします。

`(∂_x (u * u / 2))  -- product ruleを開かないwhole-expression差分

入れ子のbackquoteは、内側からの軸順と重複を保ちます。

`(∂_y (`(∂_x (`(∂_x q))))  -- x, x, yの順に適用

配置変換を意図的に行う場合の明示surfaceはresampleです。

resample(q, 0, 1)   -- 2Dの絶対placement (integer, half) へ線形補間

中間storageは型付きlocalで指定します。face fluxを明示する保存形は、 次のように通常のdivgと合成できます。

field u : scalar @ primal

step:
  local q_i @ primal = [| -κ * `(∂_x u), -κ * `(∂_y u) |]_i
  u' = u - dt * divg q

q_i @ primalは成分ごとに対応軸のfaceへ保存され、divg qはcellへ戻る差分を作ります。 このtelescopingによる保存保証は周期境界、または同じfluxと整合するghost/boundary処理の下でのものです。 現在の.fmeは物理境界条件自体を宣言せず、Formura側のYAML・boundary設定が権威です。

Tensor、form、格子配置

fieldはscalar、vector、rank-1/rank-2 tensor、k-formを宣言できます。

field E_i @ primal
field B_i @ dual
field σ{~i~j} @ primal
field A : 1-form
field F : 2-form

step:
  local q_i @ primal = [| 0, 0, 0 |]_i
  local ω : 2-form @ primal = d A

配置はCollocated、Primal、Dualのいずれかです。Primal/Dualの具体的な半セル位置は field policyとcomponent basisのparityからformurae-postが推論します。異なるplacement間の補間は 暗黙に行わず、必要ならresample(value, bit...)を使います。

Maxwellはcollocated vector、Yee vector、DEC formの各形式で記述できます。

mode dec
dimension 3
axes x, y, z

field E : 1-form
field B : 2-form

step:
  E' = E + dt * δ B
  B' = B - dt * d E'

mode decのcanonical form演算子はd、hodge、δ、Δ_Hです。 δは余微分、Δ_H A = d (δ A) + δ (d A)はHodge--de Rham Laplacianです。 宣言幾何のδはpreludeマクロとしてdFluxWeights/dFluxScale/dFluxDivへ展開され、幾何のみの係数localはformurae-postがinit凍結のstate配列にします。 Δ_Hはconstant geometryでのpureな合成をサポートし、general variable-metric formは現IRで表せないためcompile-time errorにします。 これらのform演算子は宣言済みscalar/k-formだけを受け取り、ordinary tensorを暗黙にformへ変換しません。 quoted derivativeとcollocated scalar Δもscalar-onlyです。型annotationを持たないuser def parameterの kindは証明できないため、typed operatorはfield、typed local、またはkindが確定したstep式へ直接適用します。 indexed δ~i_jは余微分とは別のKronecker tensorで、ASCII名deltaのuser定義にも捕捉されません。 d(d A) = 0は演算子ライブラリの定理としてcompiler suiteが検査し、離散的な div B = 0の保存は各exampleのcheck driverが実測します。

GeometryとLaplace--Beltrami

直交計量はscale factorまたはembeddingで宣言します。

axes θ, φ, z
embedding [ `(2 + cos θ) * cos φ, `(2 + cos θ) * sin φ, sin θ, z ]

step:
  u' = u + dt * Δ u

Egisonはmetric、inverse metric、scale factor、volumeを記号的に作り、embeddingでは直交性を 検査します。geometryを宣言したモデルのΔ uはpreludeマクロとして、実体化した重み・flux localと符号付きadjoint divergenceへ展開されます。FEIRに残るのはordinaryなMaterialize actionとwhole-operandなderivative.grid-whole requestだけで、幾何のみの係数local はformurae-postが凍結してinit一回+恒等carryのpersistent stateにします(mirror/fixed壁の 境界処理もstate配列として宣言どおりに受けます)。

FEIR

FEIR (Formurae Egison IR) はEgisonとformurae-postのcanonical protocolです。その同一性は 手で振る版番号ではなくfingerprint(内容ハッシュ)が固定します。

.fme のgeometry、:= analytic initializer、step、parse可能なdefに書いた 小数・指数リテラルは、formurae-preが綴りどおりのexact rationalへ変換します。 raw Egison def本体と= raw initializerはEgisonのFloat/生文字列の意味論を保ちます。 有限なdouble backendへ安全に下ろせない指数、または約分後の分子・分母をbinary64へ 正確に渡せない非整数リテラルは、丸めて続行せずcompile-time errorにします。 Unicode π はEgison CASでシンボリックに簡約され、残った値はFEIRの (named-constant pi)としてformurae-postまで保持されます。FMRをrenderするときだけ、binary64のπと 同値で両operandが2^53未満の(884279719003555 / 281474976710656)へ変換します。 ASCII piはEgisonのFloatと衝突するためaliasではありません。parameter値と= raw initializerは symbolic FEIRを通らないので、そこではπを使わずbackend数値を明示します。

• exact rationalを保持するcanonical S-expression
• closedなnamed mathematical constant
• stable AxisId、FieldId、FunctionId、OriginId
• scalar/tensor normal formとderivative multi-index付きFieldJet
• GeometryNF、discretization profile、opaque discrete request
• registry/primitive-manifest/profile fingerprint
• .fmeのpath・line・columnとdefinition expansion trace

list nodeの順序はcanonical S-expressionをrenderしたbyte列で決まり、Egison encoderとHaskell validatorが同じ規則を使います。decoderはwire順を保持するため、非canonicalな入力順をparse時の sortで隠さずhard errorにします。

成功したEgison stageのstdoutはFEIR 1個だけです。diagnosticはstderrへ分離され、warning、type error、 evaluation error、余分なstdoutはmachine runnerが拒否します。

クイックスタート

インストール

Formurae、Egison、検証済みFormuraはすべてCabalでインストールできます。 cabal installの実行ファイルディレクトリ(通常は~/.local/bin)をPATHに加えてください。

cabal install egison-5.1.0

git clone https://github.com/egison/formura.git
cd formura
git checkout 3bc74b5c6f1a24dfffe869839d75fd44b8aa2eb0
cabal install exe:formura --overwrite-policy=always
cd ..

git clone https://github.com/egison/formurae.git
cd formurae
cabal install exe:formurae exe:formurae-pre exe:formurae-post \
  --overwrite-policy=always

一括CLIは.egi、.feir、.fmrを入力ファイルと同じディレクトリへ書き、 compileでは続けてFormuraを呼び出します。

formurae compile examples/diffusion3d/diffusion3d.fme
formurae lower examples/diffusion3d/diffusion3d.fme

compileには入力と同じbasenameの.yamlが必要です。lowerは.fmr生成で停止します。 EGISON、FORMURA、FORMURAE_PRE、FORMURAE_POST環境変数で各実行ファイルを明示できます。

開発と検証

リポジトリ全体の試験はGHC 9.6系、隣接する../egison開発tree、および検証済みFormuraを使います。 make setupはFormuraを固定commitからCabalでbin/formuraへインストールします。 1-rank用MPI stubを同梱しています。

make setup
cabal build
make diffusion3d
make maxwell3d_yee
make metric_torus

make NAMEは.fme -> .egi -> .feir -> .fmr -> C -> checkを通します。全例は次で検証できます。

make all

各stageを直接確認する場合:

cabal run -v0 formurae-pre -- examples/diffusion3d/diffusion3d.fme > /tmp/model.egi

tools/run_formurae_normalization.sh ../egison \
  /tmp/model.egi > /tmp/model.feir

cabal run -v0 formurae-post -- /tmp/model.feir > /tmp/model.fmr

生成物

.fmeが編集対象です。27個のFME例では.egi、.feir、.fmrをreview可能な生成artifactとして 追跡し、Makefileから再生成します。galleryは4段すべてを表示します。mhd_otは19本の保存流束を typed localとして物質化し、lbm_d3q19は中心1階・2階差分の恒等式で整数1セルpullを構成して、 どちらも通常の.fme -> .egi -> .feir -> .fmr経路で検査します。LBMの19成分宣言と式を速度集合から 自動展開するfield f : family 19構文は、記述量をさらに減らす将来の表層機能です。

リポジトリ構成

パス	役割
app/formurae/	インストール済みtoolchainを駆動する一括CLI
app/formurae-pre/	Formurae frontend CLI
app/formurae-post/	FEIR validation・discretization・Formura backend CLI
src/Formurae/FEIR/	FEIR syntax、codec、validation、fingerprint
src/Formurae/Pre/	parse、registry、effect analysis、Egison emitter
src/Formurae/Post/	placement、stencil、geometry/backend plan、FMR AST/printer
lib/formurae-operators.egi	pure continuum operatorとopaque request constructor
lib/formurae-primitives.egi	primitive manifestから自動生成するfull-signature binding
lib/formurae-feir.egi	MathValue/Tensorからcanonical FEIRへのencoder
spec/feir-primitives.sexp	5 primitiveのfull signatureを規定する唯一のmanifest source
spec/egison-normalization.list	Egison normalization libraryの規範load順
examples/	model、生成artifact、C numerical check
gallery/	galleryのasset(画像・動画・データ)と生成スクリプト
html/ja/・html/en/	gallery・usage guideのHTML(日本語/英語)

galleryの時間場は、初期・最終画像の補間ではなく、数値計算中に等間隔で保存した実データから H.264動画を生成します。ffmpegを用意し、全exampleのC生成後に次を実行します。

make all
make gallery-assets

gallery/gen.shが静止画用snapshotと動画frame dataを同じrunで生成し、 render.pyが静止画、render_video.pyが全フレーム共通の色スケールで動画を描画・encodeします。 誤差曲線、厳密解比較、時空図は検証情報を同時に読める静止図のまま保持します。

検証

変更は次の層で検査します。

make compiler-tests
make all

• FEIR round-trip、malformed input、fingerprint、source diagnostic
• formurae-pre scope/effect/ambient-binding tests
• Egison analytic differentiation、FieldJet、tensor/form operator tests
• formurae-post profile、exact Taylor stencil、placement、quoted derivative、geometry-aware Δ / δ tests
• collocated/Yee/DEC/variable-metric exampleのFormura parseとC numerical checks
• Egison math representative samples、mini-test全件、cabal test

現在の受入れ基準は tests/compiler_suite.sh、個別の tests/*.sh、および Makefile の 検証targetに実行可能な形で保持します。

設計上、旧fec CLI、旧generated .egi schema、callback/marker based loweringとの後方互換性は 提供しません。仕様変更時はexample、document、testを新しい意味へ同時に更新します。

関連資料

• DSL-DESIGN.md: 表層構文と設計履歴
• html/ja/usage.html/html/en/usage.html: tutorialとusage guide
• html/ja/gallery.html/html/en/gallery.html: 検証済み応用のgallery
• APPLICATIONS.md: 応用例一覧
• UPSTREAM.md: Formura側の拡張計画

ライセンス

MIT。Formura本体とvendor sourceはそれぞれのlicenseに従います。