term-rewriting-rs

一个用于表示、解析和计算一阶 术语重写系统 的 Rust 库。

用法

作为依赖项包含

[dependencies]
term_rewriting = "0.7"

实际使用库

extern crate term_rewriting;
use term_rewriting::{Signature, Term, parse_trs, parse_term};

fn main() {
    // We can parse a string representation of SK combinatory logic,
    let mut sig = Signature::default();
    let sk_rules = "S x_ y_ z_ = (x_ z_) (y_ z_); K x_ y_ = x_;";
    let trs = parse_trs(&mut sig, sk_rules).expect("parsed TRS");

    // and we can also parse an arbitrary term.
    let mut sig = Signature::default();
    let term = "S K K (K S K)";
    let parsed_term = parse_term(&mut sig, term).expect("parsed term");

    // These can also be constructed by hand.
    let mut sig = Signature::default();
    let app = sig.new_op(2, Some(".".to_string()));
    let s = sig.new_op(0, Some("S".to_string()));
    let k = sig.new_op(0, Some("K".to_string()));

    let constructed_term = Term::Application {
        op: app,
        args: vec![
            Term::Application {
                op: app,
                args: vec![
                    Term::Application {
                        op: app,
                        args: vec![
                            Term::Application { op: s, args: vec![] },
                            Term::Application { op: k, args: vec![] },
                        ]
                    },
                    Term::Application { op: k, args: vec![] }
                ]
            },
            Term::Application {
                op: app,
                args: vec![
                    Term::Application {
                        op: app,
                        args: vec![
                            Term::Application { op: k, args: vec![] },
                            Term::Application { op: s, args: vec![] },
                        ]
                    },
                    Term::Application { op: k, args: vec![] }
                ]
            }
        ]
    };

    // This is the same output the parser produces.
    assert_eq!(parsed_term, constructed_term);
}

术语重写系统

术语重写系统（TRS）是理论计算机科学中的一个简单形式化方法，用于模拟基于树的结构（如自然语言解析树或抽象语法树）的行为和演变。

一个 TRS 被定义为对 (S, R)。 S 是一个称为签名的符号集合，与一个不相交的且可数的无限集合的变量一起，定义了系统可以考虑的所有可能的树，或术语。 R 是一组重写规则。一个重写规则是一个方程 s = t，其解释如下：任何匹配由 s 描述的模式的术语都可以根据由 t 描述的模式进行重写。 S 和 R 一起定义了一个 TRS，它描述了一个计算系统，可以被视为一种编程语言。term-rewriting-rs 提供了一种描述任意一阶 TRS（即规则中没有 λ 绑定）的方法。

进一步阅读

• Baader & Nipkow (1999). 术语重写与所有. 剑桥大学出版社。
• Bezem, Klop, & de Vrijer (编者) (2003). 术语重写系统. 剑桥大学出版社。
• 重写. (2017). Wikipedia。