Dynamic programming (DP) is an algorithmic design paradigm for the efficient, exact solution of otherwise intractable, combinatorial problems. However, DP algorithm design is often presented in an ad-hoc manner. It is sometimes difficult to justify algorithm correctness. To address this issue, this paper presents a rigorous algebraic formalism for systematically deriving DP algorithms, based on semiring polymorphism. We start with a specification, construct an algorithm to compute the required solution which is self-evidently correct because it exhaustively generates and evaluates all possible solutions meeting the specification. We then derive, through the use of shortcut fusion, an implementation of this algorithm which is both efficient and correct. We also demonstrate how, with the use of semiring lifting, the specification can be augmented with combinatorial constraints, showing how these constraints can be fused with the algorithm. We furthermore demonstrate how existing DP algorithms for a given combinatorial problem can be abstracted from their original context and re-purposed. This approach can be applied to the full scope of combinatorial problems expressible in terms of semirings. This includes, for example: optimal probability and Viterbi decoding, probabilistic marginalization, logical inference, fuzzy sets, differentiable softmax, relational and provenance queries. The approach, building on ideas from the existing literature on constructive algorithmics, exploits generic properties of polymorphic functions, tupling and formal sums and algebraic simplifications arising from constraint algebras. We demonstrate the effectiveness of this formalism for some example applications arising in signal processing, bioinformatics and reliability engineering. Python software implementing these algorithms can be downloaded from: http://www.maxlittle.net/software/dppolyalg.zip.

翻译：动态规划（DP）是一种算法设计范式，用于高效精确求解原本难以处理的组合问题。然而，DP算法设计常常以特定方式呈现，有时难以证明算法正确性。为解决此问题，本文提出一种基于半环多态性的严格代数形式体系，用于系统化推导DP算法。我们从规范出发，构造一个自明正确的算法来计算所需解，因为它穷举生成并评估所有满足规范的可行解。随后，通过使用快捷融合技术，推导出该算法既高效又正确的实现。我们还展示了如何利用半环提升，在规范中增加组合约束，并演示这些约束如何与算法融合。此外，我们证明给定组合问题的现有DP算法可脱离原始上下文进行抽象并重新利用。该方法可应用于所有能用半环表达的组合问题，包括：最优概率与维特比解码、概率边缘化、逻辑推理、模糊集、可微softmax、关系查询与溯源查询。该方法基于现有构造算法学文献的思想，利用了多态函数的泛化性质、元组化、形式求和以及约束代数产生的代数简化。我们通过信号处理、生物信息学和可靠性工程中的示例应用证明了该形式体系的有效性。实现这些算法的Python软件可下载自：http://www.maxlittle.net/software/dppolyalg.zip。