📝Algebraic Subtyping

Theory books recommendations:

  • Introduction to Lattices and Order by Davey and Priestley

  • Categories for the Working Mathematician by Mac Lane

  • Stone Spaces by Johnstone (mix of order and category theories)

  • Galois connections and fixed point calculus by Backhouse (Kleene algebra)

theory:

  • preorder ≤ on a set A is reflexive transitive binary relation.

  • ≡ is a kernel of preorder such that a ≡ b iff a ≤ b and b ≤ a

  • partial order is a preorder satisfying antisymmetry (if a ≤ b and b ≤ a, then a = b)

  • partial order is preorder which kernel is equivalence (=)

  • poset is a set equipped with partial order

  • if S ≤ A then upper bound of S is a of A such that s ≤ a for any s in S

  • least upper bound or join is upper bound b of S such that b ≤ a for any a = upper bound of S

  • meet is greatest lower bound

  • ⊔S - join

  • ⊔∅ = ⊥

  • ⊓S - meet

  • ⊓∅ = ⊤

  • lattice is a poset where every finite subset has a meet and join (has finite joins and meets)

  • join-semilattice is a poset that has finite joins

  • meet-semilattice is a poset that has finite meets

  • complete lattice is a poset that has arbitrary joins and meets (not necessary of finite subsets)

  • ^ same for complete semilattices