Crate term_rewriting [−] [src]
A Rust library for representing, parsing, and computing with first-order term rewriting systems.
Example
use term_rewriting::{Signature, Term, parse_trs, parse_term}; // 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);
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
- Baader & Nipkow (1999). Term rewriting and all that. Cambridge University Press.
- Bezem, Klop, & de Vrijer (Eds.) (2003). Term Rewriting Systems. Cambridge University Press.
- Rewriting. (2017). Wikipedia.
Structs
Operator |
A symbol with fixed arity. Only carries meaning alongside a |
Rule |
A rewrite rule equating a left-hand-side |
Signature |
Records a universe of symbols. |
SignatureChange |
Allows terms/rules/TRSs to be reified for use with another signature.
See |
TRS |
A first-order term rewriting system. |
Variable |
A symbol for an unspecified term. Only carries meaning alongside a |
Enums
Atom | |
Context | |
MergeStrategy |
Specifies how to merge two signatures.
See |
ParseError | |
Term |
A first-order term: either a |
Functions
parse | |
parse_term | |
parse_trs |
Type Definitions
Place |
Represents a place in a |