or run

npx @tessl/cli init
Log in

Version

Tile

Overview

Evals

Files

docs

basic-structures.mdindex.mdinstances.mdlattice-structures.mdpriority-system.mdring-structures.md
tile.json

lattice-structures.mddocs/

Lattice Structures

Lattice structures represent order-theoretic algebraic systems with meet (∧) and join (∨) operations. The algebra library provides a comprehensive hierarchy from basic semilattices to Boolean algebras and Heyting algebras, enabling logical and order-theoretic abstractions.

Capabilities

Basic Lattice Structures

JoinSemilattice

Provides join operation (least upper bound/supremum).

/**
 * Join semilattice with associative, commutative, idempotent join operation
 * Join represents "least upper bound" or "supremum"
 */
trait JoinSemilattice[A] {
  /** Join operation (∨, least upper bound) */
  def join(lhs: A, rhs: A): A
  /** Get underlying semilattice structure */
  def joinSemilattice: Semilattice[A]
  /** Derive partial order from join operation */
  def joinPartialOrder(implicit ev: Eq[A]): PartialOrder[A]
}

object JoinSemilattice {
  def apply[A](implicit ev: JoinSemilattice[A]): JoinSemilattice[A] = ev
}

MeetSemilattice

Provides meet operation (greatest lower bound/infimum).

/**
 * Meet semilattice with associative, commutative, idempotent meet operation  
 * Meet represents "greatest lower bound" or "infimum"
 */
trait MeetSemilattice[A] {
  /** Meet operation (∧, greatest lower bound) */
  def meet(lhs: A, rhs: A): A
  /** Get underlying semilattice structure */
  def meetSemilattice: Semilattice[A]
  /** Derive partial order from meet operation */
  def meetPartialOrder(implicit ev: Eq[A]): PartialOrder[A]
}

object MeetSemilattice {
  def apply[A](implicit ev: MeetSemilattice[A]): MeetSemilattice[A] = ev
}

Lattice

Complete lattice with both meet and join operations.

/**
 * Lattice with both meet and join operations
 * Satisfies absorption laws: meet(a, join(a, b)) == join(a, meet(a, b)) == a
 */
trait Lattice[A] extends JoinSemilattice[A] with MeetSemilattice[A] {
  /** Get dual lattice where meet and join are swapped */
  def dual: Lattice[A]
}

object Lattice {
  def apply[A](implicit ev: Lattice[A]): Lattice[A] = ev
}

Usage Example:

import algebra.lattice._
import algebra.instances.all._

// Integer lattice using min/max
val intLattice = Lattice[Int]
val meet = intLattice.meet(5, 3)  // min(5, 3) = 3
val join = intLattice.join(5, 3)  // max(5, 3) = 5

// Boolean lattice using logical operations
val boolLattice = Lattice[Boolean] 
val conjunction = boolLattice.meet(true, false)  // false (AND)
val disjunction = boolLattice.join(true, false)  // true (OR)

Bounded Lattice Structures

BoundedJoinSemilattice

Join semilattice with bottom element.

/**
 * Join semilattice with bottom element (least element)
 */
trait BoundedJoinSemilattice[A] extends JoinSemilattice[A] {
  /** Bottom element (⊥, least element) */
  def zero: A
  /** Test if element is bottom */
  def isZero(a: A)(implicit ev: Eq[A]): Boolean
  /** Get bounded semilattice structure */
  def joinSemilattice: BoundedSemilattice[A]
}

BoundedMeetSemilattice

Meet semilattice with top element.

/**
 * Meet semilattice with top element (greatest element)
 */
trait BoundedMeetSemilattice[A] extends MeetSemilattice[A] {
  /** Top element (⊤, greatest element) */
  def one: A
  /** Test if element is top */
  def isOne(a: A)(implicit ev: Eq[A]): Boolean
  /** Get bounded semilattice structure */
  def meetSemilattice: BoundedSemilattice[A]
}

BoundedLattice

Lattice with both top and bottom elements.

/**
 * Lattice with both top (⊤) and bottom (⊥) elements
 */
trait BoundedLattice[A] extends Lattice[A] 
  with BoundedMeetSemilattice[A] 
  with BoundedJoinSemilattice[A] {
  /** Get dual bounded lattice */
  override def dual: BoundedLattice[A]
}

Distributive Lattice Structures

DistributiveLattice

Lattice where join distributes over meet and vice versa.

/**
 * Distributive lattice where operations distribute over each other
 * meet(a, join(b, c)) == join(meet(a, b), meet(a, c))
 * join(a, meet(b, c)) == meet(join(a, b), join(a, c))
 */
trait DistributiveLattice[A] extends Lattice[A]

object DistributiveLattice {
  def apply[A](implicit ev: DistributiveLattice[A]): DistributiveLattice[A] = ev
  /** Create distributive lattice from total order using min/max */
  def minMax[A: Order]: DistributiveLattice[A]
}

BoundedDistributiveLattice

Bounded distributive lattice.

/**
 * Bounded distributive lattice
 * Can be viewed as a commutative rig where join is addition and meet is multiplication
 */
trait BoundedDistributiveLattice[A] extends BoundedLattice[A] with DistributiveLattice[A] {
  /** View this lattice as a commutative rig */
  def asCommutativeRig: CommutativeRig[A]
  /** Get dual bounded distributive lattice */
  override def dual: BoundedDistributiveLattice[A]
}

Logic Structures

Logic

Logic operations on bounded distributive lattice.

/**
 * Logic operations on bounded distributive lattice
 * Provides standard logical connectives
 */
trait Logic[A] extends BoundedDistributiveLattice[A] {
  /** Logical AND (same as meet) */
  def and(a: A, b: A): A
  /** Logical OR (same as join) */  
  def or(a: A, b: A): A
  /** Logical NOT (complement) */
  def not(a: A): A
  /** Exclusive OR */
  def xor(a: A, b: A): A
  /** NAND (NOT AND) */
  def nand(a: A, b: A): A
  /** NOR (NOT OR) */
  def nor(a: A, b: A): A  
  /** XNOR (NOT XOR) */
  def nxor(a: A, b: A): A
}

object Logic {
  def apply[A](implicit ev: Logic[A]): Logic[A] = ev
  /** Create Logic from Heyting algebra */
  def fromHeyting[A](implicit h: Heyting[A]): Logic[A]
}

DeMorgan

Logic satisfying De Morgan's laws.

/**
 * Logic satisfying De Morgan's laws
 * not(and(a, b)) == or(not(a), not(b))
 * not(or(a, b)) == and(not(a), not(b))
 */
trait DeMorgan[A] extends Logic[A] {
  /** Implication operation (a → b) */
  def imp(a: A, b: A): A
}

object DeMorgan {
  def apply[A](implicit ev: DeMorgan[A]): DeMorgan[A] = ev
  /** Create DeMorgan from Boolean algebra */
  def fromBool[A](implicit b: Bool[A]): DeMorgan[A]
}

Heyting

Heyting algebra (intuitionistic/constructive logic).

/**
 * Heyting algebra for intuitionistic logic
 * Has implication but may not have classical negation (excluded middle)
 */
trait Heyting[A] extends BoundedDistributiveLattice[A] {
  /** Logical AND (same as meet) */
  def and(a: A, b: A): A
  /** Meet operation */  
  def meet(a: A, b: A): A
  /** Logical OR (same as join) */
  def or(a: A, b: A): A
  /** Join operation */
  def join(a: A, b: A): A
  /** Implication operation (a → b) */
  def imp(a: A, b: A): A
  /** Pseudo-complement (¬a = a → ⊥) */
  def complement(a: A): A
  /** Exclusive OR */
  def xor(a: A, b: A): A
  /** NAND operation */
  def nand(a: A, b: A): A
  /** NOR operation */
  def nor(a: A, b: A): A
  /** XNOR operation */
  def nxor(a: A, b: A): A
}

object Heyting {
  def apply[A](implicit ev: Heyting[A]): Heyting[A] = ev
}

Usage Example:

import algebra.lattice._
import algebra.instances.all._

val heyting = Heyting[Boolean]
val conjunction = heyting.and(true, false)  // false
val disjunction = heyting.or(true, false)   // true  
val implication = heyting.imp(true, false)  // false (true → false = false)
val complement = heyting.complement(true)   // false

Boolean Algebra Structures

GenBool

Generalized Boolean algebra.

/**
 * Generalized Boolean algebra
 * Distributive lattice with bottom element and relative complement
 */
trait GenBool[A] extends DistributiveLattice[A] with BoundedJoinSemilattice[A] {
  /** Logical AND (same as meet) */
  def and(a: A, b: A): A
  /** Meet operation */
  def meet(a: A, b: A): A
  /** Logical OR (same as join) */
  def or(a: A, b: A): A
  /** Join operation */  
  def join(a: A, b: A): A
  /** Relative complement (a ∧ ¬b) */
  def without(a: A, b: A): A
  /** Exclusive OR */
  def xor(a: A, b: A): A
  /** View as Boolean ring */  
  def asBoolRing: BoolRing[A]
}

object GenBool {
  def apply[A](implicit ev: GenBool[A]): GenBool[A] = ev
}

Bool

Boolean algebra (classical logic).

/**
 * Boolean algebra for classical logic
 * Complete Boolean algebra with complement satisfying excluded middle
 */
trait Bool[A] extends Heyting[A] with GenBool[A] {
  /** Material implication (a → b ≡ ¬a ∨ b) */
  def imp(a: A, b: A): A
  /** Relative complement */
  def without(a: A, b: A): A
  /** Exclusive OR (a ⊕ b ≡ (a ∨ b) ∧ ¬(a ∧ b)) */
  def xor(a: A, b: A): A
  /** Get dual Boolean algebra */
  def dual: Bool[A]
  /** View as Boolean ring where XOR is addition and AND is multiplication */
  def asBoolRing: BoolRing[A]
}

object Bool {
  def apply[A](implicit ev: Bool[A]): Bool[A] = ev
}

Usage Example:

import algebra.lattice._
import algebra.instances.all._

val bool = Bool[Boolean]
val conjunction = bool.and(true, false)      // false
val disjunction = bool.or(true, false)       // true
val negation = bool.complement(true)         // false
val implication = bool.imp(true, false)      // false
val xor = bool.xor(true, false)             // true
val without = bool.without(true, false)      // true (true AND NOT false)

// Boolean algebra laws
val a = true
val b = false
val excludedMiddle = bool.or(a, bool.complement(a))  // true (a ∨ ¬a)
val nonContradiction = bool.and(a, bool.complement(a))  // false (a ∧ ¬a)

Conversions Between Structures

The library provides conversions between related algebraic structures:

// Convert between Boolean algebras and Boolean rings
class BoolRingFromBool[A](implicit bool: Bool[A]) extends BoolRing[A]
class BoolFromBoolRing[A](implicit ring: BoolRing[A]) extends Bool[A]

class GenBoolFromBoolRng[A](implicit rng: BoolRng[A]) extends GenBool[A]
class BoolRngFromGenBool[A](implicit genBool: GenBool[A]) extends BoolRng[A]

// Dual structures
class DualBool[A](implicit bool: Bool[A]) extends Bool[A]

Lattice Instances

Standard instances are provided for common types:

  • Boolean: Complete Boolean algebra
  • Numeric types: Min/max lattices (Int, Long, Double, etc.)
  • Collections: Set union/intersection lattices
  • Options: Lattices based on underlying type lattices
  • Tuples: Component-wise lattice operations

Usage Example:

import algebra.lattice._
import algebra.instances.all._

// Set lattice using union/intersection
val setLattice = Lattice[Set[Int]]
val set1 = Set(1, 2, 3)
val set2 = Set(2, 3, 4)
val union = setLattice.join(set1, set2)        // Set(1, 2, 3, 4)
val intersection = setLattice.meet(set1, set2)  // Set(2, 3)

// Option lattice
val optionLattice = Lattice[Option[Int]]
val some5 = Some(5)
val some3 = Some(3)
val none = None
val joined = optionLattice.join(some5, none)   // Some(5)
val met = optionLattice.meet(some5, some3)     // Some(3) (min)

This hierarchy enables both mathematical reasoning about order structures and practical applications in logic programming, constraint solving, and data analysis.