Show HN: Google Zanzibar に基づく Lean4 Datalog DSL - AI プロジェクト向け

ZIL は Lean 4 で動作する小さなリレーショナル言語で、名前付きオブジェクトとその間の関係、および関係から追加の関係を導出するルールを記述します。その関係モデルは Google Zanzibar の論文で説明されたタプルモデルに影響を受けています。Zanzibar では、認可タプルを object#relation@user と表現し、例えば doc:readme#owner@user:10 はユーザー10がドキュメント readme の所有者であることを示します。ZIL も同様の構文を使用しますが、Lean 4 のネイティブ構文では矢印を使ってノード間の関係を表現します。

ZIL は認可だけでなく、プロジェクト関係管理にも拡張されます。例えば、宣言は要件を implements、定理はコンポーネントを validates、モジュールは別のモジュールに dependsOn などです。Datalog スタイルの Horn ルールを使用して新しい関係を導出します。例えば、グループがドキュメントを閲覧でき、ユーザーがそのグループに属している場合、そのユーザーもドキュメントを閲覧できます。ZIL ではこれを定理形状のルールとして表現できます。

プロジェクト例では、パーサー、正規化処理、および正規化の妥当性を証明する定理の関係を保存できます。ルールを通じて変更影響を導出でき、例えばパーサーが変更された場合、それに依存するすべてのコンポーネントをレビューする必要があります。ZIL はクエリもサポートし、どの宣言が特定の要件を実装しているか、どのモジュールがどの宣言に依存しているか、どのタスクがブロックされているかなどを質問できます。

ZIL のコア構造はノード（宣言、要件、ユーザーなどを識別）、関係（2つの項を接続）、ルール（既存の関係から関係を導出）、クエリ（マッチする項と変数バインディングを返す）の4つです。ノードは lean.Parser.parse のような安定した名前を使用します。クイックスタートでは、パッケージのビルド、テストの実行、段階的な例の実行方法を紹介しています。

ZIL のリレーションスキーマはソースとターゲットの型を定義でき、例えば implements : declaration → requirement です。型付きルールにより変数の型を保証できます。ZIL はプロジェクトの事実をソースコードとともに保存し、開発者、レビューツール、CI、ドキュメントツール、AI アシスタントが同じマップを利用できます。チェックポイント、変更比較、推論関係の説明をサポートし、ZILX/1 および ZILD/1 フォーマットで異なるツール間でコンテキストを共有できます。