Automating the Analysis of Parsing Algorithms (and other Dynamic Programs)

TL;DR

This paper introduces a system that automates the analysis of parsing algorithms and other dynamic programs in NLP, providing guarantees on complexity, type correctness, and code efficiency.

Contribution

It presents a novel system that automatically infers types, detects dead and redundant code, and estimates runtime and space bounds for NLP algorithms.

Findings

Successfully infers types and detects dead code

Determines parametric runtime and space complexity bounds

Applies to various NLP algorithms

Abstract

Much algorithmic research in NLP aims to efficiently manipulate rich formal structures. An algorithm designer typically seeks to provide guarantees about their proposed algorithm -- for example, that its running time or space complexity is upper-bounded as a certain function of its input size. They may also wish to determine the necessary properties of the quantities derived by the algorithm to synthesize efficient data structures and verify type errors. In this paper, we develop a system for helping programmers to perform these types of analyses. We apply our system to a number of NLP algorithms and find that it successfully infers types, dead and redundant code, and parametric runtime and space complexity bounds.