管道指称设计：零成本的构造正确性数据管道
Pipeline Denotational Design: Correct-by-Construction Data Pipelines at Zero Cost
AI总结：
提出管道指称设计（PDD）方法论，在设计时零成本实现数据管道构造正确性，可验证 AI 生成管道的粒度一致性，已在生产工具链中实现并评估。
AI中文摘要：
管道指称设计（Pipeline Denotational Design, PDD）是一种以设计为核心的方法论，用于构建构造正确性的数据管道。随着智能体大规模生成管道代码，瓶颈从编写转向管道验证，而最关键的错误——会悄悄放大聚合结果的粒度不一致——无法被模式检查、类型检查和抽样测试检测到。PDD 在语义域而非代码中设计管道：设计由类型化操作代数（即管道设计代数，一种实例）构成，其中每个良类型组合在构造上就是粒度正确的。仅基于粒度，该保证具有普适性：它适用于任何粒度推断操作集，且适用于任何引擎。正确性在设计时以零成本在三层（粒度、行为类和域）确立，无需访问数据：粒度通过与数据无关的计算（CalcG）确定，行为类通过类型检查器确定，域规则通过基于操作契约的携带证明组合确定。管道正确性定理将其余部分简化为单一输入边界检查：唯一依赖数据的残留部分是输入是否满足设计的前置条件（数据质量，而非代码正确性），PDD 将其生成为 SQL/PySpark 验证查询。构造正确性是一个谱系：同一设计可通过运行时检查、部署的类型级检查器或 Agda/Lean 4 中的机器检查证明进行验证。这重塑了工程师的角色：智能体实例化预验证模式并交付机器可检查的证书；人类验证紧凑规范并进行检查。我们在生产工具链中实现了该方法论，并针对管道模式、行为类和数据建模范式开展了评估。由于仅基于粒度，相同的设计时检查可扩展到语义层和本体上的智能体生成查询。
英文摘要：
Pipeline Denotational Design (PDD) is a design-first methodology for building data pipelines that are correct by construction. As AI agents generate pipeline code at scale, the bottleneck shifts from writing to verifying pipelines, and the errors that matter most (grain inconsistencies that silently inflate aggregates) evade schema checks, type checks, and sampled tests. PDD designs pipelines in a semantic domain rather than in code: a design is composed from a typed algebra of operations (the Pipeline Design Algebra, one instantiation) in which every well-typed composition is grain-correct by construction. Resting on grain alone, the guarantee is universal: it holds for any grain-inferring operation set, over any engine. Correctness is established in three layers (grain, behavioral class, and domain) at design time, at zero cost, with no access to data: grain by a data-independent computation (CalcG), behavioral class by the type checker, and domain rules by a proof-carrying composition over operation contracts. A Pipeline Correctness theorem collapses the rest to a single input-boundary check: the only data-dependent residue is whether inputs meet the design's preconditions (data quality, not code correctness), which PDD emits as SQL/PySpark verification queries. Correctness by construction is a spectrum: the same design can be verified by runtime checks, the deployed type-level checker, or machine-checked proofs in Agda/Lean 4. This recasts the engineer's role: an agent instantiates a pre-verified pattern and ships a machine-checkable certificate; the human validates a compact specification and checks it. We realize the methodology in a production toolchain and set out an evaluation across pipeline patterns, behavioral classes, and data modelling paradigms. Because it rests on grain alone, the same design-time check extends to AI-generated queries over semantic layers and ontologies.
