Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Lazy, Concurrent Convertibility Checker

Nathanaëlle Courant, Xavier Leroy

TL;DR

The paper tackles the problem of converting lambda-terms efficiently by introducing a lazy, concurrent convertibility checker. It combines non-strict evaluation, sharing, and explicit scheduling within a process-calculus-based framework to explore multiple convertibility proofs in parallel, ensuring the simplest proof is found if one exists. A Krivine-like WHNF evaluator, normalization-by-evaluation techniques, and a globally shared constant environment underpin the core reduction semantics, while a formally verified Rocq proof establishes partial correctness of the approach. Experimental results and a detailed abstract-machine design demonstrate practical feasibility and highlight performance benefits over heuristic, sequential checkers while acknowledging potential exponential worst-case behavior. The work offers a principled, verifiable alternative to heuristic convertibility checking with potential impact on proof assistants and dependently-typed languages.

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.

A Lazy, Concurrent Convertibility Checker

TL;DR

The paper tackles the problem of converting lambda-terms efficiently by introducing a lazy, concurrent convertibility checker. It combines non-strict evaluation, sharing, and explicit scheduling within a process-calculus-based framework to explore multiple convertibility proofs in parallel, ensuring the simplest proof is found if one exists. A Krivine-like WHNF evaluator, normalization-by-evaluation techniques, and a globally shared constant environment underpin the core reduction semantics, while a formally verified Rocq proof establishes partial correctness of the approach. Experimental results and a detailed abstract-machine design demonstrate practical feasibility and highlight performance benefits over heuristic, sequential checkers while acknowledging potential exponential worst-case behavior. The work offers a principled, verifiable alternative to heuristic convertibility checking with potential impact on proof assistants and dependently-typed languages.

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.
Paper Structure (25 sections, 67 equations, 5 figures)

This paper contains 25 sections, 67 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Intuitions on convertibility checking
  3. Expressing laziness with a process calculus
  4. Strong call-by-need reduction
  5. The source language
  6. Reduction to weak head normal form
  7. Reduction under lambdas and normalization
  8. Defined constants
  9. Convertibility testing
  10. The basic algorithm
  11. Handling defined constants
  12. Extensions
  13. Avoiding redundant unfolding of constants
  14. Handling $\eta$-conversion
  15. Sharing convertibility processes
  16. ...and 10 more sections

Figures (5)

  • Figure 1: The simple process calculus used as a metalanguage in this article.
  • Figure 2: The explicitly-scheduled abstract machine, part 1.
  • Figure 3: The explicitly-scheduled abstract machine, part 2.
  • Figure 4: The inference rules for the convertibility judgment $t \approx u : B$
  • Figure 5: Timings, in seconds, for the examples of convertibility problems given in the text for Rocq and our two OCaml implementations, Simple and Full. Speedups are relative to Rocq and are expressed as base-10 logarithms, i.e. decimal orders of magnitude. Higher is faster. See the main text for the description of the test cases and the explanation of the two results given for the last test.