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