Sealing Pointer-Based Optimizations Behind Pure Functions
Daniel Selsam, Simon Hudon, Leonardo de Moura
cs.PL
Mar 3, 2020 · v2
TL;DR
Implemented pointer-based optimizations in Lean 4's runtime using dependent types for referential transparency.
Abstract
Functional programming languages are particularly well-suited for building automated reasoning systems because logical terms can be represented directly as inductive types, term traversal can make use of higher-order combinators, and persistent datastructures enable backtracking cheaply. However, traversing a term requires time proportional to the tree size of the term as opposed to its graph size. This is a significant problem for theorem provers such as Lean and Coq, where the exponential blowup of term-tree sizes has proved to be both common and difficult to prevent. We show how to use dependent types to seal the necessary pointer-address manipulations behind pure functional interfaces with only a negligible amount of additional trust. The approach was implemented for Lean v4 and could be adopted by other dependently-typed languages.
Problem
Theorem provers like Lean and Coq suffer from exponential blowup of term-tree sizes during traversal, since traversing a term requires time proportional to tree size rather than graph size. This is both common and difficult to prevent in practice.
Approach
The paper shows how to use dependent types to seal pointer-address manipulations behind pure functional interfaces, requiring only a negligible amount of additional trust. The key idea is that pointer-based optimizations (sharing, hash-consing) are hidden behind interfaces that maintain the pure functional semantics expected by the type system.
Results
The approach was implemented for Lean v4 and enables graph-size term traversal while maintaining pure functional guarantees. The technique could be adopted by other dependently-typed languages facing the same exponential blowup problem.
