Enum term_rewriting::Term

pub enum Term {
    Variable(Variable),
    Application {
        op: Operator,
        args: Vec<Term>,
    },
}

A first-order term: either a Variable or an application of an Operator.

Variants

Variable(Variable)

A concrete but unspecified Term (e.g. x, y). See Variable for more information.

Examples

let mut sig = Signature::default();

// Constructing a Variable manually
let var = sig.new_var(Some("x_".to_string()));
let var_term = Term::Variable(var);

// Constructing a Variable using the parser
let var = parse_term(&mut sig, "x_");

Application

An Operator applied to zero or more Terms (e.g. (f(x, y), g()).

A Term that is an application of an Operator with arity 0 applied to 0 Terms can be considered a constant.

Examples

let mut sig = Signature::default();

// Constructing a Constant manually
let a = sig.new_op(0, Some("A".to_string()));
let const_term = Term::Application {
    op: a,
     args: vec![],
};

// Constructing a Constant using the parser
let const_term = parse_term(&mut sig, "A");

// Constructing an Application manually
let x = sig.new_var(Some("x_".to_string()));
let b = sig.new_op(1, Some("B".to_string()));
let op_term = Term::Application {
    op: b,
    args: vec![Term::Variable(x)],
};

// Constructing an Application using the parser
let op_term = parse_term(&mut sig, "B(x_)");

Fields of Application

op: Operatorargs: Vec<Term>

Methods

impl Term

pub fn display(&self) -> String

Serialize a Term.

Examples

let mut sig = Signature::default();

let term = parse_term(&mut sig, "A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)")
    .expect("parse of A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)");

assert_eq!(term.display(), ".(.(.(A B(x_)) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL)))) DECC(DECC(DIGIT(1) 0) 5))");

pub fn pretty(&self) -> String

A human-readable serialization of the Term.

Examples

let mut sig = Signature::default();

let term = parse_term(&mut sig, "A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)")
    .expect("parse of A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)");

assert_eq!(term.pretty(), "A B(x_) [2, 1, 0] 105");

pub fn atoms(&self) -> Vec<Atom>

Every Atom used in the Term.

Examples

let mut sig = Signature::default();

let example_term = parse_term(&mut sig, "A(B x_)").expect("parse of A(B x_)");
let atoms: Vec<String> = example_term.atoms().iter().map(|a| a.display()).collect();

assert_eq!(atoms, vec!["x_", "B", "A"]);

pub fn variables(&self) -> Vec<Variable>

Every Variable used in the Term.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "A B y_ z_").expect("parse of A B y_ z_");
let var_names: Vec<String> = t.variables().iter().map(|v| v.display()).collect();

assert_eq!(var_names, vec!["y_", "z_"]);

pub fn operators(&self) -> Vec<Operator>

Every Operator used in the Term.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "A B y_ z_").expect("parse of A B y_ z_");
let op_names: Vec<String> = t.operators().iter().map(|v| v.display()).collect();

assert_eq!(op_names, vec!["A", "B", "."]);

pub fn head(&self) -> Atom

The head of the Term.

Examples

let mut sig = Signature::default();

let op = sig.new_op(2, Some("A".to_string()));
let t = parse_term(&mut sig, "A(B z_)").expect("parse of A(B z_)");

assert_eq!(t.atoms().len(), 3);
assert_eq!(t.head(), Atom::Operator(op));

pub fn args(&self) -> Vec<Term>

The arguments of the Term.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "C(A B)").expect("parse of C(A B)");
let arg0 = parse_term(&mut sig, "A").expect("parse of A");
let arg1 = parse_term(&mut sig, "B").expect("parse of B");

assert_eq!(t.args(), vec![arg0, arg1]);

let t2 = parse_term(&mut sig, "A").expect("parse of A");

assert_eq!(t2.args(), vec![]);

pub fn subterms(&self) -> Vec<(&Term, Place)>

Every subterm and its Place, starting with the Term and the empty Place.

Examples

let mut sig = Signature::default();

let b = sig.new_op(0, Some("B".to_string()));
let a = sig.new_op(1, Some("A".to_string()));

let p: Vec<usize> = vec![];
let p1: Vec<usize> = vec![0];
let t = parse_term(&mut sig, "A(B)").expect("parse of A(B)");
let subterm0 = Term::Application {
    op: a.clone(),
    args: vec![Term::Application {
        op: b.clone(),
        args: vec![],
    }],
};
let subterm1 = Term::Application {
    op: b.clone(),
    args: vec![],
};

assert_eq!(t.subterms(), vec![(&subterm0, p), (&subterm1, p1)]);

pub fn size(&self) -> usize

The number of distinct Places in the Term.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "A B").expect("parse of A B");

assert_eq!(t.size(), 3);

let t = parse_term(&mut sig, "A(B)").expect("parse of A(B)");

assert_eq!(t.size(), 2);

pub fn at(&self, place: &[usize]) -> Option<&Term>

Get the subterm at the given Place if possible. Otherwise, return None.

Examples

let mut sig = Signature::default();
let op = sig.new_op(0, Some("A".to_string()));
let t = parse_term(&mut sig, "B(A)").expect("parse of B(A)");

assert_eq!(t.size(), 2);
let p: &[usize] = &[7];

assert_eq!(t.at(p), None);

let p: &[usize] = &[0];
let args = vec![];

assert_eq!(t.at(p), Some(&Term::Application { op, args }));

pub fn replace(&self, place: &[usize], subterm: Term) -> Option<Term>

Create a copy of the Term where the Term at the given Place has been replaced with subterm.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "B(A)").expect("parse of B(A)");
let t2 = parse_term(&mut sig, "C").expect("parse of C");
let expected_term = parse_term(&mut sig, "B(C)").expect("parse of B(C)");

let p: &[usize] = &[0];
let new_term = t.replace(p, t2);

assert_eq!(new_term, Some(expected_term));

pub fn shared_score(t1: &Term, t2: &Term) -> f64

Compute the percentage of shared subterms between two Terms.

Examples

let mut sig = Signature::default();

let t1 = parse_term(&mut sig, "S (K y_ z_)").expect("parse of S K y_ z_");
let t2 = parse_term(&mut sig, "S (K w_ x_)").expect("parse of S K w_ x_");
let t3 = parse_term(&mut sig, "K (K w_ x_) S").expect("parse of S K w_ x_");

// Identical Terms
assert_eq!(Term::shared_score(&t1, &t1), 1.0);

// Alpha-equivalent Terms
assert_eq!(Term::shared_score(&t1, &t2), 1.0);

// Distinct Terms
assert_eq!(Term::shared_score(&t1, &t3), 0.75);

pub fn substitute(&self, sub: &HashMap<&Variable, &Term>) -> Term

Given a mapping from Variables to Terms, perform a substitution.

Examples

let mut sig = Signature::default();

let term_before = parse_term(&mut sig, "S K y_ z_").expect("parse of S K y_ z_");
let s_term = parse_term(&mut sig, "S").expect("parse of S");
let k_term = parse_term(&mut sig, "K").expect("parse of K");

let vars = sig.variables();
let y = &vars[0];
let z = &vars[1];

let mut sub = HashMap::new();
sub.insert(y, &s_term);
sub.insert(z, &k_term);

let expected_term = parse_term(&mut sig, "S K S K").expect("parse of S K S K");
let subbed_term = term_before.substitute(&sub);

assert_eq!(subbed_term, expected_term);

pub fn alpha<'a>(
    t1: &'a Term,
    t2: &'a Term
) -> Option<HashMap<&'a Variable, &'a Term>>

Compute the alpha equivalence for two Terms.

Examples

let mut sig = Signature::default();
let s = sig.new_op(0, Some("S".to_string()));

let t = parse_term(&mut sig, "S K y_ z_").expect("parse of S K y_ z_");
let t2 = parse_term(&mut sig, "S K a_ b_").expect("parse of S K a_ b_");
let t3 = parse_term(&mut sig, "S K y_").expect("parse of S K y_");

let vars = sig.variables();
let (y, z, a, b) = (&vars[0], &vars[1], &vars[2], &vars[3]);

assert_eq!(y.display(), "y_".to_string());
assert_eq!(z.display(), "z_".to_string());
assert_eq!(a.display(), "a_".to_string());
assert_eq!(b.display(), "b_".to_string());

let ta = Term::Variable(a.clone());
let tb = Term::Variable(b.clone());
let mut expected_alpha: HashMap<&Variable, &Term> = HashMap::new();
expected_alpha.insert(y, &ta);
expected_alpha.insert(z, &tb);

assert_eq!(Term::alpha(&t, &t2), Some(expected_alpha));

assert_eq!(Term::alpha(&t, &t3), None);

pub fn shape_equivalent(t1: &Term, t2: &Term) -> bool

Returns whether two Terms are shape equivalent.

Shape equivalence is where two Terms may not contain the same subterms, but they share the same structure(a.k.a. shape).

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "S K y_ z_").expect("parse of S K y_ z_");
let t2 = parse_term(&mut sig, "A B x_ w_").expect("parse of A B x_ w_");
let t3 = parse_term(&mut sig, "S K y_").expect("parse of S K y_");

assert!(Term::shape_equivalent(&t, &t2));

assert!(!Term::shape_equivalent(&t, &t3));

pub fn pmatch<'a>(
    cs: Vec<(&'a Term, &'a Term)>
) -> Option<HashMap<&'a Variable, &'a Term>>

Given a vector of contraints, return a substitution which satisfies the constrants. If the constraints are not satisfiable, return None. Constraints are in the form of patterns, where substitutions are only considered for variables in the first term of each pair.

For more information see Pattern Matching.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "C(A)").expect("parse of C(A)");

let t2 = parse_term(&mut sig, "C(x_)").expect("parse of C(x_)");

let t3 = parse_term(&mut sig, "C(y_)").expect("parse of C(y_)");

let t4 = parse_term(&mut sig, "A(x_)").expect("parse of A(x_)");

assert_eq!(Term::pmatch(vec![(&t, &t2)]), None);

let t_k = &t2.variables()[0];
let t_v = Term::Variable(t3.variables()[0].clone());
let mut expected_sub = HashMap::new();

// maps variable x in term t2 to variable y in term t3
expected_sub.insert(t_k, &t_v);

assert_eq!(Term::pmatch(vec![(&t2, &t3)]), Some(expected_sub));

assert_eq!(Term::pmatch(vec![(&t3, &t4)]), None);

pub fn unify<'a>(
    cs: Vec<(&'a Term, &'a Term)>
) -> Option<HashMap<&'a Variable, &'a Term>>

Given a vector of contraints, return a substitution which satisfies the constrants. If the constraints are not satisfiable, return None.

For more information see Unification.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "C(A)").expect("parse of C(A)");

let t2 = parse_term(&mut sig, "C(x_)").expect("parse of C(x_)");

let t3 = parse_term(&mut sig, "C(y_)").expect("parse of C(y_)");

let t4 = parse_term(&mut sig, "B(x_)").expect("parse of B(x_)");

let t_k = &t2.variables()[0];
let t_v = Term::Application {
    op: t.operators()[0].clone(),
    args:vec![],
};

let mut expected_sub = HashMap::new();

// maps variable x in term t2 to constant A in term t
expected_sub.insert(t_k, &t_v);

assert_eq!(Term::unify(vec![(&t, &t2)]), Some(expected_sub));

let t_v = Term::Variable(t3.variables()[0].clone());

let mut expected_sub = HashMap::new();

 // maps variable x in term t2 to variable y in term t3
expected_sub.insert(t_k, &t_v);

assert_eq!(Term::unify(vec![(&t2, &t3)]), Some(expected_sub));

assert_eq!(Term::unify(vec![(&t3, &t4)]), None);

Trait Implementations

impl PartialEq<Term> for Term

fn eq(&self, other: &Term) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Term) -> bool

This method tests for !=.

impl Clone for Term

fn clone(&self) -> Term

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl From<Term> for Context

fn from(t: Term) -> Context

Performs the conversion.

impl Eq for Term

impl Debug for Term

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Hash for Term

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given [Hasher].