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 進行了最佳化，使用箭頭表示關係，如 node(doc.readme) ⟶[owner] node(user.u10)。

ZIL 不僅限於授權，還擴充套件到專案管理。例如，宣告可以 implements 需求，定理可以 validates 元件，模組可以 dependsOn 其他模組。這些關係透過 Datalog 風格的 Horn 規則進行推導。一個經典例子：如果組可以檢視文件，且使用者屬於該組，那麼使用者也可以檢視。在 ZIL 中，這可以表示為一條定理形狀的規則。

在專案中，ZIL 可以儲存解析器、歸一化過程及其驗證定理之間的關係。透過規則，可以推匯出變更影響：當解析器改變時，所有依賴於它的元件都需要審查。ZIL 還支援查詢：哪個宣告實現了某個需求？哪個模組依賴於某個宣告？哪些任務被阻塞？

ZIL 的核心結構包括節點（標識宣告、需求、使用者等）、關係（連線兩個項）、規則（從已有關係推導新關係）和查詢（返回匹配項和變數繫結）。節點使用穩定名稱，如 lean.Parser.parse。快速入門部分介紹瞭如何構建包、執行測試以及逐步示例。

ZIL 的關係模式可以定義源和目標型別，例如 implements : declaration → requirement。型別規則確保變數型別正確。ZIL 將專案事實與原始碼一起儲存，供開發者、審查工具、CI、文件工具和 AI 助手使用。它支援檢查點、變更比較和推理關係解釋，並透過 ZILX/1 和 ZILD/1 格式在不同工具間共享上下文。