Struct RealizabilityModel 

pub struct RealizabilityModel {
    pub ty: PcfType,
}

A realizability model for PCF types.

Each type is interpreted as a set of realizers (PCA elements), with the partial equivalence relation identifying equivalent realizers.

Fields

ty: PcfType

The PCF type being modeled

Implementations

impl RealizabilityModel

pub fn new(ty: PcfType) -> Self

Create a model for a given PCF type.

pub fn is_realizer(&self, val: &PcfValue) -> bool

Check if a value is a valid realizer for this model’s type.

pub fn per_equiv(&self, v1: &PcfValue, v2: &PcfValue) -> bool

The PER (partial equivalence relation) for this type. Two values are PER-equivalent if they are both valid realizers and computationally equivalent.

pub fn domain(&self) -> impl Fn(&PcfValue) -> bool + '_

The domain of the PER: values related to themselves.