对称编程与推理的数学基础
Mathematical foundations for symmetric programming and reasoning
Ohad Kammar, Matija Pretnar
AI 速读 基于摘要
该文基于数学中“不失一般性”（w.l.o.g.）的证明原则，提出一种统一利用对称性的数学抽象，用于编程与推理。
cs.PL · cs.LO · math.CT · math.GR · math.LO
查看原文摘要
We develop a mathematical abstraction for uniformly exploiting symmetries in programming and reasoning based on the mathematical proof principle `without-loss-of-generality' (w.l.o.g.). Given: group actions that describe symmetries of the input and the output; and a canoniser, which captures how arbitrary inputs get sent to canonical ones, our construction extends any function from the canonical inputs to the whole domain. We characterise the conditions on the canonisers which guarantee that the construction gives the unique equivariant (i.e. symmetry-preserving) extension. Furthermore, we adapt the construction to a dependently-typed setting, where it captures traditional symmetric w.l.o.g. arguments via the Curry-Howard correspondence. Finally, we extend the construction to algebraic data types, where the symmetries of the constructors both uniquely determine the symmetries of the data type and pave the way for efficient execution.