A Lazy, Concurrent Convertibility Checker
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912810499309568 |
|---|---|
| author | Courant, Nathanaëlle Leroy, Xavier |
| author_facet | Courant, Nathanaëlle Leroy, Xavier |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_18418 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Lazy, Concurrent Convertibility Checker Courant, Nathanaëlle Leroy, Xavier Logic in Computer Science Programming Languages 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. |
| title | A Lazy, Concurrent Convertibility Checker |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2510.18418 |