使用Bindlib库在OCaml中抽象表示绑定器
Abstract Representation of Binders in OCaml using the Bindlib Library
摘要：
OCaml的Bindlib库提供了一组工具，用于通过变量绑定操作数据结构。它非常适合抽象语法树的表示，并且已经被用于六种语言和证明助手（包括逻辑框架Dedukti的新版本）的实现。Bindlib针对快速替换进行了优化，并支持变量重命名。由于绑定的表示是基于高阶抽象语法的，因此在替换过程中不会发生变量捕获。因此，变量名在替换时不会更新。然而，它们可以被显式地重新计算以避免“视觉捕获”（即，具有相同外观名称的不同变量）。
英文摘要：
The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract syntax trees, and has already been used for the implementation of half a dozen languages and proof assistants (including a new version of the logical framework Dedukti). Bindlib is optimised for fast substitution, and it supports variable renaming. Since the representation of binders is based on higher-order abstract syntax, variable capture cannot arise during substitution. As a consequence, variable names are not updated at substitution time. They can however be explicitly recomputed to avoid "visual capture" (i.e., distinct variables with the same apparent name) when a data structure is displayed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
