oxilean_std/coinduction/
types.rs

1//! Coinductive proofs and greatest fixed points — types.
2
3/// A lazy, eventually-periodic stream.
4///
5/// The stream is defined by a finite `prefix` followed by an infinitely
6/// repeating `cycle`.  If `cycle` is empty, the stream is exactly `prefix`
7/// (i.e. finite for practical purposes but the API treats it as an
8/// infinite stream repeating the last element when both slices are exhausted,
9/// which is handled in the accessor functions).
10#[derive(Clone, Debug, PartialEq, Eq)]
11pub struct LazyStream<T: Clone> {
12    /// Finite prefix elements (emitted first, each exactly once).
13    pub(super) prefix: Vec<T>,
14    /// Repeating cycle (emitted round-robin after the prefix runs out).
15    /// Must be non-empty unless the stream is intended to be empty.
16    pub(super) cycle: Vec<T>,
17}
18
19/// A set of state pairs representing a candidate bisimulation relation.
20///
21/// A `BisimulationRelation<S>` is *valid* if for every pair `(s, t)` in the
22/// relation, every transition from `s` has a matching transition from `t`
23/// (and vice-versa) such that the resulting states are again in the relation.
24#[derive(Clone, Debug, PartialEq, Eq)]
25pub struct BisimulationRelation<S: Clone + Eq> {
26    pub(super) pairs: Vec<(S, S)>,
27}
28
29/// A completed coinductive proof certificate.
30///
31/// Contains the bisimulation relation that was found to be valid, plus a
32/// trace of the progress steps made during the proof search.
33#[derive(Clone, Debug)]
34pub struct CoinductiveProof<S: Clone + Eq> {
35    pub relation: BisimulationRelation<S>,
36    pub progress: Vec<String>,
37}
38
39/// A coalgebra map S → O × S represented as an explicit transition table.
40///
41/// Each entry `(src, obs, dst)` means: when in state `src`, emit observation
42/// `obs` and move to state `dst`.
43#[derive(Clone, Debug)]
44pub struct CoalgebraMap<S: Clone + Eq, O: Clone + Eq> {
45    pub(super) transitions: Vec<(S, O, S)>,
46}
47
48/// A Greibach Normal Form grammar used for coinductive context-free grammars.
49///
50/// Each rule `(lhs, terminal, rhs)` expands non-terminal `lhs` by consuming
51/// terminal `terminal` and pushing `rhs` non-terminals onto the stack.
52#[derive(Clone, Debug)]
53pub struct GreibachNormalForm {
54    pub(super) rules: Vec<(String, char, Vec<String>)>,
55}
56
57/// `Codata<F>` represents the greatest fixed point of the functor `F`.
58///
59/// Because Rust does not support infinite types directly, we model it as an
60/// explicit thunk: call `unfold()` to expose one layer of the codata on demand.
61pub struct Codata<F> {
62    /// The unfolding thunk: call it to expose one layer of the codata.
63    pub(super) unfold: Box<dyn Fn() -> F>,
64}
65
66/// A finite approximation of an infinite stream (one unrolled cons cell).
67#[derive(Clone, Debug)]
68pub struct StreamNode<T: Clone> {
69    pub head: T,
70    pub tail: Box<StreamApprox<T>>,
71}
72
73/// A finite approximation of a stream (either `Nil` or a `Cons`).
74#[derive(Clone, Debug)]
75pub enum StreamApprox<T: Clone> {
76    /// Stream exhausted at this depth.
77    Nil,
78    Cons(Box<StreamNode<T>>),
79}
oxilean_std/coinduction/types.rs

oxilean_std/coinduction/
types.rs
