SHF: Small: Collaborative research:Complexity and feasibility for programs over coinductively-defined data

Syracuse University, Syracuse NY

Investigators

Abstract

The typical tools of complexity theory and algorithms tend to be biased toward low-level models of computation that refer directly to bit-level representations of data. But when programming in the large, there are layers upon layers of abstraction over any low-level details, and a key feature of modern programming is the ability to compose different abstractions without regard to such details. Compositionality has yielded very reliable software development methodologies, in large part because the tools developed for reasoning about program correctness have developed alongside these notions of abstraction. However, tools for reasoning about complexity have not kept pace. The big picture of the principle investigators' research program is to develop techniques for compositional reasoning about complexity, thereby allowing for reasoning about run-time cost in all its facets of large-scale programming with methods similar to those so successfully deployed for reasoning about correctness. The research project funded by this grant concentrates on characterizing sensible notions of feasibility for programs that use coninductively-defined data such as streams (a program that produces or processes streaming media is just the right model to have in mind) and more generally quantifying, in a machine-checkable manner, resource usage for such programs. Although feasibility has been well-studied in the context of finite structures, extensions to potentially infinite data structures such as streams have been somewhat piecemeal. One facet of this research project is to develop principled notions of feasibility in this setting. To do so, the PIs will extend tools such as logic and programming language formalisms that have previously been used to give resource-free characterizations of complexity classes for finite structures. Such tools are already more closely tied to a compositional view of programming, and they give a jumping-off point for analyzing notions of cost in domains where the very definition of resource usage may not be so obvious. One such tool that they developed in previous work is a framework for compositional cost analysis of higher-order programs. This time-complexity semantics is essentially a translation of target-language programs into a domain of complexities, which encode information about evaluation and usage cost. The translation can be automated, and so this framework not only provides a tool for reasoning compositionally about cost, but provides machine-checkable assertions about the cost of target programs.