Struct BarRecursion 

pub struct BarRecursion {
    pub max_depth: usize,
    pub bar: Vec<bool>,
}

Simulate Spector’s bar recursion up to a bounded depth. This corresponds to the BarRecursor kernel axiom.

Fields

max_depth: usize

Maximum recursion depth allowed.

bar: Vec<bool>

The bar predicate: returns true when recursion should stop.

Implementations

impl BarRecursion

pub fn new(max_depth: usize) -> Self

Create a new BarRecursion with a given depth bound.

pub fn set_bar(&mut self, n: usize)

Set the bar at position n (meaning: sequences of length n satisfy the bar).

pub fn in_bar(&self, n: usize) -> bool

Check whether position n is in the bar.

pub fn compute( &self, n: usize, y_val: impl Fn(usize) -> i64, h_step: impl Fn(usize, i64) -> i64, ) -> i64

Compute the bar recursion value for sequence length n using functionals Y and H. y_val(n) is the “stopping value” when n is in the bar. h_step(n, prev) computes the step from n using the previous value.

pub fn bar_depth(&self) -> Option<usize>

Depth of the bar (smallest n in the bar), if any.

Trait Implementations

impl Clone for BarRecursion

fn clone(&self) -> BarRecursion

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BarRecursion

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

Formats the value using the given formatter.