Struct GameSemantics 

pub struct GameSemantics {
    pub arenas: Vec<String>,
}

Game semantics for linear logic: arenas and innocent strategies.

Fields

arenas: Vec<String>

Named arenas (one per type in the context).

Implementations

impl GameSemantics

pub fn new(arenas: Vec<String>) -> Self

Create a new game semantics structure.

pub fn innocent_strategies(&self) -> Vec<String>

Innocent strategies: strategies that only depend on the visible history (the P-view), not the full history.

pub fn composition(&self) -> String

Composition of strategies (Abramsky-Jagadeesan-Malacaria style).

pub fn tensor(&self) -> String

Tensor product of arenas.

pub fn full_completeness_statement(&self) -> String

Full completeness: every innocent strategy corresponds to a proof.

Trait Implementations

impl Clone for GameSemantics

fn clone(&self) -> GameSemantics

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for GameSemantics

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

Formats the value using the given formatter.