[−][src]Crate term_rewriting
A Rust library for representing, parsing, and computing with firstorder term rewriting systems.
Usage
[dependencies]
term_rewriting = "0.7"
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 s = sig.new_op(0, Some("S".to_string())); let k = sig.new_op(0, Some("K".to_string())); let app = sig.new_op(2, Some(".".to_string())); let constructed_term = Term::Application { op: app.clone(), args: vec![ Term::Application { op: app.clone(), args: vec![ Term::Application { op: app.clone(), args: vec![ Term::Application { op: s.clone(), args: vec![] }, Term::Application { op: k.clone(), args: vec![] }, ] }, Term::Application { op: k.clone(), args: vec![] } ] }, Term::Application { op: app.clone(), args: vec![ Term::Application { op: app.clone(), args: vec![ Term::Application { op: k.clone(), args: vec![] }, Term::Application { op: s.clone(), args: vec![] }, ] }, Term::Application { op: k.clone(), args: vec![] } ] } ] }; // This is the same output the parser produces. assert_eq!(parsed_term, constructed_term);
TRS syntax
Several functions are available which parse TRSrelated data structures according to the following grammar (defined in augmented BackusNaur form):
parse
: aTRS
and list ofTerm
s (program
)parse_trs
: aTRS
(trs
)parse_term
: aTerm
(toplevelterm
)parse_rule
: aRule
(rule
)parse_context
: aContext
(toplevelcontext
)parse_rulecontext
: aRuleContext
(rulecontext
)
program = *wsp *( *comment statement ";" *comment ) *wsp
statement = rule / toplevelterm
rule = toplevelterm *wsp "=" *wsp toplevelterm
rule /= rule *wsp "" *wsp toplevelterm
toplevelterm = term
toplevelterm /= toplevelterm 1*wsp toplevelterm
term = variable
term /= application
term /= "(" *wsp toplevelterm *wsp ")"
rulecontext = toplevelterm *wsp "=" *wsp toplevelterm
rulecontext /= rule *wsp "" *wsp toplevelterm
toplevelcontext = context
toplevelcontext /= toplevelcontext 1*wsp toplevelcontext
context = variable
context /= application
context /= hole
context /= "(" *wsp toplevelcontext *wsp ")"
hole = "[!]"
variable = identifier"_"
application = identifier "(" [ term *( 1*wsp term ) ] ")"
application /= identifier
application /= binaryapplication
; binary application is the '.' operator with arity 2.
binaryapplication = "(" *wsp term *wsp term *wsp ")"
identifier = 1*( ALPHA / DIGIT )
comment = "#" *anycharbutnewline "\n"
wsp = SP / TAB / CR / LF
Term Rewriting Systems
Term Rewriting Systems (TRS) are a simple formalism from theoretical computer science used to model the behavior and evolution of treebased 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 firstorder TRSs
(i.e. no lambdabinding 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.
Modules
trace  Record sequences of rewrites. 
Structs
Operator  A symbol with fixed arity. Only carries meaning alongside a 
Rule  A rewrite rule equating a lefthandside 
RuleContext  
Signature  Records a universe of symbols. 
SignatureChange  Allows 
TRS  A firstorder term rewriting system. 
Variable  A symbol for an unspecified term. Only carries meaning alongside a 
Enums
Atom 

Context  A firstorder 
MergeStrategy  Specifies how to merge two signatures.
See 
ParseError  The error type for parsing operations. 
Strategy  
TRSError  The error type for 
Term  A firstorder term: either a 
Functions
parse  
parse_context  Parse a string as a 
parse_rule  Parse a string as a 
parse_rulecontext  Parse a string as a 
parse_term  Parse a string as a 
parse_trs  Parse a string as a 
Type Definitions
Place  Represents a place in a 