Hostname: page-component-7c8c6479df-94d59 Total loading time: 0 Render date: 2024-03-28T21:13:11.451Z Has data issue: false hasContentIssue false

Automated complexity analysis of Nuprl extracted programs

Published online by Cambridge University Press:  26 March 2001

RALPH BENZINGER
Affiliation:
Department of Computer Science, Cornell University, Ithaca, NY 14853, USA; (e-mail: ralph@cs.cornell.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

This paper describes the Automated Complexity Analysis Prototype (ACAp) system for automated complexity analysis of functional programs synthesized with the Nuprl proof development system. We define a simple abstract cost model for NUPRL's term language based on the current call-by-name evaluator. The framework uses abstract functions and abstract lists to facilitate reasoning about primitive recursive programs with first-order functions, lazy lists and a subclass of higher-order functions. The ACAp system automatically derives upper bounds on the time complexity of NUPRL extracts relative to a given profiling semantics. Analysis proceeds by abstract interpretation of the extract, where symbolic evaluation rules extend standard evaluation to terms with free variables. Symbolic evaluation of recursive programs generates systems of multi-variable difference equations, which are solved using the MATHEMATICA computer algebra system. The use of the system is exemplified by analyzing a proof extract that computes the maximum segment sum of a list and a functional program that determines the minimum of a list via sorting. For both results, we compare call-by-name to call-by-value evaluation.

Type
Research Article
Copyright
© 2001 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.