Improving Memory Consumption with FAITH - a Proof Assistant for Improvement Theory

Abstract

In functional languages with lazy evaluation and sharing, such as Haskell, it is hard to reason about space usage. In particular, it is hard to know if a given local transformation in such a language will introduce an asymptotic space increase. Gustavsson and Sands have developed Space Improvement Theory to prove if such transformations introduced asymptotic space increase. However, since the proofs are long and complicated, Space Improvement proofs done on paper are prone to errors. To tackle this problem, I have constructed FAITH, the proof assistant for Improvement Theory. FAITH allows users to define transformational laws, such as those for Space Improvement, and then use those laws in proofs that transform one term to another step by step. In case of errors, FAITH provides helpful error messages. The main contributions of FAITH is to check proofs of inequational reasoning with custom transformational laws that can be applied inside arbitrary contexts. Keywords: