Struct programinduction::trs::TRS

pub struct TRS { /* private fields */ }

Manages the semantics of a term rewriting system.

Implementations

impl TRS

pub fn new( lexicon: &Lexicon, rules: Vec<Rule>, ctx: &TypeContext ) -> Result<TRS, TypeError>

Create a new TRS under the given Lexicon. Any background knowledge will be appended to the given ruleset.

Example

use polytype::{ptp, tp};
use programinduction::trs::{TRS, Lexicon};
use term_rewriting::{Signature, parse_rule};
use polytype::Context as TypeContext;

let mut sig = Signature::default();

let mut ops = vec![];
sig.new_op(2, Some("PLUS".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int), tp!(int)]]);
sig.new_op(1, Some("SUCC".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int)]]);
sig.new_op(0, Some("ZERO".to_string()));
ops.push(ptp![int]);

let rules = vec![
    parse_rule(&mut sig, "PLUS(x_ ZERO) = x_").expect("parsed rule"),
    parse_rule(&mut sig, "PLUS(x_ SUCC(y_)) = SUCC(PLUS(x_ y_))").expect("parsed rule"),
];

let vars = vec![
    ptp![int],
    ptp![int],
    ptp![int],
];

let lexicon = Lexicon::from_signature(sig, ops, vars, vec![], vec![], false, TypeContext::default());

let ctx = lexicon.context();

let trs = TRS::new(&lexicon, rules, &ctx).unwrap();

assert_eq!(trs.size(), 12);

pub fn size(&self) -> usize

The size of the underlying term_rewriting::TRS.

pub fn len(&self) -> usize

The length of the underlying term_rewriting::TRS.

pub fn is_empty(&self) -> bool

Is the underlying term_rewriting::TRS empty?.

pub fn pseudo_log_prior(&self) -> f64

A pseudo log prior for a TRS: the negative size of the TRS.

pub fn log_likelihood(&self, data: &[Rule], params: ModelParams) -> f64

A log likelihood for a TRS: the probability of data’s RHSs appearing in term_rewriting::Traces rooted at its LHSs.

pub fn posterior(&self, data: &[Rule], params: ModelParams) -> f64

Combine pseudo_log_prior and log_likelihood, failing early if the prior is 0.0.

pub fn add_rule<R: Rng>( &self, contexts: &[RuleContext], atom_weights: (f64, f64, f64), max_size: usize, rng: &mut R ) -> Result<TRS, SampleError>

Sample a rule and add it to the rewrite system.

Example

use polytype::{ptp, tp, Context as TypeContext};
use programinduction::trs::{TRS, Lexicon};
use rand::{rngs::SmallRng, SeedableRng};
use term_rewriting::{Context, RuleContext, Signature, parse_rule};

let mut sig = Signature::default();

let mut ops = vec![];
sig.new_op(2, Some(".".to_string()));
ops.push(ptp![0, 1; @arrow[tp!(@arrow[tp!(0), tp!(1)]), tp!(0), tp!(1)]]);
sig.new_op(2, Some("PLUS".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int), tp!(int)]]);
sig.new_op(1, Some("SUCC".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int)]]);
sig.new_op(0, Some("ZERO".to_string()));
ops.push(ptp![int]);

let rules = vec![
    parse_rule(&mut sig, "PLUS(x_ ZERO) = x_").expect("parsed rule"),
    parse_rule(&mut sig, "PLUS(x_ SUCC(y_)) = SUCC(PLUS(x_ y_))").expect("parsed rule"),
];

let vars = vec![
    ptp![int],
    ptp![int],
    ptp![int],
];

for op in sig.operators() {
    println!("{:?}/{}", op.name(), op.arity())
}
for r in &rules {
    println!("{:?}", r.pretty());
}
let lexicon = Lexicon::from_signature(sig, ops, vars, vec![], vec![], false, TypeContext::default());

let mut trs = TRS::new(&lexicon, rules, &lexicon.context()).unwrap();

assert_eq!(trs.len(), 2);

let contexts = vec![
    RuleContext {
        lhs: Context::Hole,
        rhs: vec![Context::Hole],
    }
];
let rng = &mut SmallRng::from_seed([1u8; 32]);
let atom_weights = (0.5, 0.25, 0.25);
let max_size = 50;

if let Ok(new_trs) = trs.add_rule(&contexts, atom_weights, max_size, rng) {
    assert_eq!(new_trs.len(), 3);
} else {
    assert_eq!(trs.len(), 2);
}

pub fn delete_rule<R: Rng>(&self, rng: &mut R) -> Result<TRS, SampleError>

Delete a rule from the rewrite system if possible. Background knowledge cannot be deleted.

pub fn randomly_move_rule<R: Rng>( &self, rng: &mut R ) -> Result<TRS, SampleError>

Move a Rule from one place in the TRS to another at random, excluding the background.

Example

use polytype::{ptp, tp, Context as TypeContext};
use programinduction::trs::{TRS, Lexicon};
use rand::{rngs::SmallRng, SeedableRng};
use term_rewriting::{Context, RuleContext, Signature, parse_rule};

let mut sig = Signature::default();

let mut ops = vec![];
sig.new_op(2, Some(".".to_string()));
ops.push(ptp![0, 1; @arrow[tp!(@arrow[tp!(0), tp!(1)]), tp!(0), tp!(1)]]);
sig.new_op(2, Some("PLUS".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int), tp!(int)]]);
sig.new_op(1, Some("SUCC".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int)]]);
sig.new_op(0, Some("ZERO".to_string()));
ops.push(ptp![int]);

let rules = vec![
    parse_rule(&mut sig, "PLUS(x_ ZERO) = x_").expect("parsed rule"),
    parse_rule(&mut sig, "PLUS(x_ SUCC(y_)) = SUCC(PLUS(x_ y_))").expect("parsed rule"),
];

let vars = vec![
    ptp![int],
    ptp![int],
    ptp![int],
];

println!("{:?}", sig.operators());
for op in sig.operators() {
    println!("{:?}/{}", op.name(), op.arity())
}
for r in &rules {
    println!("{:?}", r);
}

let ctx = TypeContext::default();
let lexicon = Lexicon::from_signature(sig.clone(), ops, vars, vec![], vec![], false, ctx);

let mut trs = TRS::new(&lexicon, rules, &lexicon.context()).unwrap();

let pretty_before = trs.to_string();

let rng = &mut SmallRng::from_seed([1u8; 32]);

let new_trs = trs.randomly_move_rule(rng).expect("failed when moving rule");

assert_ne!(pretty_before, new_trs.to_string());
assert_eq!(new_trs.to_string(), "PLUS(x_ SUCC(y_)) = SUCC(PLUS(x_ y_));\nPLUS(x_ ZERO) = x_;");

pub fn local_difference<R: Rng>(&self, rng: &mut R) -> Result<TRS, SampleError>

Selects a rule from the TRS at random, finds all differences in the LHS and RHS, and makes rules from those differences and inserts them back into the TRS imediately after the background.

Example

use polytype::{ptp, tp, Context as TypeContext};
use programinduction::trs::{TRS, Lexicon};
use rand::{rngs::SmallRng, SeedableRng};
use term_rewriting::{Context, RuleContext, Signature, parse_rule};

let mut sig = Signature::default();

let mut ops = vec![];
sig.new_op(2, Some(".".to_string()));
ops.push(ptp![0, 1; @arrow[tp!(@arrow[tp!(0), tp!(1)]), tp!(0), tp!(1)]]);
sig.new_op(2, Some("PLUS".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int), tp!(int)]]);
sig.new_op(1, Some("SUCC".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int)]]);
sig.new_op(0, Some("ZERO".to_string()));
ops.push(ptp![int]);

let rules = vec![
    parse_rule(&mut sig, "SUCC(PLUS(x_ SUCC(y_))) = SUCC(SUCC(PLUS(x_ y_)))").expect("parsed rule"),
];

let vars = vec![
    ptp![int],
    ptp![int],
    ptp![int],
];

for op in sig.operators() {
    println!("{:?}/{}", op.name(), op.arity())
}
for r in &rules {
    println!("{:?}", r.pretty());
}
let lexicon = Lexicon::from_signature(sig, ops, vars, vec![], vec![], false, TypeContext::default());

let mut trs = TRS::new(&lexicon, rules, &lexicon.context()).unwrap();

assert_eq!(trs.len(), 1);

let rng = &mut SmallRng::from_seed([1u8; 32]);

if let Ok(new_trs) = trs.local_difference(rng) {
    assert_eq!(new_trs.len(), 2);
    let display_str = format!("{}", new_trs);
    assert_eq!(display_str, "PLUS(x_ SUCC(y_)) = SUCC(PLUS(x_ y_));\nSUCC(PLUS(x_ SUCC(y_))) = SUCC(SUCC(PLUS(x_ y_)));");
} else {
    assert_eq!(trs.len(), 1);
}

pub fn swap_lhs_and_rhs<R: Rng>(&self, rng: &mut R) -> Result<TRS, SampleError>

Selects a rule from the TRS at random, swaps the LHS and RHS if possible and inserts the resulting rules back into the TRS imediately after the background.

Example

use polytype::{ptp, tp, Context as TypeContext};
use programinduction::trs::{TRS, Lexicon};
use rand::{rngs::SmallRng, SeedableRng};
use term_rewriting::{Context, RuleContext, Signature, parse_rule};

let mut sig = Signature::default();

let mut ops = vec![];
sig.new_op(2, Some(".".to_string()));
ops.push(ptp![0, 1; @arrow[tp!(@arrow[tp!(0), tp!(1)]), tp!(0), tp!(1)]]);
sig.new_op(2, Some("PLUS".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int), tp!(int)]]);
sig.new_op(1, Some("SUCC".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int)]]);
sig.new_op(0, Some("ZERO".to_string()));
ops.push(ptp![int]);

let rules = vec![
    parse_rule(&mut sig, "PLUS(x_ SUCC(y_)) = SUCC(PLUS(x_ y_)) | PLUS(SUCC(x_) y_)").expect("parsed rule"),
];

let vars = vec![
    ptp![int],
    ptp![int],
    ptp![int],
];

for op in sig.operators() {
    println!("{:?}/{}", op.name(), op.arity())
}
for r in &rules {
    println!("{:?}", r.pretty());
}

let lexicon = Lexicon::from_signature(sig, ops, vars, vec![], vec![], false, TypeContext::default());

let mut trs = TRS::new(&lexicon, rules, &lexicon.context()).unwrap();

assert_eq!(trs.len(), 1);

let rng = &mut SmallRng::from_seed([1u8; 32]);

if let Ok(new_trs) = trs.swap_lhs_and_rhs(rng) {
    assert_eq!(new_trs.len(), 2);
    let display_str = format!("{}", new_trs);
    assert_eq!(display_str, "SUCC(PLUS(x_ y_)) = PLUS(x_ SUCC(y_));\nPLUS(SUCC(x_) y_) = PLUS(x_ SUCC(y_));");
} else {
    assert_eq!(trs.len(), 1);
}


let mut sig = Signature::default();

let mut ops = vec![];
sig.new_op(2, Some(".".to_string()));
ops.push(ptp![0, 1; @arrow[tp!(@arrow[tp!(0), tp!(1)]), tp!(0), tp!(1)]]);
sig.new_op(2, Some("A".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int), tp!(int)]]);
sig.new_op(1, Some("B".to_string()));
ops.push(ptp![@arrow[tp!(int), tp!(int)]]);

let rules = vec![
    parse_rule(&mut sig, "A(x_ y_) = B(x_ )").expect("parsed rule"),
];

let vars = vec![
    ptp![int],
    ptp![int],
    ptp![int],
];

let lexicon = Lexicon::from_signature(sig, ops, vars, vec![], vec![], false, TypeContext::default());

let mut trs = TRS::new(&lexicon, rules, &lexicon.context()).unwrap();

assert!(trs.swap_lhs_and_rhs(rng).is_err());

Trait Implementations

impl Clone for TRS

fn clone(&self) -> TRS

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for TRS

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

Formats the value using the given formatter.

impl Display for TRS

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

Formats the value using the given formatter.

impl PartialEq for TRS

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

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

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

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for TRS