Dealing with associativity in reduction relations

Using Coq
1

I’ve run into a problem with giving semantics to categorical programming languages.

Associativity of composition makes reduction relations icky.

A toy example to illustrate the problem (my real code uses actual typing judgments.)

The basic grammar

Inductive obj := unit | empty | prod (_ _: obj) | sum (_ _: obj).
Inductive term : sort -> sort -> Type :=
| id A: term A A
| compose {A B C}: term B C -> term A B -> term A C
| bang A: term A unit
| fanout {A B C}: term C A -> term C B -> term C (prod A B)
| fst {A B}: term (prod A B) A
| snd {A B}: term (prod A B) B
| absurd A: term empty A
| fanin {A B C}: term A C -> term B C -> term (sum A B) C
| inl {A B}: term A (sum A B)
| inr {A B}: term B (sum A B)
.
Infix "'o'" := compose (at level 30, no associativity).

You’d want to attach reduction relations like

Induction step: forall {A B}, term A B -> term A B -> Type :=
| step_id_left {A B} (f: term A B): id A o f ~> f
| step_id_right {A B} (f: term A B): f o id A ~> f

| step_fst_fanout {A B C} (f: term C A) (g: term C B): fst o fanout f g ~> f
| step_fanin_inl {A B C} (f: term A C) (g: term B C): fanin f g o inl ~> f

where "A ~> B" := (step A B).

And so on and so forth.

But there is a problem (fst o fst) o fanout x y does not reduce

I could add a rule like

| step_assoc {A B C D} (f: term C D) (g: term B C) (h: term A B): f o (g o h) ~> (f o g) o h

But that would prefer one canonical form over the other. I want to make f o (g o h) equivalent and not prefer one over the other. Also I would have to rework sum types.

I’m not quite sure what the recommended way of doing this is.
If Coq had higher inductive types one could add a loop to the AST.

| compose_assoc {A B C D} (f: term C D) (g: term B C) (h: term A B): f o (g o h) = (f o g) o h

And I feel like things would mostly just work.

But I’m not sure how to handle things rn.
You end up with some nonsense like:

| compose {A B}: tree A B -> term A B

Where tree would be something like a binary search tree thing/free path category.

And you would have various union operations combining trees together.

It just all seems very awkward in practice and I’m wondering if there is a better way for this sort of thing.

2

When working with some sort of monoid structure it can be useful to replace a binary operation with a list structure. So instead of working with:

id A : term A A
compose {A B C} : term B C -> term A B -> term A C

you would have a mutual inductive type:

Inductive term : sort -> sort -> Type :=
| ncompose : term_list A B -> term A B
| ...
with term_list : sort -> sort -> Type :=
| nil A : term_list A A
| cons A B C : term B C -> term_list A B -> term_list A C
.

Notice how the constructor ncompose takes care of both id and compose. The advantage of doing things this way is that composition has a fixed associativity. You should be able to define functions like compose later on that essentially concatenate lists. It might also be the case that id reduces definitionally a bit more than in your case, but I haven’t checked this in detail.

If you want to discuss this a bit more you can ping me (@**Ali Caglayan**) on the coq Zulip: Coq

1 Like
3

Hi @Ali I guess that’s basically the compromise I was proposing at the end.

The trouble is I’m not sure how reduction relations would work then.

Something like

| step_compose {A X Y B}: compose (A ++ [fst, fanout X Y] ++ B) ~> compose (A ++ [X] ++ B)

Just feels wrong to me.

It’s also bothersome because there’s not an obvious way to translate this to an actual evaluator that implements the semantics.

4

I’ve just realised that my suggestion doesn’t quite work by the way. The ncompose and term_list can interact badly.

Another way to do it would be to go with your original suggestion, but have a composition free syntax on the side. This would be the same without the compose clause. That way you can turn your original syntax into lists of the composition free one by “ironing out” the associativity. Then it should be possible to define the reduction operations directly on these lists, and finally there would be a “realization step” which turns the list back into your original syntax.

Something like this to start:

(* Axiom sort : Type. *)

Inductive sort := unit | empty | prod (_ _: sort) | sum (_ _: sort).
(* Inductive term : sort -> sort -> Type :=
| id A: term A A
| compose {A B C}: term B C -> term A B -> term A C
| bang A: term A unit
| fanout {A B C}: term C A -> term C B -> term C (prod A B)
| fst {A B}: term (prod A B) A
| snd {A B}: term (prod A B) B
| absurd A: term empty A
| fanin {A B C}: term A C -> term B C -> term (sum A B) C
| inl {A B}: term A (sum A B)
| inr {A B}: term B (sum A B)
.
 *)
Inductive pterm : sort -> sort -> Type :=
| pid A : pterm A A
| pbang A : pterm A unit
| pfanout {A B C} : pterm C A -> pterm C B -> pterm C (prod A B)
| pfst {A B}: pterm (prod A B) A
| psnd {A B}: pterm (prod A B) B
| pabsurd A: pterm empty A
| pfanin {A B C}: pterm A C -> pterm B C -> pterm (sum A B) C
| pinl {A B}: pterm A (sum A B)
| pinr {A B}: pterm B (sum A B)
.

Inductive term : sort -> sort -> Type :=
| compose {A B C} : term B C -> term A B -> term A C
| pterm_term {A B} : pterm A B -> term A B
.

Inductive pterm_list : sort -> sort -> Type :=
| nil {A} : pterm_list A A
| cons {A B C} : pterm B C -> pterm_list A B -> pterm_list A C
.

Fixpoint concat {A B C} (x : pterm_list B C)
  : pterm_list A B -> pterm_list A C :=
  match x with
  | nil => fun y => y
  | cons t x' => fun y => cons t (concat x' y)
  end.

Fixpoint flatten {A B} (x : term A B) : pterm_list A B :=
  match x with
  | compose u v => concat (flatten u) (flatten v)
  | pterm_term t => cons t nil
  end.
5

That ends up looking a lot like normalization by evaluation something like

Inductive val: sort -> sort -> Type :=
| halt {X}: val X X
| stuck {X A B}: term A B -> val X A -> val X B
| tuple {X A B}: val X A -> val X B -> val X (prod A B
| val_inl {X A B}: val X A -> val X (sum A B)
| val_inr {X A B}: val X A -> val X (sum A B)
.

You then define semantics as a sort of action

Definition act {Env A B}: term A B -> val Env A -> val Env B.

And then decompile back

It’s just this only solves the problem by defining as a left or right action.

I want to avoid canonicalization to one or the other association.