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 格式在不同工具間共享上下文。