Crate term_rewriting [−] [src]

A Rust library for representing and parsing first-order term rewriting systems.

Example

use term_rewriting::types::*;

// A string representation of SK combinatory logic, including:

// a rule for the S combinator,
let s_rule = "S x_ y_ z_ = (x_ z_) (y_ z_);".to_string();

// the rule for the K combinator,
let k_rule = "K x_ y_ = x_;";

// and an arbitrary term,
let term = "S K K (K S K);";

// can be parsed to give back the TRS and a term.
let mut sig = Signature::default();
let (parsed_trs, parsed_term_vec) = sig.parse(&(s_rule + k_rule + term)).expect("successful parse");

// These can also be constructed by hand. Let's look at the term:
let mut sig = Signature::default();
let app = sig.get_op(".", 2);
let s = sig.get_op("S", 0);
let k = sig.get_op("K", 0);

let term = Term::Application {
    head: app.clone(),
    args: vec![
        Term::Application {
            head: app.clone(),
            args: vec![
                Term::Application {
                    head: app.clone(),
                    args: vec![
                        Term::Application { head: s.clone(), args: vec![] },
                        Term::Application { head: k.clone(), args: vec![] },
                    ]
                },
                Term::Application { head: k.clone(), args: vec![] }
            ]
        },
        Term::Application {
            head: app.clone(),
            args: vec![
                Term::Application {
                    head: app.clone(),
                    args: vec![
                        Term::Application { head: k.clone(), args: vec![] },
                        Term::Application { head: s.clone(), args: vec![] },
                    ]
                },
                Term::Application { head: k.clone(), args: vec![] }
            ]
        }
    ]
};

let constructed_term_vec = vec![term];

// This is the same output the parser produces.
assert_eq!(parsed_term_vec, constructed_term_vec);

Term Rewriting Systems

Term Rewriting Systems (TRS) are a simple formalism from theoretical computer science used to model the behavior and evolution of tree-based structures like natural langauge parse trees or abstract syntax trees.

A TRS is defined as a pair (S, R). S is a set of symbols called the signature and together with a disjoint and countably infinite set of variables, defines the set of all possible trees, or terms, which the system can consider. R is a set of rewrite rules. A rewrite rule is an equation, s = t, and is interpreted as follows: any term matching the pattern described by s can be rewritten according to the pattern described by t. Together S and R define a TRS that describes a system of computation, which can be considered as a sort of programming language. term_rewriting provides a way to describe arbitrary first-order TRSs (i.e. no lambda-binding in rules).

Further Reading

Modules

types