Struct GaloisConnection 

pub struct GaloisConnection<A, B> {
    pub lower: Box<dyn Fn(A) -> B>,
    pub upper: Box<dyn Fn(B) -> A>,
}

Representation of a Galois connection between two posets.

A Galois connection is a pair of monotone maps (l : A → B, u : B → A) satisfying: l(a) ≤ b ↔ a ≤ u(b).

Fields

lower: Box<dyn Fn(A) -> B>

Left adjoint (lower adjoint).

upper: Box<dyn Fn(B) -> A>

Right adjoint (upper adjoint).

Implementations

impl<A: Clone, B: Clone> GaloisConnection<A, B>

pub fn new( lower: impl Fn(A) -> B + 'static, upper: impl Fn(B) -> A + 'static, ) -> Self

Create a new Galois connection from the adjoint pair.

pub fn apply_lower(&self, a: A) -> B

Apply the lower adjoint.

pub fn apply_upper(&self, b: B) -> A

Apply the upper adjoint.

pub fn verify( &self, a: A, b: B, le_a: impl Fn(&A, &A) -> bool, le_b: impl Fn(&B, &B) -> bool, ) -> bool

Verify the Galois connection condition on concrete elements given order predicates for both sides.