Lamcal

lamcal 是一个 Lambda Calculus 解析器和评估器，以及一个独立的命令行 REPL 应用程序，用于交互式地处理 lambda 表达式。所有代码都是用 Rust 编写的。

亮点

• 纯无类型 lambda 演算的实现
• 通过在所有函数中使用 trampolining 而不是递归来支持任意巨大的项
• 功能丰富的 命令行 REPL 应用程序 (独立 crate)

库可以用作

• 将经典符号中的 lambda 表达式解析为项，例如 parse_str("(λx.(λy.x y) a) b")
  或 parse_str("(\\x.(\\y.x y) a) b")
• 使用函数程序化地构造项，例如 lam("x", app(var("x"), var("y")))
• 使用宏 app! 构建函数应用序列，例如：app![var("a"), var("b"), var("c")]，它与app(app(var("a"), var("b")), var("c)) 等价。
• 评估λ项，用环境中变量名绑定的预定义项替换变量。
• 使用不同的策略，如枚举或追加tick符号对项应用α转换。
• 使用不同的策略，如按名调用、按正常顺序或按值调用对项应用β归约。
• 可以通过实现用户特定的α转换和β归约策略进行扩展。

独立的crate lamcal-repl (crate, github-repository ) 提供了命令行REPL（读取-评估-打印循环）应用程序，可以交互式地操作λ项并应用α转换和β归约。

功能

• 提供两种评估函数变体：一个关联函数，例如 Term::reduce，它会原地修改项；以及一个独立的函数，例如 reduce，它会保留原始项不变，并返回一个新项作为结果。
• α转换和β归约策略定义为特质，以轻松实现自定义策略并使用此库的功能。
• 检查系统可以检查项在评估和归约过程中的每个中间状态，并可以根据任意条件停止处理。
• 处理 Term 的递归数据结构的所有函数中都没有递归，以避免在应用于大型项时发生栈溢出错误。相反，所有函数都遵循trampolining模式。
• 解析器提供了有关解析错误的详细信息，例如错误在源流中的位置以及在有效表达式中期望的内容。
• 可选支持与 failure crate 兼容的错误类型。

用法

要将 lamcal 作为库添加到您的项目中，请将以下内容添加到您的 Cargo.toml 文件中

[dependencies]
lamcal = "0.4"

并将其添加到您的crate根目录

extern crate lamcal;

有关库的详细信息，请参阅crates.io上的文档。

此库可选支持 failure crate。对 failure crate 的支持是一个crate功能。要启用它，请将依赖项添加到您的 Cargo.toml，如下所示

[dependencies]
lamcal = { version = "0.4", features = ["failure"] }

许可证

遵循Apache License 2.0许可
详情请参阅 LICENSE 或 https://apache.ac.cn/licenses/LICENSE-2.0.

贡献

除非你明确声明，否则任何根据Apache-2.0许可证定义的、有意提交以包含在工作中的贡献，将按照上述条款许可，不附加任何额外条款或条件。