A Lazy, Concurrent Convertibility Checker

TL;DR

This paper introduces a novel convertibility-checking algorithm for lambda-terms that leverages laziness and concurrency to efficiently determine equivalence, avoiding the pitfalls of heuristic methods.

Contribution

It presents a new algorithm combining laziness and concurrency for convertibility checking, with formal proof and experimental evaluation.

Findings

Algorithm always finds an easy solution if one exists.

Mechanized proof of partial correctness provided.

Lightweight experimental evaluation conducted.

Abstract

Convertibility checking - determining whether two lambda-terms are equal up to reductions - is a crucial component of proof assistants and dependently-typed languages. Practical implementations often use heuristics to quickly conclude that two terms are or are not convertible without reducing them to normal form. However, these heuristics can backfire, triggering huge amounts of unnecessary computation. This paper presents a novel convertibility-checking algorithm that relies crucially on laziness and concurrency} Laziness is used to share computations, while concurrency is used to explore multiple convertibility subproblems in parallel or via fair interleaving. Unlike heuristics-based approaches, our algorithm always finds an easy solution to the convertibility problem, if one exists. The paper presents the algorithm in process calculus style and discusses its mechanized proof of partial correctness, its complexity, and its lightweight experimental evaluation.