Unifying dynamic programming design patterns

Design and Analysis of Computer Algorithms is a must of Computer Curricula. It covers many topics that group around several core themes including algorithmic design patterns (ADP) like the greedy method, divide-and-conquer, dynamic programming, backtracking and branch-and-bound. These design patterns are usually considered as Classics of the Past (going back to days of R. Floyd and E. Dijkstra). However, ADP can be (semi)formalized as design templates, specified by correctness conditions, and formally verified either in the Floyd-Hoare methodology, by means of the Manna-Pnueli proof-principles, or in some other way. This approach has lead to new insights and better comprehension of the design patterns, of specification and verification methods. Formalization of backtracking (BT) and branch-and-bound (B&B) ADP has been presented at TIME-2011 symposium. In the present paper, we suggest and discuss a formalization of Dynamic Programming. A methodological novelty consists in treatment (interpretation) of ascending Dynamic Programming as least fix-point computation (according to the Knaster-Tarski fix-point theorem). This interpretation leads to a uniform approach to classical optimization problems as well as to problems where optimality is not explicit. (Examples of the latter are the Cocke-Younger-Kasami parsing algorithm and computation of inverse for a total function.) This interpretation leads also to an opportunity to design, specify and verify (1) a unified template for imperative Dynamic Programming, (2) a unified template for inverting Dynamic Programming (in countable domains), and may lead to (3) a unified template for data-flow implementation of Dynamic Programming. The present paper is a revised and extended version of the original publication in the Proceedings of the 3rd Workshop on Metacomputation (2012) that focused on inverting Dynamic Programming.