Finding equations in functional programs
Johannes Bader · 2014
This thesis describes an algorithm finding and proving equations suitable to be used as rewrite rules, which have the potential to simplify a functional program. To be independent from any specific functional programming language, a dialect of λ-calculus is introduced. It covers common features of such languages, including recursion, pattern matching and case-expressions. The main focus of this work lies on putting expressions of this language in a partial order. Finally, a concrete strategy for finding rewrite rules using this partial order is specified.