module Blog.BCO where

Basic combinatorial objects and call-by-push-value

Basic combinatorial objects were introduced by Hofstra in [1] as a means of unifying various constructions in realizability theory. In essence, they are posets equipped with a designated class of "realizable" partial endomaps maps. Examples include PCAS, ordered PCAs, but also locales and general posets. In to (ordered) PCAs, BCOs have a strong value/computation divide: the values are the elements of the poset, and the computations are the realizable maps. This is vaguely remeniscent of call-by-push-value calculi, which performs a similar stratification. This file is an exploration of this idea.

Before we proceed, lets give a formal definition of a basic combinatorial object. First, an auxillary definition: a partial function $f : A \rightharpoonup B$ between posets is stable if for every $x \leq y$ with $f y \downarrow$, $f x \downarrow$ and $f x \leq f y$. In other words, $f$ must be monnotone and the domain of definition of $f$ must be a sieve.

The data of a basic combinatorial object consists of:

A carrier set $V$
A poset $x \leadsto y$ on $V$
A subset $F \subseteq (V \rightharpoonup V)$ of strict partial endomaps

We also impose some closure conditions on $F$:

There exists some $\iota \in F$ such that $\forall x$, $\iota x \downarrow$ and $\iota(x) \leadsto x$.
For every $f, g \in F$, there exists a $h \in F$ such that for all $x$ with $g(x) \downarrow$ and $f(g(x)) \downarrow$, $h(x) \downarrow$ and $h(x) \leadsto f(g(x))$.

A useful intuition for a BCO is that it is the set of terms of some (untyped) programming language $L$, and the poset $\leadsto$ is the posetal completion of reflexive-transitive closure of some sort of small-step operational semantics. The subset $F$ should be thought of as all the partial unary functions that can be realized by terms in $L$.

From this perspective, the closure conditions on $F$ requires that there exists a realizer $\iota$ that approximates the identity function, and that there exits realizers that approximate the composition of two realizable maps. Note that the approximation is important here: applying the identity function in the lambda calculus is not a no-op from the perspective of operational semantics.

There is also a subtlety here regarding existence of realizers: should they only merely exist, or are the structure? Both options have their merits:

Note that there are many ways to implement the identity function in a programming language, each with their own reduction behavior. This suggests that we might want to use mere existence.
On the other hand, the category of BCOs has no hope of being univalent, as maps of BCOs are not monotone. This means that mere existence isn't as important. Also, mere existence is really annoying.

For these reasons, we opt to add realizers as structure.

We start with the underlying poset.

record BCO (ov of ℓv : Level) : Type (lsuc (ov ⊔ of ⊔ ℓv)) where
  field
    Val : Type ov
    _↝_ : Val → Val → Type ℓv
    ↝-refl : ∀ {x} → x ↝ x
    ↝-trans : ∀ {x y z} → x ↝ y → y ↝ z → x ↝ z
    ↝-antisym : ∀ {x y} → x ↝ y → y ↝ x → x ≡ y
    ↝-is-prop : ∀ {x y} → is-prop (x ↝ y)

On to realizable functions

  field
    Fn : Type of
    _⋆_ : Fn → Val → ↯ Val
    ⋆-reflect-↓ : ∀ (f : Fn) → ∀ {x y} → x ↝ y → ∣ (f ⋆ y) .def ∣ → ∣ (f ⋆ x) .def ∣
    ⋆-pres-↝ : ∀ (f : Fn) → ∀ {x y fx↓ fy↓} → x ↝ y → (f ⋆ x) .elt fx↓ ↝ (f ⋆ y) .elt fy↓
    ⋆-inj : ∀ (f g : Fn) → (∀ x → f ⋆ x ≡ g ⋆ x) → f ≡ g

Finally, our realizers. To make things a bit more compact, we start by defining an ordering on partial elements of Val, and extending that to an ordering on functions.

  _≼_ : ↯ Val → ↯ Val → Type _
  x ≼ y = ∀ (y↓ : ∣ y .def ∣) → Σ[ x↓ ∈ ∣ x .def ∣ ] (x .elt x↓ ↝ y .elt y↓)

  _⊩_ : (Val → ↯ Val) → (Val → ↯ Val) → Type _
  f ⊩ g = ∀ {x y} → x ↝ y → f x ≼ g y

As an aside, we note that strict maps are precisely the maps for which f ⊩ f.

Finally, we ask for the relevant realizers.

  field
    ι : Fn
    _⊗_ : Fn → Fn → Fn
    ι-⋆ : (ι ⋆_) ⊩ pure
    ⊗-⋆ : ∀ {f g : Fn} → ((f ⊗ g) ⋆_) ⊩ ((f ⋆_) <=< (g ⋆_))

Effectful BCOs

Though useful, BCOs leave a bit to be desired. The most obvious problem is the partial functions encoded directly in the definition: these are a pain to work with, and preclude realizability constructions that involve some other sort of effects beyond non-termination To fix this, we introduce the notion of an effectful bco, which essentially encodes a portion of CBPV as algebraic structure.

Once effects start coming into play, we may as well add types. Here, we have two sorts of types: value and computation. We only assert the existence of two type formers: computational function types, and a lifting Eff of value types to computation types. Unlike CBPV, we do not have a type of thunks, as there are applications in realizability where we may not have a way to encode a computation as a value.

record EBCO (ℓtv ℓtc ov ℓv oc ℓc : Level) : Type (lsuc (ℓtv ⊔ ℓtc ⊔ ov ⊔ ℓv ⊔ oc ⊔ ℓc)) where
  field
    VTp : Type ℓtv
    CTp : Type ℓtc
    _⇒_ : VTp → CTp → CTp
    Eff : VTp → CTp

Next, we introduce values and computations, indexed by their respective types.

    Val : VTp → Type ov
    Compute : CTp → Type oc

Values are a poset.

    _↝ᵛ_ : ∀ {α} → Val α → Val α → Type ℓv
    ↝ᵛ-refl : ∀ {α} {x : Val α} → x ↝ᵛ x
    ↝ᵛ-trans : ∀ {α} {x y z : Val α} → x ↝ᵛ y → y ↝ᵛ z → x ↝ᵛ z
    ↝ᵛ-antisym : ∀ {α} {x y : Val α} → x ↝ᵛ y → y ↝ᵛ x → x ≡ y
    ↝ᵛ-is-prop : ∀ {α} {x y : Val α} → is-prop (x ↝ᵛ y)

Computations are also a poset. Morally, this is encoding all of the derived relations _≼_ and _⊩_ that we defined in BCOs.

  field
    _↝ᶜ_ : ∀ {α} → Compute α → Compute α → Type ℓc
    ↝ᶜ-refl : ∀ {α} {x : Compute α} → x ↝ᶜ x
    ↝ᶜ-trans : ∀ {α} {x y z : Compute α} → x ↝ᶜ y → y ↝ᶜ z → x ↝ᶜ z
    ↝ᶜ-antisym : ∀ {α} {x y : Compute α} → x ↝ᶜ y → y ↝ᶜ x → x ≡ y
    ↝ᶜ-is-prop : ∀ {α} {x y : Compute α} → is-prop (x ↝ᶜ y)

We have 3 terms: application, lifting of values to effects, along with a bind operator that lets us apply a function to an effectful value. Note that we use a function in bind as opposed to a binding form, as we don't have binders!

  field
    _⋆_ : ∀ {α β} → Compute (α ⇒ β) → Val α → Compute β
    val : ∀ {α} → Val α → Compute (Eff α)
    bind : ∀ {α β} → Compute (Eff α) → Compute (α ⇒ β) → Compute β

We require that everything be sufficiently monotone, and that binding a value is the same thing as application.

  field
    ⋆-pres-↝
      : ∀ {α β} {f g : Compute (α ⇒ β)} {x y}
      → (f ↝ᶜ g) → x ↝ᵛ y → (f ⋆ x) ↝ᶜ (g ⋆ y)
    val-pres-↝
      : ∀ {α} {x y : Val α}
      → x ↝ᵛ y → val x ↝ᶜ val y
    bind-pres-↝
      : ∀ {α β} {x y : Compute (Eff α)} {f g : Compute (α ⇒ β)}
      → x ↝ᶜ y → f ↝ᶜ g → bind x f ↝ᶜ bind y g
    bind-val : ∀ {α β} (x : Val α) (f : Compute (α ⇒ β)) → bind (val x) f ↝ᶜ (f ⋆ x)

Finally, we ask for realizers for val, along with a realizer for monadic composition.

  field
    ι : ∀ {α} → Compute (α ⇒ Eff α)
    _⊗_ : ∀ {α β γ} → Compute (β ⇒ γ) → Compute (α ⇒ Eff β) → Compute (α ⇒ γ)
    ι-⋆ : ∀ {α} (x : Val α) → (ι ⋆ x) ↝ᶜ val x
    ⊗-⋆
      : ∀ {α β γ} {f : Compute (β ⇒ γ)} {g : Compute (α ⇒ Eff β)}
      → ∀ x → ((f ⊗ g) ⋆ x) ↝ᶜ bind (g ⋆ x) f

Earlier, we noted that we do not have general thunk types. However, we can ask for thunks as structure on a per-type basis.

module _ {tv cv ov oc ℓv ℓc} (A : EBCO tv cv ov oc ℓv ℓc) where
  open EBCO A

  record Thunkable (α : CTp) : Type (tv ⊔ ov ⊔ oc ⊔ ℓv ⊔ ℓc) where
    field
      Thunk : VTp
      thunk : Compute α → Val Thunk
      force : Val Thunk → Compute α

      thunk-↝ : ∀ {x y} → x ↝ᶜ y → thunk x ↝ᵛ thunk y
      force-↝ : ∀ {x y} → x ↝ᵛ y → force x ↝ᶜ force y
      force-thunk : ∀ x → force (thunk x) ↝ᶜ x

BCOs to EBCOs

Note that every BCO can be transformed into an EBCO by only having a single value type, and only allowing unary functions.

BCO→EBCO : ∀ {o} → BCO o o o → EBCO lzero lzero o o o o
BCO→EBCO {o = o} A = ebco where
  open BCO A

  data CTp : Type where
    _⇒_ : ⊤ → CTp → CTp
    Eff : ⊤ → CTp

  Compute : CTp → Type _
  Compute (_ ⇒ Eff _) = Fn
  Compute (_ ⇒ (_ ⇒ _)) = Lift _ ⊥
  Compute (Eff _) = ↯ Val

The poset on computations is defined via induction on types, and computes to the relations we previously used when working with BCOs. We use the same poset of values.

  _∣_↝ᶜ_ : ∀ α → Compute α → Compute α → Type o
  (α ⇒ Eff β) ∣ f ↝ᶜ g = ∀ {x y} → x ↝ y → Eff β ∣ (f ⋆ x) ↝ᶜ (g ⋆ y)
  Eff α ∣ x ↝ᶜ y = ∀ (y↓ : ∣ y .def ∣) → Σ[ x↓ ∈ ∣ x .def ∣ ] (x .elt x↓ ↝ y .elt y↓)

The final construction is more-or-less just putting data back together.

  ebco : EBCO _ _ _ _ _ _
  ebco .EBCO.VTp = ⊤
  ebco .EBCO.CTp = CTp
  ebco .EBCO._⇒_ = _⇒_
  ebco .EBCO.Eff = Eff
  ebco .EBCO.Val _ = Val

The proofs that we have a pair of preorders are pretty ugly, so we hide them from the innocent reader.

  ebco .EBCO._↝ᵛ_ = _↝_
  ebco .EBCO.↝ᵛ-refl = ↝-refl
  ebco .EBCO.↝ᵛ-trans = ↝-trans
  ebco .EBCO.↝ᵛ-antisym = ↝-antisym
  ebco .EBCO.↝ᵛ-is-prop = ↝-is-prop
  ebco .EBCO.Compute = Compute
  ebco .EBCO._↝ᶜ_ {α = α} x y = α ∣ x ↝ᶜ y
  ebco .EBCO.↝ᶜ-refl {α = α ⇒ Eff β} {f} x↝y fy↓ =
    ⋆-reflect-↓ f x↝y fy↓ , ⋆-pres-↝ f x↝y
  ebco .EBCO.↝ᶜ-refl {α = Eff α} x↓ = x↓ , ↝-refl
  ebco .EBCO.↝ᶜ-trans {α = α ⇒ Eff β} p q x↝y hy↓ =
    p x↝y (q ↝-refl hy↓ .fst) .fst , ↝-trans (p x↝y (q ↝-refl hy↓ .fst) .snd) (q ↝-refl hy↓ .snd)
  ebco .EBCO.↝ᶜ-trans {α = Eff α} p q z↓ =
    p (q z↓ .fst) .fst , ↝-trans (p (q z↓ .fst) .snd) (q z↓ .snd)
  ebco .EBCO.↝ᶜ-antisym {α = α ⇒ Eff β} {f} {g} p q = ⋆-inj f g λ x →
    part-ext (fst ⊙ q ↝-refl) (fst ⊙ p ↝-refl) λ fx↓ gx↓ →
    ↝-antisym
      (subst (λ fx↓ → (f ⋆ x) .elt fx↓ ↝ (g ⋆ x) .elt gx↓) prop! (p ↝-refl gx↓ .snd))
      (subst (λ gx↓ → (g ⋆ x) .elt gx↓ ↝ (f ⋆ x) .elt fx↓) prop! (q ↝-refl fx↓ .snd))
  ebco .EBCO.↝ᶜ-antisym {α = Eff α} {x} {y} p q =
    part-ext (fst ⊙ q) (fst ⊙ p) λ x↓ y↓ →
    ↝-antisym
      (subst (λ x↓ → x .elt x↓ ↝ y .elt y↓) prop! (p y↓ .snd))
      (subst (λ y↓ → y .elt y↓ ↝ x .elt x↓) prop! (q x↓ .snd))
  ebco .EBCO.↝ᶜ-is-prop {α = α ⇒ Eff β} = hlevel 1
  ebco .EBCO.↝ᶜ-is-prop {α = Eff α} = hlevel 1

The monadic structure comes from the monad of partial elements ↯.

  ebco .EBCO._⋆_ {β = Eff β} f x = f ⋆ x
  ebco .EBCO.val = pure
  ebco .EBCO.bind {β = Eff β} x f = x >>= (f ⋆_)
  ebco .EBCO.⋆-pres-↝ {β = Eff β} f↝g x↝y y↓ = f↝g x↝y y↓
  ebco .EBCO.val-pres-↝ x↝y _ = tt , x↝y
  ebco .EBCO.bind-pres-↝ {β = Eff β} x↝y f↝g (y↓ , gy↓) =
    (x↝y y↓ .fst , f↝g (x↝y y↓ .snd) gy↓ .fst) , f↝g (x↝y y↓ .snd) gy↓ .snd
  ebco .EBCO.bind-val {β = Eff β} x f y↓ = (tt , y↓) , ↝-refl

The realizers are exactly our realizers from before.

  ebco .EBCO.ι = ι
  ebco .EBCO._⊗_ {γ = Eff γ} = _⊗_
  ebco .EBCO.ι-⋆ x = ι-⋆ ↝-refl
  ebco .EBCO.⊗-⋆ {γ = Eff γ} x = ⊗-⋆ ↝-refl

References

[1] P. J. W. Hofstra, “All realizability is relative,” Math. Proc. Camb. Phil. Soc., vol. 141, no. 02, p. 239, Sep. 2006, doi: 10.1017/S0305004106009352.

TOTBWF/BCO.lagda.md

Basic combinatorial objects and call-by-push-value

Effectful BCOs

BCOs to EBCOs

References