Enum Formula 

pub enum Formula {
    Atom(String),
    NegAtom(String),
    Tensor(Box<Formula>, Box<Formula>),
    Par(Box<Formula>, Box<Formula>),
    One,
    Bottom,
    With(Box<Formula>, Box<Formula>),
    Plus(Box<Formula>, Box<Formula>),
    Top,
    Zero,
    OfCourse(Box<Formula>),
    WhyNot(Box<Formula>),
    Lolli(Box<Formula>, Box<Formula>),
}

A linear logic formula.

Linear logic has a rich set of connectives split into multiplicative and additive families, plus exponentials for controlled structural rules.

Variants

Atom(String)

Atomic proposition

NegAtom(String)

Negated atomic proposition (A⊥)

Tensor(Box<Formula>, Box<Formula>)

Tensor product (A ⊗ B) - “both A and B independently”

Par(Box<Formula>, Box<Formula>)

Par (A ⅋ B) - “A or B, opponent chooses”

One

Multiplicative unit (1)

Bottom

Multiplicative false (⊥)

With(Box<Formula>, Box<Formula>)

With (A & B) - “both available, you choose one”

Plus(Box<Formula>, Box<Formula>)

Plus (A ⊕ B) - “one of them, I choose which”

Top

Additive truth (⊤)

Zero

Additive false (0)

OfCourse(Box<Formula>)

Of course (!A) - “unlimited supply of A, can copy/discard”

WhyNot(Box<Formula>)

Why not (?A) - “demand for A”

Lolli(Box<Formula>, Box<Formula>)

Linear implication (A ⊸ B) - sugar for A⊥ ⅋ B

Implementations

impl Formula

pub fn negate(&self) -> Formula

Compute the linear negation of a formula.

Linear negation is involutive: (A⊥)⊥ = A

De Morgan dualities:

• (A ⊗ B)⊥ = A⊥ ⅋ B⊥
• (A ⅋ B)⊥ = A⊥ ⊗ B⊥
• (A & B)⊥ = A⊥ ⊕ B⊥
• (A ⊕ B)⊥ = A⊥ & B⊥
• 1⊥ = ⊥
• ⊥⊥ = 1
• (!A)⊥ = ?(A⊥)
• (?A)⊥ = !(A⊥)

pub fn desugar(&self) -> Formula

Desugar the formula by expanding A ⊸ B to A⊥ ⅋ B.

pub fn is_positive(&self) -> bool

Returns true if this formula is positive (async/eager).

Positive formulas: ⊗, 1, ⊕, 0, !, atoms

pub fn is_negative(&self) -> bool

Returns true if this formula is negative (sync/lazy).

Negative formulas: ⅋, ⊥, &, ⊤, ?, negated atoms

pub fn pretty(&self) -> String

Pretty print the formula with Unicode symbols.

pub fn pretty_ascii(&self) -> String

Pretty print the formula with ASCII symbols.

pub fn pretty_latex(&self) -> String

Pretty print the formula for LaTeX.

pub fn atom(name: impl Into<String>) -> Formula

Create an atom formula.

pub fn neg_atom(name: impl Into<String>) -> Formula

Create a negated atom formula.

pub fn tensor(a: Formula, b: Formula) -> Formula

Create a tensor (A ⊗ B).

pub fn par(a: Formula, b: Formula) -> Formula

Create a par (A ⅋ B).

pub fn lolli(a: Formula, b: Formula) -> Formula

Create a linear implication (A ⊸ B).

pub fn with(a: Formula, b: Formula) -> Formula

Create a with (A & B).

pub fn plus(a: Formula, b: Formula) -> Formula

Create a plus (A ⊕ B).

pub fn of_course(a: Formula) -> Formula

Create an of-course (!A).

pub fn why_not(a: Formula) -> Formula

Create a why-not (?A).

Trait Implementations

impl Clone for Formula

fn clone(&self) -> Formula

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Formula

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

Formats the value using the given formatter.

impl Eq for Formula

impl Hash for Formula

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Formula

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Formula