Crate term_rewriting

Expand description

A Rust library for representing, parsing, and computing with first-order 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 TRS-related data structures according to the following grammar (defined in augmented Backus-Naur form):

parse: a TRS and list of Terms (program)
parse_trs: a TRS (trs)
parse_term: a Term (top-level-term)
parse_rule: a Rule (rule)
parse_context: a Context (top-level-context)
parse_rulecontext: a RuleContext (rulecontext)

program = *wsp *( *comment statement ";" *comment ) *wsp

statement = rule / top-level-term

rule = top-level-term *wsp "=" *wsp top-level-term
rule /= rule *wsp "|" *wsp top-level-term

top-level-term = term
top-level-term /= top-level-term 1*wsp top-level-term

term = variable
term /= application
term /= "(" *wsp top-level-term *wsp ")"

rulecontext = top-level-term *wsp "=" *wsp top-level-term
rulecontext /= rule *wsp "|" *wsp top-level-term

top-level-context = context
top-level-context /= top-level-context 1*wsp top-level-context

context = variable
context /= application
context /= hole
context /= "(" *wsp top-level-context *wsp ")"

hole = "[!]"

variable = identifier"_"

application = identifier "(" [ term *( 1*wsp term ) ] ")"
application /= identifier
application /= binary-application

; binary application is the '.' operator with arity 2.
binary-application = "(" *wsp term *wsp term *wsp ")"

identifier = 1*( ALPHA / DIGIT )

comment = "#" *any-char-but-newline "\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 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.

Modules§

trace: Record sequences of rewrites.

Structs§

Operator: A symbol with fixed arity. Only carries meaning alongside a Signature.
Rule: A rewrite rule equating a left-hand-side Term with one or more right-hand-side Terms.
RuleContext: A Rule with Holes; a sort of Rule template.
Signature: Records a universe of symbols.
SignatureChange: Allows Terms/Rules/TRSs to be reified for use with another Signature. See Signature::merge.
TRS: A first-order term rewriting system.
Variable: A symbol for an unspecified term. Only carries meaning alongside a Signature.

Enums§

Atom: Atoms are the parts of a TRS that are not constructed from smaller parts: Variables and Operators.
Context: A first-order Context: a Term that may have Holes; a sort of Term template.
MergeStrategy: Specifies how to merge two signatures. See Signature::merge.
ParseError: The error type for parsing operations.
Strategy
TRSError: The error type for TRS manipulations.
Term: A first-order term: either a Variable or an application of an Operator.

Functions§

parse: Parse a string as a TRS and a list of Terms.
parse_context: Parse a string as a Context.
parse_rule: Parse a string as a Rule.
parse_rulecontext: Parse a string as a RuleContext.
parse_term: Parse a string as a Term.
parse_trs: Parse a string as a TRS.

Type Aliases§

Place: Represents a place in a Term.

Crate term_rewritingCopy item path