Causal Functions

Viewing streams this way leads us to our first definition of productive & truthful functions on streams!

Record causal (A : Type) (B : Type) : Type := mkCausal {
  f : forall n, vec A n -> vec B n;
  caused : forall n l, f n (truncate l) = truncate (f (S n) l)
}.

For historical reasons, these objects are called "causal functions", which consist of

1. A family of maps f n : vec A n -> vec B n taking A-vectors of length n to B-vectors of length n. For a causal function c and some nat m, we will call f c m the m-th component of c. The typing of these components ensures the "one-at-a-time" productivity of this family, viewed as a stream function. Vectors of length 1 yield vectors of length 1, and adding one more element to the input yields exactly one more element of output. But nothing in the type ensures that the first elmement remained the same. That's the job of the second component of the record, which consists of...
2. Proofs that the family f "commutes with truncation", as shown in the commutative diagram below. Intuitively, f n (truncate l) = truncate (f (S n) l) says that f n and f (S n) must agree on the first n elements of their input: only the final element of f (S n) can be "new".

Gluing all of these squares together, the data of a causal function is contained in the following diagram: a pair of infinitely descending chains, connected pointwise by the components of f.

To the observer trained in the arts of category theory, this may spark some recognition: vec is "just" an \(\omega\)-presheaf, and causal functions are "just" presheaf morphisms.

Now with our definition of causal functionns in hand, it's time to interpret causal functions as stream functions, i.e. turn a causal map that operates on finite prefixes of a stream into one that transforms whole streams.

To begin, we note that causal maps naturally act as functions A -> B by considering the f 1 : vec 1 -> vec 1 component as a map on singleton lists.

Definition causalApply1 {A B} (c : causal A B) (x : A) : B.
A, B: Type
c: causal A B
x: A
B
Admitted.

This should allow us to lift a causal function from A to B to a function from streams of A-s to streams of B-s. Intuitively, the process is straightforward. Given a causal function c, we will define its interpreation as a stream map interpCausal c : stream A -> stream B as the function which takes a stream SCons x s, and returns the stream SCons y s', where y is the result of using c as a function A -> B and passing x, and s' is the result of the recursive call.

This intuitive idea is translated into code below.

CoFixpoint interpCausalWrong {A B} (c : causal A B) (s : stream A) : stream B :=
  match s with
  | SCons _ x s => let y := causalApply1 c x in
                   SCons _ y (interpCausalWrong c s)
  end.

Unfortunately, as the identifier suggests, this is wrong in an important way. To understand why, consider the stream SCons x (SCons y s). The function interpCausalWrong sends this to SCons x' (SCons y' s'), with x' = causalApply1 c x and y' = causalApply1 c y. Unfolding the definition of causalApply1, this means that x' and y' are both the result of applying the first component of c.

However, we would expect the first two bits of the output be the results of applying the 2nd component of c to the length-2 vector Snoc (Snoc x Empty) y.

To fix this, we must shift our perspective. If we've processed n elements of the stream so far, We produce the n+1-st output by Snoc-ing the n+1-st input onto the prior n, applying the n+1-st component of c, and then taking the tail. This process is encoded by the function causalApplySnoc below.

Definition causalApplySnoc {A B} {n : nat} (c : causal A B) (l : vec A n) (x : A) : B :=
  match f _ _ c (S n) (Snoc _ l x) in vec _ (S n) return B with
  | Snoc _ _ y => y
  end.

We can now write interpCausal by simply accumulating elements as we see them, and kicking the whole process off with the empty stream.

CoFixpoint interpCausalAux {A B} {n : nat} (c : causal A B) (l : vec A n) (s : stream A) : stream B :=
  match s with
  | SCons _ x s => let y := causalApplySnoc c l x in
                   SCons _ y (interpCausalAux c (Snoc _ l x) s)
  end.

Definition interpCausal {A B} (c : causal A B) : stream A -> stream B :=
  fun s => interpCausalAux c (Empty _) s.

To our initual query of "which are the nice functions" stream -> stream, interpCausal provides the answer: "those which arise as interpCausal c for some causal function c".

Transducers

As it turns out, causal functions are just one formalism for capturing this class of stream maps! Another is by way of transducers, which are best thought of as stateful functions of type A -> B. More precisely, a transducer is a function that takes in an A, and produces both an output B, and a new transducer: the new state. The coinductive definition below uses a single constructor T to encode this: every transducer t : transd is of the form T f, where f : A -> B * transd is a function from an input A to pair of an output B and a new transducer to take the place of the old one.

CoInductive transd (A : Type) (B : Type): Type := 
| T : (A -> B * transd A B) -> transd A B.

Of course, nothing in the type discipline prevents us from using the same f multiple times and ignoring the output transd, so we will just have to be careful about not accidentally reusing stale states.

Because stepping the transducer requires a pattern match, we wrap this behavior in a function step : transd A B -> A -> B * (transd A B), defined below.

Definition step {A B} (t : transd A B) (x : A) : B * transd A B :=
    match t with
    | T _ _ f => f x
    end.

To get a sense of how transducers work, let's define a transducer which computes the partial sums of its input.

CoFixpoint partialSumAux (n : nat) : transd nat nat :=
  T _ _ (fun x => let y := x + n in (y, partialSumAux y)).

Definition partialSum : transd nat nat := partialSumAux 0.

This transducer accumulates a running total n of the values it's seen so far. When it gets an input x, it outputs x + n, and transitions to a new state where the running total is x + n.

With an illustative example in hand, we can start to look at ways of interpreting transducers. Unlike last time, the natural thing works! A transducer t is interpreted as the function that, when given a stream SCons x s, steps t on x, producing output y and a new transducer t', and returns the stream with y cons'd to the front of interpreting t' on the rest of the stream.

CoFixpoint interpTransd {A B} (t : transd A B) : stream A -> stream B :=
  fun s =>
    match s with
    | SCons _ x s => let (y,t') := step t x in
                     SCons _ y (interpTransd t' s)
    end.

The fact that stepping t returns a new transducer ready to handle the rest of the stream means we don't have to do any auxiliary state-passing: it's all handled by the definition of the particular t.

interpTransd provides yet another answer to the question of which functions stream A -> stream B are nice: those which arise by interpTransd t for some transducer t!

Back and Forth

As it happens, the two answers we have discussed thus far seem to actually be the same: transducers and causal functions define the same class of stream morphisms. The first step in showing this is to show that transducers and causal functions are inter-convertible: we can turn one into the other, and vice versa. Surprisingly, both directions are straightforward.

We begin by showing that transducers can be interpreted as causal functions. Given a transducer t, the components of the corresponding causal function are the functions vec A n -> vec B n which fold step t over the input vector from left to right, threading the updated state through. This is implemented in the two functions below: stepN handles the threading of the transducer through, and execN simply projects out the result.

Fixpoint stepN {A B} {n} (t : transd A B) (l : vec A n) : transd A B * vec B n :=
    match l with
    | Empty _ => (t,Empty _)
    | Snoc _ l' x => let (t',l'') := stepN t l' in
                     let (y,t'') := step t' x in
                     (t'',Snoc _ l'' y)
    end.

Definition execN {A B} (t : transd A B) : forall n, vec A n -> vec B n :=
  fun n l => snd (stepN t l).

To turn this family of components defined by execN t into a causal map, we must also prove the commuting squares which show that execN t commutes with truncation. Proving this will require a sort of "eta law" for execN called execN_snoc. In short, this says that the result of the n+1-st component of execN t is just that of the n-th, with one more step of t tacked on at the end.

Theorem execN_snoc {A B} : forall t n l x, execN t (S n) (Snoc A l x) = Snoc B (execN t n l) (let (t',_) := stepN t l in fst (step t' x)).
A, B: Type
forall (t : transd A B) (n : nat) (l : vec A n)
  (x : A),
execN t (S n) (Snoc A l x) =
Snoc B (execN t n l)
  (let (t', _) := stepN t l in fst (step t' x))
Proof.
A, B: Type
forall (t : transd A B) (n : nat) (l : vec A n)
  (x : A),
execN t (S n) (Snoc A l x) =
Snoc B (execN t n l)
  (let (t', _) := stepN t l in fst (step t' x))
  intros.
A, B: Type
t: transd A B
n: nat
l: vec A n
x: A
execN t (S n) (Snoc A l x) =
Snoc B (execN t n l)
  (let (t', _) := stepN t l in fst (step t' x))
  unfold execN.
A, B: Type
t: transd A B
n: nat
l: vec A n
x: A
snd (stepN t (Snoc A l x)) =
Snoc B (snd (stepN t l))
  (let (t', _) := stepN t l in fst (step t' x))
  cbn.
A, B: Type
t: transd A B
n: nat
l: vec A n
x: A
snd
  (let (t', l'') := stepN t l in
   let (y, t'') := step t' x in (t'', Snoc B l'' y)) =
Snoc B (snd (stepN t l))
  (let (t', _) := stepN t l in fst (step t' x))
  destruct (stepN t l).
A, B: Type
t: transd A B
n: nat
l: vec A n
x: A
t0: transd A B
v: vec B n
snd (let (y, t'') := step t0 x in (t'', Snoc B v y)) =
Snoc B (snd (t0, v)) (fst (step t0 x))
  destruct (step t0 x).
A, B: Type
t: transd A B
n: nat
l: vec A n
x: A
t0: transd A B
v: vec B n
b: B
t1: transd A B
snd (t1, Snoc B v b) =
Snoc B (snd (t0, v)) (fst (b, t1))
  cbn.
A, B: Type
t: transd A B
n: nat
l: vec A n
x: A
t0: transd A B
v: vec B n
b: B
t1: transd A B
Snoc B v b = Snoc B v b
  reflexivity.
Qed.


Theorem execN_caused {A B} (t : transd A B) : forall (n : nat) (l : vec _ (S n)),
  execN t n (truncate l) = truncate (execN t (S n) l).
A, B: Type
t: transd A B
forall (n : nat) (l : vec A (S n)),
execN t n (truncate l) = truncate (execN t (S n) l)
Proof.
A, B: Type
t: transd A B
forall (n : nat) (l : vec A (S n)),
execN t n (truncate l) = truncate (execN t (S n) l)
  intros.
A, B: Type
t: transd A B
n: nat
l: vec A (S n)
execN t n (truncate l) = truncate (execN t (S n) l)

We begin by using the dependent destruction tactic, which uses the fact that l has length at least one to refine our goal to handling the case where l is actually Snoc l a.

  dependent destruction l.
t: transd A B
l: vec A n
a: A
execN t n (truncate (Snoc A l a)) =
truncate (execN t (S n) (Snoc A l a))
  cbn.
t: transd A B
l: vec A n
a: A
execN t n l = truncate (execN t (S n) (Snoc A l a))

We then apply the execN_snoc lemma to massage the execN t (S n) (Snoc _ l a) term into a form where we can directly reduce truncate.

  rewrite execN_snoc.
t: transd A B
l: vec A n
a: A
execN t n l =
truncate
  (Snoc B (execN t n l)
     (let (t', _) := stepN t l in fst (step t' a)))

Ignoring the cruft in the second component of the snoc, we note that the RHS is of the form truncate (Snoc _ (execN t l) _), which directly reduces by one use of cbn to execN t l, as required.

  cbn.
t: transd A B
l: vec A n
a: A
execN t n l = execN t n l
  reflexivity.
Qed.

With components and proofs in hand, we can package them together to get a function transdToCausal : transd A B -> causal A B.

Definition transdToCausal {A B} (t : transd A B) : causal A B :=
  mkCausal _ _ (execN t) (execN_caused t).

Of course, we can also go backwards: causal maps define transducers. This translation works essentially the same way as the interpretation of causal functions as stream maps: we accumulate the previously-seen values, and apply the n+1-st component after n accumulated values to get the next.

CoFixpoint causalToTransdAux {A B} {n : nat} (c : causal A B) (l : vec A n) : transd A B :=
  T _ _ (fun x => 
           let y := causalApplySnoc c l x in
           (y, causalToTransdAux c (Snoc _ l x))
        ).

Definition causalToTransd {A B} (c : causal A B) : transd A B :=
  causalToTransdAux c (Empty _).

What's Left

Of course, these maps back and forth create natural proof obligations. In order to show that causal maps and transducers define the same set of stream functions, it remains to show the following:

1. The causalToTransd and transdToCausal functions are (weakly) inverses, up to suitable equivalence relations on causal A B and transd A B.
2. Equivalent causal functions and equivalent trandsucers are interpreted as equivalent stream functions: i.e. the functions interpCausal and interpTransd are congruences.

We define these equivalence relations and theorems below – I have yet to prove them.

CoInductive stream_eq {A} : stream A -> stream A -> Prop :=
| Eq_SCons : forall x s s', stream_eq s s' -> stream_eq (SCons _ x s) (SCons _ x s').

Definition causal_eq {A B} (c : causal A B) (c' : causal A B) :=
  forall n l, f _ _ c n l = f _ _ c' n l.

CoInductive transd_eq {A B} : transd A B -> transd A B -> Prop :=
| Eq_T : forall f f', (forall (x : A), (fst (f x)) = (fst (f' x)) /\ transd_eq (snd (f x)) (snd (f' x))) -> transd_eq (T _ _ f) (T _ _ f').

Theorem causalToTransdAndBack {A B} :
  forall (c : causal A B), causal_eq c (transdToCausal (causalToTransd c)).
A, B: Type
forall c : causal A B,
causal_eq c (transdToCausal (causalToTransd c))
Proof.
A, B: Type
forall c : causal A B,
causal_eq c (transdToCausal (causalToTransd c))
Admitted.

Theorem transdToCausalAndBack {A B} :
  forall (t : transd A B), transd_eq t (causalToTransd (transdToCausal t)).
A, B: Type
forall t : transd A B,
transd_eq t (causalToTransd (transdToCausal t))
Proof.
A, B: Type
forall t : transd A B,
transd_eq t (causalToTransd (transdToCausal t))
Admitted.

Theorem interpCausal_cong {A B} :
  forall (c c' : causal A B), causal_eq c c' -> forall s, stream_eq (interpCausal c s) (interpCausal c' s).
A, B: Type
forall c c' : causal A B,
causal_eq c c' ->
forall s : stream A,
stream_eq (interpCausal c s) (interpCausal c' s)
Proof.
A, B: Type
forall c c' : causal A B,
causal_eq c c' ->
forall s : stream A,
stream_eq (interpCausal c s) (interpCausal c' s)
Admitted.

Theorem interpTransd_cong {A B} :
  forall (t t' : transd A B), transd_eq t t' -> forall s, stream_eq (interpTransd t s) (interpTransd t' s).
A, B: Type
forall t t' : transd A B,
transd_eq t t' ->
forall s : stream A,
stream_eq (interpTransd t s) (interpTransd t' s)
Proof.
A, B: Type
forall t t' : transd A B,
transd_eq t t' ->
forall s : stream A,
stream_eq (interpTransd t s) (interpTransd t' s)
Admitted.

Reflections on Literate Programming in Coq

This document was written as my final project in Prof. Andrew Head's course "Live and Literate Programming" in Fall 2022. After a semester of studying literate programing, this case study left me with a few take-aways and recommendations for future designers of literate programming tools for theorem provers like Coq.

• Literate programming tools should never enforce that the code in the woven (pdf/html output) view appear in the same order as it does in the original code view. Unfortunately, Alectryon requires definition-order documents. I would much prefer something like Torii where I can weave the code together in an order that makes pedagogical sense, but does not necessarily pass the proof checker. The writing style in this document is severely hampered by the need to present everything before it appears.
• Alectryon does not permit the hiding of definition bodies. Many of the theorems and definitions that appear in this document are "standard" in the sense that they require little mathematical insight to prove or develop. Some examples include the cons and tail functions on snoc-lists, as well as the compatability theorems like cons_snoc or truncate_cons. Unfortunately, Alectryon requires that if the statements and type signatures of these theorems and definitions are to be shown in the document, then their proofs and bodies must also be shown. This is significant cruft that draws the reader away from their real task understanding the imporant theorems and definitions.
• It is very difficult to write an Alectryon document without the use of the library's custom emacs-based editing tool which allows one to fluidly change back and forth between code-primary and markdown-primary views. The philosophy of the tool is that neither view should be considered "primary", and that there is no third view that the code and markdown compile from. In practice, however, without the use of the emacs extension (or emacs altogether), the Coq format quickly becomes primary.