lambda_calculus

lambda_calculus是在安全的Rust中实现纯λ演算的一个简单、无依赖版本。

特性

• λ表达式的解析器，包括经典和De Bruijn索引记法
• 7种β-归约策略
• 一组标准项（组合子）
• λ编码的布尔、对、元组、选项和结果数据类型
• 单对编码的列表
• Church-、Scott-和Parigot编码的数字和列表
• Stump-Fu（嵌入迭代器）-和二进制编码的数字
• 有符号数字

安装

在Cargo.toml中添加以下内容以包含库

[dependencies]
lambda_calculus = "3"

编译特性

• backslash_lambda：将λ的显示从λ改为\
• encoding：构建数据编码模块；默认特性

Cargo.toml中的示例特性设置

[dependencies.lambda_calculus]
version = "3"
default-features = false # do not build the data encoding modules
features = ["backslash_lambda"] # use a backslash lambda

示例

比较经典和De Bruijn索引记法

代码

use lambda_calculus::data::num::church::{succ, pred};

fn main() {
    println!("SUCC := {0} = {0:?}", succ());
    println!("PRED := {0} = {0:?}", pred());
}

标准输出

SUCC := λa.λb.λc.b (a b c) = λλλ2(321)
PRED := λa.λb.λc.a (λd.λe.e (d b)) (λd.c) (λd.d) = λλλ3(λλ1(24))(λ2)(λ1)

解析λ表达式

代码

use lambda_calculus::*;

fn main() {
    assert_eq!(
        parse(&"λa.λb.λc.b (a b c)", Classic),
        parse(&"λλλ2(321)", DeBruijn)
    );
}

显示β-归约步骤

代码

use lambda_calculus::*;
use lambda_calculus::data::num::church::pred;

fn main() {
    let mut expr = app!(pred(), 1.into_church());

    println!("{} order β-reduction steps for PRED 1 are:", NOR);

    println!("{}", expr);
    while expr.reduce(NOR, 1) != 0 {
        println!("{}", expr);
    }
}

标准输出

normal order β-reduction steps for PRED 1 are:
(λa.λb.λc.a (λd.λe.e (d b)) (λd.c) (λd.d)) (λa.λb.a b)
λa.λb.(λc.λd.c d) (λc.λd.d (c a)) (λc.b) (λc.c)
λa.λb.(λc.(λd.λe.e (d a)) c) (λc.b) (λc.c)
λa.λb.(λc.λd.d (c a)) (λc.b) (λc.c)
λa.λb.(λc.c ((λd.b) a)) (λc.c)
λa.λb.(λc.c) ((λc.b) a)
λa.λb.(λc.b) a
λa.λb.b

比较不同归约策略的步骤数量

代码

use lambda_calculus::*;
use lambda_calculus::data::num::church::fac;

fn main() {
    let expr = app(fac(), 3.into_church());

    println!("comparing normalizing orders' reduction step count for FAC 3:");
    for &order in [NOR, APP, HNO, HAP].iter() {
        println!("{}: {}", order, expr.clone().reduce(order, 0));
    }
}

标准输出

comparing normalizing orders' reduction step count for FAC 3:
normal: 46
applicative: 39
hybrid normal: 46
hybrid applicative: 39

比较不同的数字编码

代码

use lambda_calculus::*;

fn main() {
    println!("comparing different encodings of number 3 (De Bruijn indices):");
    println!("  Church encoding: {:?}", 3.into_church());
    println!("   Scott encoding: {:?}", 3.into_scott());
    println!(" Parigot encoding: {:?}", 3.into_parigot());
    println!("Stump-Fu encoding: {:?}", 3.into_stumpfu());
    println!("  binary encoding: {:?}", 3.into_binary());
}

标准输出

comparing different encodings of number 3 (De Bruijn indices):
  Church encoding: λλ2(2(21))
   Scott encoding: λλ1(λλ1(λλ1(λλ2)))
 Parigot encoding: λλ2(λλ2(λλ2(λλ1)1)(2(λλ1)1))(2(λλ2(λλ1)1)(2(λλ1)1))
Stump-Fu encoding: λλ2(λλ2(2(21)))(λλ2(λλ2(21))(λλ2(λλ21)(λλ1)))
  binary encoding: λλλ1(13)