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.

翻译：自然语言处理领域的许多算法研究旨在高效处理丰富的形式化结构。算法设计者通常希望为其提出的算法提供性能保证——例如，其运行时间或空间复杂度存在基于输入规模的特定上界函数。他们可能还希望确定算法所推导量的必要性质，以合成高效数据结构并验证类型错误。本文开发了一个辅助程序员执行此类分析的系统。我们将该系统应用于多个自然语言处理算法，发现其能成功推断类型、无效及冗余代码，以及参数化的运行时与空间复杂度边界。