compiler/io.github.aplcornell.viaduct.algebra/FreeDistributiveLattice

FreeDistributiveLattice

class FreeDistributiveLattice<A> : HeytingAlgebra<FreeDistributiveLattice<A>>

The free distributive lattice over an arbitrary set A of elements. In addition to lattice identities, the following hold:

a /\ (b \/ c) == (a /\ b) \/ (a /\ c)

a \/ (b /\ c) == (a \/ b) /\ (a \/ c)

Constructors

FreeDistributiveLattice

fun <A> FreeDistributiveLattice(element: A)

Types

object Companion

LessThanOrEqualTo

data class LessThanOrEqualTo<A>(val from: FreeDistributiveLattice<A>, val to: FreeDistributiveLattice<A>)

Represents the assumption that from is below to.

Functions

open operator override fun equals(other: Any?): Boolean

open override fun hashCode(): Int

open infix override fun imply(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A>

Returns the relative pseudocomplement of this relative to that. the relative pseudocomplement is greatest x s.t. this & x <= that.

open infix override fun join(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A>

The least upper bound of this and that.

lessThanOrEqualTo

fun lessThanOrEqualTo(that: FreeDistributiveLattice<A>, assumptions: List<FreeDistributiveLattice.LessThanOrEqualTo<A>>): Boolean

open infix override fun meet(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A>

The greatest lower bound of this and that.

open override fun toString(): String

Properties

val joinOfMeets: PersistentSet<Meet<A>>