A cost-aware logical framework

We present calf , a c ost- a ware l ogical f ramework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of programming languages in terms of a modal account of phase distinctions , we argue that the cost structure of programs motivates a phase distinction between intension and extension . Armed with this technology, we contribute a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input/output behavior cannot depend on cost. As a full-spectrum dependent type theory, calf presents a unified language for programming and specification of both cost and behavior that can be integrated smoothly with existing mathematical libraries available in type theoretic proof assistants. We evaluate calf as a general framework for cost analysis by implementing two fundamental techniques for algorithm analysis: the method of recurrence relations and physicist’s method for amortized analysis . We deploy these techniques on a variety of case studies: we prove a tight, closed bound for Euclid’s algorithm, verify the amortized complexity of batched queues, and derive tight, closed bounds for the sequential and parallel complexity of merge sort, all fully mechanized in the Agda proof assistant. Lastly we substantiate the soundness of quantitative reasoning in calf by means of a model construction.

Decidable linear list constraints

We present new results on a constraint satisfaction problem arising from the inference of resource types in automatic amortized analysis for object-oriented programs by Rodriguez and Hofmann.These constraints are essentially linear inequalities between infinite lists of nonnegative rational numbers which are added and compared pointwise. We study the question of satisfiability of a system of such constraints in two variants with significantly different complexity. We show that in its general form (which is the original formulation presented by Hofmann and Rodriguez at LPAR 2012) this satisfiability problem is hard for the famous Skolem-Mahler-Lech problem whose decidability status is still open but which is at least NP-hard. We then identify a subcase of the problem that still covers all instances arising from type inference in the aforementioned amortized analysis and show decidability of satisfiability in polynomial time by a reduction to linear programming. We further give a classification of the growth rates of satisfiable systems in this format and are now able to draw conclusions about resource bounds for programs that involve lists and also arbitrary data structures if we make the additional restriction that their resource annotations are generated by an infinite list (rather than an infinite tree as in the most general case). Decidability of the tree case which was also part of the original formulation by Hofmann and Rodriguez still remains an open problem.

Reduced space-time and time costs Ising dislocation codes and arbitrary ancillas

We propose two distinct methods of improving quantum computing protocols based on surface codes. First, we analyze the use of dislocations instead of holes to produce logical qubits, potentially reducing spacetime volume required. Dislocations\cite{dis2,dis} induce defects which, in many respects, behave like Majorana quasi-particles. We construct circuits to implement these codes and present fault-tolerant measurement methods for these and other defects which may reduce spatial overhead. One advantage of these codes is that Hadamard gates take exactly $0$ time to implement. We numerically study the performance of these codes using a minimum weight and a greedy decoder using finite-size scaling. Second, we consider state injection of arbitrary ancillas to produce arbitrary rotations. This avoids the logarithmic (in precision) overhead in online cost required if $T$ gates are used to synthesize arbitrary rotations. While this has been considered before\cite{ancilla}, we consider also the parallel performance of this protocol. Arbitrary ancilla injection leads to a probabilistic protocol in which there is a constant chance of success on each round; we use an amortized analysis to show that even in a parallel setting this leads to only a constant factor slowdown as opposed to the logarithmic slowdown that might be expected naively.

Type-based amortized resource analysis with integers and arrays

Proving bounds on the resource consumption of a program by statically analyzing its source code is an important and well-studied problem. Automatic approaches for numeric programs with side effects usually apply abstract interpretation-based invariant generation to derive bounds on loops and recursion depths of function calls. This article presents an alternative approach to resource-bound analysis for numeric and heap-manipulating programs that uses type-based amortized resource analysis. As a first step towards the analysis of imperative code, the technique is developed for a first-order ML-like language with unsigned integers and arrays. The analysis automatically derives bounds that are multivariate polynomials in the numbers and the lengths of the arrays in the input. Experiments with example programs demonstrate two main advantages of amortized analysis over current abstract interpretation–based techniques. For one thing, amortized analysis can handle programs with non-linear intermediate values like f((n + m)2). For another thing, amortized analysis is compositional and works naturally for compound programs like f(g(x)).