GV

GeezerVison

The World Wide Web, restored to 800 pixels of glory.

Home|About|Gaming cabinet|Archives|How it works|Starter sites

On this site

  • Sign in
  • ActionsCI/CD and automation
  • CodespacesCloud development environments
  • All Features
  • Documentation
  • Training
  • Certifications
  • Build with Copilot
  • Customize Copilot
  • Integrations
  • Trending repos
  • GitHub Sponsors
  • Developer articles
  • Enterprises

This view

  • Original page
  • New address

GeezerVison is showing github.com — GitHub - egison/formurae

BranchesTags
Open more actions menu

Latest commit

 

History

249 Commits
249 Commits

Folders and files

NameName
Last commit message
Last commit date
TODO
TODO
 
 
app
app
 
 
benchmarks
benchmarks
 
 
examples
examples
 
 
figures
figures
 
 
formura-patch
formura-patch
 
 
future-work
future-work
 
 
gallery
gallery
 
 
html
html
 
 
lib
lib
 
 
mpistub
mpistub
 
 
spec
spec
 
 
src/Formurae
src/Formurae
 
 
tests
tests
 
 
tools
tools
 
 
upstream
upstream
 
 
.gitignore
.gitignore
 
 
AGENTS.md
AGENTS.md
 
 
APPLICATIONS.md
APPLICATIONS.md
 
 
CHANGELOG.md
CHANGELOG.md
 
 
DEVELOPMENT.md
DEVELOPMENT.md
 
 
DSL-DESIGN.md
DSL-DESIGN.md
 
 
LICENSE
LICENSE
 
 
Makefile
Makefile
 
 
README.md
README.md
 
 
Setup.hs
Setup.hs
 
 
UPSTREAM.md
UPSTREAM.md
 
 
formurae.cabal
formurae.cabal
 
 
setup.sh
setup.sh
 
 

Repository files navigation

Formurae

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

例題・デモ・ベンチマークは、Formura 本体を拡張せず、既存の機能と通常のコード生成経路で 実装できるシミュレーションを対象にします(例外として、境界のある領域での時間方向の ブロッキングと MPI 分割は 2026-09-12 にユーザー指示で fork に実装しました)。近傍格子点を参照する局所更新を中心に、 初期条件・境界処理・補助計算も含めて実装可能性を確認します。 開発時の詳細は AGENTS.md に従います。

表層言語の拡張子は .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で下添字を明示できます。 Egisonと同じ(gradLike u)_iという綴りも同じ意味で使えます。括弧でくくった式の直後に 添字をつける書き方はinit・step・defのどこでも構造化された式として解析され、 (gradLike u)_i . Q~i~jのように.による縮約とも組み合わせられます。 引数なしで定義したテンソル値にも,christoffel~i_1_lのように数値添字を使って 成分を取り出せます。

def は引数を省略すると値を定義します。先に定義した値を名前だけで参照でき, 使わない仮引数や呼び出し時の 0 は不要です。例えば,座標 x, y とパラメータ cx, cy に対して, 次のように書けます。

def u = `(x - cx)
def v = `(y - cy)
def rr = sqrt (u^2 + v^2)

スカラーだけでなくテンソルや関数も値として定義できます。引数を持つ定義と同様に, 自分自身や後に現れる定義への参照はエラーになります。バッククォートは,くくった式を 記号計算中に展開せずひとまとまりとして扱う指示です。

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

generateTensor は def の本体で使えます。例えば、9成分の平衡分布を 1つの式から作り、初期化で利用できます(weights・cx・cy は重みと移動方向の表です)。

def equilibriumPopulations r u v =
  generateTensor (\[q] -> equilibrium weights_q cx_q cy_q r u v) [9]

init:
  f_a := (equilibriumPopulations initialDensity initialU 0)_a

q は1〜9の整数で、_a は生成した9成分に付ける添字記号です。 生成はEgisonでの正規化時に行われ、実行時のテンソル生成処理は増えません。 完全な使用例は 二次元の波 にあります。

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に従います。

空間次元と独立した成分数

index a, b : 9 は,添字記号 a と b の範囲をそれぞれ 1〜9 と宣言します。 dimension と axes は引き続き計算領域の空間次元と座標を指定します。 index は場と関数の宣言より前に書きます。

dimension 2
axes x, y
index a, b : 9

field f_a             -- 9成分
field u~i             -- 空間方向の2成分
field c_a~i           -- 9×2成分
field M_a_b           -- 9×9成分

場の各軸のサイズは宣言時の添字で決まります。宣言していない i,j などは, 従来どおり dimension 個の空間方向を表します。同じサイズを宣言した記号への 付け替え(f_a → f_b)は可能ですが,f_i として2成分に読み替えることはできません。 数値添字 f_9 は第9成分を取り出します。

static field,添字を明示した local / let,関数の添字付き引数でも同じ指定を使えます。 例えば,9成分の場を各成分で拡散させる更新は次のように書けます。

def diffuse X_b = X_b + dt * (∂^2_x X_b + ∂^2_y X_b)
step:
  local next_a = diffuse f
  f'_b = next_b

上付きと下付きの同じ添字を . で縮約する,つまりその成分について和を取ると, weights~a . f_a は9項の和になります。∂_i f_a では i が空間方向,a が成分番号です。 実行検査用の例は,拡散,縮約,空間微分, 9×2の場,対称・反対称な3×3の場を含みます。

明示した index は空間方向ではありません。index a : 2 と空間次元が同じ場合でも, ∂_a や空間の計量 g_a_b には使えません。@ primal / @ dual による格子配置も 空間方向の添字だけで決めます。例えば c_a_i @ primal は,すべての a について i の方向に半格子だけずらします。

サイズには正の整数を指定します。対称・反対称な場の2軸には同じサイズと種類 (両方とも空間方向,または両方とも成分番号)が必要です。微分形式の軸は空間方向のままです。 index 宣言があるモデルの局所場には local q_a や local q_a_i のように添字を 明示します。local q : tensor の推論は,空間方向だけを使うモデルで利用できます。 場の対応範囲は従来と同じで,通常の添字付きの場は2軸までです。

弾性波の例と適用条件

壁のある球殻の弾性波の例は,同じプログラムを球座標と, 同じ球殻の非直交座標(経度の線が半径とともに巻く座標系,metric tensor で計量を宣言)で 実行し,剛体の壁(速度を 0 に保つ球面と円錐)で反射しながら P 波と S 波が速さ 2 対 1 で 分離して広がることを示します.origin 宣言で座標を半径と余緯度そのものにし, boundary … : sbp の壁でも時間方向のブロッキングと MPI 分割(壁のある軸の分割を含む)が 通常版とビット単位で一致します.ねじれ振動の厳密なモード(3 次の球 Bessel 関数と $P_3^1$)に対する 2 次収束,エネルギー,波速,二つの座標系の一致を verify.py が確かめ, run.py・render.py が論文の図の実行と描画を行います.

周期領域の弾性波の例は,同じプログラムを直交座標と, 同じ周期立方体の非直交座標(格子線が横に波打つ座標系,metric tensor で計量を宣言)で 実行し,P 波と S 波が速さ 2 対 1 で分離して広がることを示します.演算子は計量・逆計量・ 計量の解析微分をその場で使い,Egison がコンパイル時に展開・簡約した係数を生成された 時間ステップがセルの座標から評価します.時間方向のブロッキングと MPI 分割はそのまま 使えます(Formura のコード生成器がブロッキングされたステップの座標を誤っていた点は fork で修正済み). 初期パルス,波の指標,エネルギー,波速を測るモーメント,平面波厳密解との誤差まで すべて .fme の場として計算し,C ドライバは起動と記録だけを行います.

直交座標の例は周期境界で,4ステップをまとめる 時間方向のブロッキングを設定しています.初期条件と更新式は .fme にありますが, 検証用のエネルギー・波速の計算は C 側に残っています.

球座標の例は壁のある非周期境界を持ちます. 2026-09-12 の Formura の拡張(fork の tb-boundaries,setup.sh が固定する版)により, 壁のある軸でも時間方向のブロッキングと MPI による領域分割が使えるようになり, この例も間隔 2 のブロッキングで生成します.実験の初期値は C 側で設定しています. 同じ制約のあった円筒座標の弾性波は,2026-09-10に例題から削除しました. 壁のある全例題でブロッキング版と分割版(mpicc・mpirun がある場合)が通常版と ビット単位で一致することは make tb-wall-tests(tests/tb_wall_examples.py)が確かめます. 各例の初期化・境界・高速化機能の確認結果は 弾性波の例題調査 にまとめています.

球座標の再現手順と過去の数値結果, 関連研究との比較を参照してください.

巻き込む波と引き波

巻き込む波と引き波は,横から見た二次元の水槽で 水と空気の境界を追跡します.水面が前へせり出す形を,格子ボルツマン法 (格子点間を移動する分布から流れを求める方法)で計算します.初期条件,海底, 水面の更新,水量保存の測定をすべて .fme に記述し,Formura 本体を変更せずに 通常の生成経路で実行します.1つの波が崩れ,岸へ乗り上げた水が沖へ戻る引き波まで計算し, 流れが岸向きから沖向きに変わり,持続することを検査します.make breaking-wave-demo で動画まで生成し, make breaking-wave-verify で静水との比較も検査できます.

三次元版は,3次元空間で19種類の移動速度を使う D3Q19へ拡張し,奥行きによって波高と波の位置が変わる水槽を計算します. index a : 19 で宣言した分布 f_a と,3成分の流速 u_i を使います. 立体の水面と2か所の断面を動画にし,水量保存・静水・奥行き方向の対称性を検査します. 実行と描画は make breaking-wave3d-demo,数値検証は make breaking-wave3d-verify です. 描画用ライブラリの準備は三次元版のREADMEを参照してください. まず二次元の波の巻き込み・崩壊・水際の後退・計算精度・表示を整え, その後に三次元と飛沫へ進める方針を波の開発計画にまとめています. 波の動画と関連する流体の基礎検証は,専用の波のシミュレーション (English)に掲載しています.

座標に依存しない流体モデルに向け, D2Q9の分布の移動を微分方程式で解く実験を 追加しています.同じ更新式を直交座標・間隔が変わる直交座標・非直交の曲線座標で 実行し,一様流,移動の厳密解,粘性で減衰する流れを比較します. make kinetic-coordinates-verify で三つの格子サイズの計算と検証を再現できます.

有限体積法によるD2Q9の輸送では, 面の両側を明示的に選ぶ sampleLower/sampleUpper を使い, 一次風上法と,各セル内の傾きから面の値を求めるMUSCL法を比較します. 傾きを制限し,二段の時間積分を組み合わせることで,分布のぼけを抑えます. 同じ更新式を直交格子と曲がった格子で実行し,9方向それぞれの総量保存, 中間段階を含む非負性,滑らかな移動問題の収束を確認します. make kinetic-fv-verify で48条件の検証,make kinetic-fv-gallery で 保存済みの結果から日英の波の専用ページの更新を再現できます.

衝突と粘性の検証では,この輸送に 分布を平衡状態へ近づけるBGK衝突項を加えます.位置によって横向きの速さが変わる せん断流の減衰を,方程式から導いた参照値と比較します.三つの緩和時間, 直交格子と曲がった格子,格子の細分化で誤差を調べ,質量と運動量の保存も確認します. make kinetic-viscosity-verify で50条件の検証,make kinetic-viscosity-gallery で 日英の波の専用ページの更新を再現できます.

重力と静水の検証では,上下の反射壁と 重力を加え,静水状態からの差を計算することで重力と圧力のつり合いを保ちます. 静水・密度の小さな乱れ・水平加速度による運動量の変化を,直交格子と曲がった格子で 調べます.壁は流体を通さず,接線方向には滑る条件です.領域を流体で満たした試験で, 水面は下記の小振幅の実験へ進めています.make kinetic-hydrostatic-verify で 検証を,make kinetic-hydrostatic-gallery で日英の波の専用ページの更新を再現できます.

小振幅の水面との結合では,上面の壁を 水面の圧力条件へ置き換え,面を通る質量流束(水の流量)で水面の高さも更新します. 静水からの小さな変化の一次の項を残す線形化を用い,同じ微分方程式を直交格子と 曲線格子で解きます.静水,重力0,四段階の格子,時間刻みの半減など16条件で, 線形化した総質量の保存と波の周期・振幅を検査します.make kinetic-surface-verify で検証を, make kinetic-surface-gallery で水面の動画と日英の波の専用ページを再生成します. 動く水面への拡張として,下記の占有率の輸送を検証します.

水の占有率の保存輸送では,各セルを水が占める 割合を0〜1に保ち,水量を保存して運びます.同じ物理的な形状と流れを直交格子・曲線格子で 計算し,波形の横移動と,円形の水領域を渦で伸ばして戻す実験を比較します. 流れを指定した輸送試験であり,D2Q9の圧力・重力とはまだ結合していません. make surface-transport-verify で検証を,make surface-transport-gallery で 二つの動画と日英の波の専用ページを再生成します.

D2Q9の質量輸送との結合では,流体が実際に面を 通して運ぶ質量を共有して,水を表す割合を更新します.密度が変わっても水を表す質量を保存し, 一定の割合を保つことを検査します.全領域に同じ流体を置き,その一部に印を付けた段階です. make kinetic-transport-verify で20条件の検査,make kinetic-transport-gallery で 割合・流速・密度の動画と日英の波のページを再生成します.任意の向きの水面の圧力条件, 重力,新しく水になるセルの初期化,傾斜した海底への結合が次の課題です.

動く自由表面と斜面の開発例では,D2Q9の 微分方程式に大気圧の水面と重力を結合し,水が新しいセルへ入り,斜面を上って戻る過程を 調べています.空中の水の層の自由落下では,厚い層の遅れが占有率の再構成に起因することを 1次元の再現計算で特定し,満杯の隣接セル側へ水を詰める再構成と部分セル内の水の位置を考慮した 重心指標で必須4条件が通過しました.160×64格子の基礎10条件と斜面の静水・粘性の検査も通過しています. 一方,同じ入射波の海岸計算では巻き込みが得られず,新しい再構成は斜めの水面で階段状の段差を 残したため,波の計算には採用していません.巻き込み・空洞・衝突と,薄い水まで含む水際の後退を 検査対象とし,計算の終了と目標の達成を区別して記録します.

材料則と座標変換を変更する応用デモ

三つの比較デモでは,利用者が定義した演算子を 材料モデルや装置の比較に使います.複合材の超音波は 繊維方向と局所的な剛性低下による受信波形の違い,場の回転子は座標変換の回転角と材料層の厚さ, 円筒型電池の冷却は熱伝導の方向依存性と冷却面を比較します. 初期条件・境界処理・更新式・物理量の測定を .fme に記述し,通常の生成経路で実行します. 日英の gallery には比較動画,測定値,ソースと検証結果を掲載しています. make application-demos で計算・検証・動画・gallery を再生成できます(描画用 Python と ffmpeg が必要).

最小例

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

Δは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を二重適用しません。

時間変化しない場

位置ごとに異なっても時間では変化しない係数は、static field で宣言します。

static field G1{_j_k} @ collocated := gammaTheta
static field J : scalar @ collocated := volume
static field twiceJ : scalar @ collocated := 2 * J

右辺は初期化時に宣言された格子配置で一度だけ評価され、以後は値が保持されます。 init への代入や G1' = G1 のような更新式は不要です。 型・添字・格子配置の指定は通常の field と共通です。 右辺には座標、パラメータ、計量、および先に宣言した static field を使えます。 通常の field、後に宣言した固定場、自分自身、次の時刻の値には依存できません。 これらの依存は def の評価後にも検査します。init での再初期化と step での更新もエラーです。 def は式の値を定義し、static field はその値を格子上に保存する点が異なります。

微分の意味

添字つきの ∂ は,式全体を格子上で評価してから差分する微分です.

∂_x (u * u)          -- u*u 全体を参照先の点で評価して差分

計量などを解析的に微分する場合は ∂/∂ を使います. 未知の解析微分則を0とみなすことはなく,Egisonがエラーにします.

通常の1階差分に対する次のbackquoteは同じ意味を持ちます.

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

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

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

解析的な式の中のbackquoteはEgisonへの指示で、くくった部分式を展開せずに一つの原子として扱います。 生成されるプログラムには中身の式がそのまま入ります。座標変換の写像を∂/∂で微分するときに `(x - cx)のように中心をずらした座標を原子にしておくと、正規化が数分から1分程度になります (examples/transformation_optics)。

配置を変えて線形補間する場合は resample を使います。

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

面の両側の値を個別に選ぶ場合は,次の操作を使います.q が整数点にある場合, 小さい/大きい計算座標側のセル値をそのまま選びます.

sampleLower(q, 1, 0)   -- x方向の面に接する小さい座標側の値
sampleUpper(q, 1, 0)   -- 同じ面に接する大きい座標側の値

配置が変わる軸は1つに限ります.定数だけの式,同じ配置,複数軸の同時変更は エラーになります.係数を含め,式全体を選んだ元の位置で評価します. これらを共通化する場合は離散演算を記述できる macro を使います.

中間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 の boundary x : sbp は差分の境界行を選びます. 物理的な壁条件は例題の更新式や境界項で与え,FormuraのYAML設定で 実行時の境界処理を指定します.

origin r = 1.0 は軸 r の最初の格子点の座標値を指定します(省略時は 0). 座標 r はそのまま物理的な半径や余緯度として使え,1 + r のような ずれた多項式を Egison が展開せずに済むので,計量を成分で宣言する曲線座標の 生成物が小さくなります.sbpLoR などの sbp 境界の定数もこの原点を含みます.

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の各形式で記述できます。

dimension 3
axes x, y, z

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

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

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

座標線が直交しない座標系では、計量を成分で宣言します。

axes θ, ψ                                    -- トーラスのねじった座標 φ = ψ + θ
metric g
metric tensor [[36 + (12 + 6 * cos θ)^2, (12 + 6 * cos θ)^2], [(12 + 6 * cos θ)^2, (12 + 6 * cos θ)^2]]
metric volume 6 * (12 + 6 * cos θ)         -- 省略すると sqrt(det g) をEgisonが作る

metric tensorではEgisonが対称性を検査し、逆計量と体積要素を導きます。このとき使えるのは g~i~j・g_i_j・volumeと∂/∂による計量の解析微分で、直交性を前提とするcanonicalな Δ・δ・hodgeはコンパイル時エラーになります(流束形を明示的に書きます)。 examples/excitable_torus/excitable_torus_twisted.fmeは同じ興奮波のモデルをこの座標で書き、 直交座標の結果と2次精度で一致することをcharts.pyで確認します。

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(軸のrecordは origin 宣言があるときだけ省略可能な start fieldを持つ)
  • scalar/tensor normal formとderivative multi-index付きFieldJet
  • GeometryNF、discretization profile、opaque discrete request
  • 場の各軸のサイズと,空間方向を表す軸の位置 spatial-slots(1から数える)
  • 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が編集対象です。42個の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成分を まとめて宣言する場合は index a : 19 と field f_a を使えます。 lbm_d3q19 では,この添字宣言で分布と衝突・移動の各段階をまとめています。

リポジトリ構成

パス 役割
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します。 誤差曲線、厳密解比較、時空図は検証情報を同時に読める静止図のまま保持します。

検証

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

EGISON_DIR=$(tools/prepare_elastic_validation.sh)
EGISON_HEAP_LIMIT=4G make compiler-tests EGISON_DIR="$EGISON_DIR"
EGISON_HEAP_LIMIT=4G make all EGISON_DIR="$EGISON_DIR"

検証済みの Egison は 87cbb478c845e9760ecfc1d0518b464df10a72cf です。 依存版は spec/egison-revision で管理し、準備スクリプトは .build/egison-<リビジョン> に展開します。隣接する Egison の作業ツリーは変更しません。 EGISON_DIR を省略すると ../egison を使うため、開発中の最新版でも同じ検査を実行できます。 EGISON_HEAP_LIMIT は Egison が管理するメモリの上限を指定します。標準の上限は 4G です。 大きなモデルの出力情報は型付きの小さな定義へ分割し、1G の上限でも正規化できることを検査します。

  • 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
  • html/ja/waves.html/html/en/waves.html: 水面の波と関連する流体モデルの検証
  • APPLICATIONS.md: 応用例一覧
  • UPSTREAM.md: Formura側の過去の拡張案と実装記録

ライセンス

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

About

No description, website, or topics provided.

Resources

Readme
MIT license
Activity
Custom properties

Stars

0 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

Packages

Contributors

Languages

You are visitor 01402520 — GeezerVison does not store the pages you look up.
Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.