Library structures.DCPOSLs

Require Import LogicalRelations.
Require Import interfaces.Category.
Require Import interfaces.ConcreteCategory.
Require Import structures.Posets.
Require Import structures.DCPOs.
Require Import structures.Lattices.

Require Import PropExtensionality.
Require Import FunctionalExtensionality.
Require Import Classical.
Require Import ClassicalChoice.
Require Import ChoiceFacts.

Dcpo-lattices

A dcpo-semilattice is a set equipped independently with both the structure of a dcpo and that of a semilattice. Structures of this kind are mentioned for example in §6.2 of Abramsky and Jung's domain theory textbook, which discusses various forms of powerdomains.
For our purposes, the specific structures we combine are:
  • pointed dcpos and strict Scott-continuous functions between them, representing spaces of potentially non-terminating computations, and
  • completely distributive lattices, representing computation spaces with different kinds of nondeterministic choices.
Note that both structures involve a partial order, least element and supremum operations. In fact, every complete lattice is a dcpo, and every sup-preserving function is strict Scott-continuous. However, a dcpo-semilattice provides two distinct partial orderings of its carrier set, which may or may not have anything to do with each other.

Class DCPOLattice (L : Type) :=
  {
    dcposl_dcpo :> DCPO L;
    dcposl_sl :> CDLattice L;
    (*sup_dsup*)
  }.

Free dcpo

Before we construct the free dcpo-semilattice, we start with the free dcpo generated by a set, a standard construction which essentially consists of the discrete order extended with a bottom element. For our purposes, we will call the elements of the free dcpo "outcomes", which can either be values from the generating set or bottom element meant to denote divergence.

Variant outcome {A} := val (a : A) | div.
Arguments outcome : clear implicits.

The information ordering on outcomes allows div to be replaced by a terminating outcome.

Variant outcome_le {A} : relation (outcome A) :=
  | val_le a : outcome_le (val a) (val a)
  | div_le x : outcome_le div x.

Global Instance outcome_le_preo A :
  PreOrder (@outcome_le A).

Global Instance outcome_le_antisym A :
  Antisymmetric (outcome A) eq outcome_le.

Classically speaking, the order defined above is also a dcpo: any directed set will contain at most one of the generators, in which case it will be the supremum. If there is no generator in the set then the supremum must be div. However, it is not possible to provide a dsup operator as defined in the DCPO library without the use of classical axioms, as we would need the generator membership condition to be decidable for a set given in outcome A → Prop. Since we only use the construction above as a building block, this is not an issue.

Free semilattice

On the other side of things, the free sup-lattice generated by a set is simply its powerset, ordered under inclusion, where suprema are given by set unions. We may want to refactor the code to make this explicit somewhere, though this construction is a special case of the downset completion mechanized in lattices/Downset.v.

Free dcpo-semilattice

Per Abramsky and Jung, a dcpo-semilattice is a dcpo which provides the join operation of a semilattice. As a dcpo operator, the join must preserve directed sups in each argument. In the infinitary case of the sup-lattices we are considering, this manifests as the distributivity property
⋃i∈I · ⋁j∈Jᵢ · xi,j = ⋁f∈(∏i·Jᵢ) · ⋃i∈I · xi,f(i)
where ⋃ denotes the join operation associated with the sup-lattice and ⋁ is the directed-sup operation (the least element can be seen as the empty sup) associated with the dcpo structure. Maps between dcpo-semilattices must respect both structures and be at the time strict Scott-continuous with regards to the dcpo and sup-preserving with regards the semilattice ordering.

Module FDSL.

We will need the following choice principle to prove complete distributivity.

  Lemma choice_dep :
    DependentFunctionalChoice.

Carrier set

The free dcpo-semilattice can be defined using sets of outcomes.

  Definition omap A :=
    outcome A → Prop.

Lattice structure

The associated sup-lattice structure is induced by the set inclusion ordering, where suprema are given by set union.



DCPO structure

By contrast, the directed-complete structure is more subtle. The least element is the singleton {div}. As the computation progresses, any div outcome in the set can be replaced by a new set of outcomes. This new set of outcomes can be empty, and could itself include div if some of the computation's nondeterministic are still running. However, once div has been dropped from the set, the computation is fully terminated and can no longer be modified by further execution.

  Section DCPO.
    Context (A : Type).

The order described above can be defined as follows.

    Record le (x y : omap A) :=
      {
        le_fw a : x (val a) → y (val a);
        le_bw σ : y σ → x div ∨ x σ;
      }.

    Lemma le_div (x y : omap A) :
      le x y → y div → x div.

    Global Instance le_preo :
      PreOrder le.

    Global Instance le_antisym :
      Antisymmetric _ eq le.


Under that ordering, fully terminating computations are the maximal elements. Two computations will have an upper bound when it is possible to extend them so that they produce the same set of outcomes. Sups for sets of computations which are compatible in this way can be defined as follows.

    Section DSUP.
      Context {I} (x : I → omap A) `{Dx : !Directed x}.

      Definition dsup : omap A :=
        fun σ ⇒
          match σ with
            | val a ⇒ ∃ i, x i (val a)
            | div ⇒ ∀ i, x i div
          end.

      Lemma directed_val i j a :
        x i (val a) → x j div ∨ x j (val a).

      Lemma dsup_has_all σ :
        dsup σ → ∀ i, x i div ∨ x i σ.

      Global Instance dsup_spec :
        IsSup x dsup.
    End DSUP.

    Global Instance le_dc : DCPO (omap A) :=
      {
        lce := le;
        dsup I x Hx := dsup x;
      }.
  End DCPO.

Monad operations

TODO: we could have a proper definition of the ConcreteCategory of dcpo-semilattice and their homomorphisms and prove the full adjunction property, but for now we can start with the induced monad.

  Variant ret {A} (a : A) : omap A :=
    | ret_intro : ret a (val a).

  Variant bind {A B} (f : A → omap B) (x : omap A) : omap B :=
    | bind_div : x div → bind f x div
    | bind_val a σ : x (val a) → f a σ → bind f x σ.

  Lemma bind_ret_l {A} (x : omap A) :
    bind (@ret A) x = x.

  Lemma bind_ret_r {A B} (f : A → omap B) (a : A) :
    bind f (ret a) = f a.

  Lemma bind_bind {A B C} (g : B → omap C) (f : A → omap B) (x : omap A) :
    bind g (bind f x) = bind (fun a ⇒ bind g (f a)) x.

End FDSL.

ITree interoperability


Require Import ExtLib.Structures.Monad.
Require Import ITree.Basics.Basics.
Require Import ITree.Interp.Interp.

Section FORALL_ISSUP.
  Context {J : Type} {P : J → Type} `{Pdcpo: ∀ j, DCPO (P j)}.

  Global Instance forall_issup {I} (x : I → ∀ j, P j) (y : ∀ j, P j) :
    (∀ j, IsSup (fun i ⇒ x i j) (y j)) → IsSup x y.
End FORALL_ISSUP.

Global Instance fdsl_monad : Monad FDSL.omap :=
  {
    ret A a := FDSL.ret a;
    bind A B x f := FDSL.bind f x;
  }.

Section ITER.
  Context {I R} (f : I → FDSL.omap (I + R)).

  Definition iter_next (F : I → FDSL.omap R) : I → FDSL.omap R :=
    fun i ⇒ bind (f i) (sum_rect _ F (ret (m := FDSL.omap))).

  (* XXX while iter_next is monotonic it is actually not
    Scott-continuous in F. This means we will need the
    Cousot-Cousot style fixed point construction based on
    transfinite iteration and Kleene fixed points are not
    enough. *)

  Global Instance iter_next_mor :
    DCPO.Morphism iter_next.
  Admitted.
End ITER.

Global Instance dcpo_monaditer : MonadIter FDSL.omap :=
  fun R I (f : I → FDSL.omap (I + R)%type) ⇒
    lfp (iter_next f).