Struct AlphaEquivalenceChecker 

pub struct AlphaEquivalenceChecker;

Check α-equivalence of two terms (de Bruijn terms are equal up to renaming of bound variables by definition — so alpha-equivalence is just structural equality after normalization of bound variable names, which in de Bruijn form is plain equality).

Implementations

impl AlphaEquivalenceChecker

pub fn new() -> Self

Create a new checker.

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

Check whether two terms are alpha-equivalent. With de Bruijn indices, alpha-equivalence is structural equality.

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

Check alpha-equivalence modulo one layer of beta-reduction. Useful when terms may differ by a single administrative redex.

pub fn alpha_equiv_normalized(&self, t1: &Term, t2: &Term, limit: usize) -> bool

Check whether two terms are alpha-equivalent after full normalization (with a step limit).

Trait Implementations

impl Default for AlphaEquivalenceChecker

fn default() -> Self

Returns the “default value” for a type.