# 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 |