Distributive Logic

J.R.B. Cockett Department of Computer Science University of Tennessee Knoxville TN 37996-1301

October 28, 1992

Abstract

Equational logics are very good at handling algebraic theories. However, in programming languages which have branch instructions this sort of logic is ultimately inadequate. A branch instruction is a map to a coproduct and the problem with equational logics is that they cannot handle coproduct types.

This paper introduces an equational style logic which incorporates the coproduct as a fundamental component. It is proven that the logic corresponds to distributive categories, that is categories with a final object, finite products, and coproducts, in which the product distributes over the coproduct.

1 Introduction

Ode To a Lost Coproduct

In times of yore when elses dangled when case statements were new fangled and gotos little jumps did no harm the coproduct governed every branching arm.

But coproduct, coproduct where did you go when you failed to fit logics fine flow? And how did programs still flow about when lambda calculus missed you out?

The coproduct is a much underrated construction missing from most standard logics and yet fundamental to the flow of control in programs. It is surprising that even with the increased interest in appling logic to computer science that the lack of this construct has not been more sorely felt.

In almost all settings of computational interest we are interested in a coproduct which distributes over the product. In this paper I will describe “distributive logic” which is an equational style logic which has the distributing coproduct as one of its basic constructs. Mechanisms are described for translating this logic into categorical combinators (categorical notation) and for translating in the reverse direction. We shall show that these translations are consistent and give an equivalence of representations between distributive logic and distributive categories.

2 Distributive Categories

A distributive category is a category with a final object, finite products and finite coproducts such that the product distributes over the coproduct. It is well-known that the initial distributive category is (equivalent to) finite sets, Sets_{fin}. More generally, distributive categories are of some computational interest as they provide a model for acyclic code.

One way of setting up a distributive category is by introducing the final object and products together with a parameterized coproduct. This essentially says that whenever we have maps:

f_{1} : A × C ⟶ G, f_{2} : B × C ⟶ G

there is a unique map

dst_{0}(f_{1}, f_{2}) : (A + B) × C ⟶ G

such that ⟨p_{0}.b_{0}, p_{1}⟩. dst_{0}(f_{1}, f_{2}) = f_{1} and ⟨p_{0}.b_{1}, p_{1}⟩. dst_{0}(f_{1}, f_{2}) = f_{2}.

It suffices, however, to add d_{0} = dst_{0}(b_{0}, b_{1}) : (A + B) × C ⟶ (A × C) + (B × C) as inverse to the map ⟨⟨p_{0}.b_{0}, p_{1}⟩; ⟨p_{0}.b_{1}, p_{1}⟩⟩ to obtain the same result. This is the usual approach and the one we shall take in this paper in order to give a simple axiomatization of distributive categories. However, the flavor of what we intend is a parameterization.

It is worth noting in the above development that we have actually right parameterized the coproduct and, of course, we could have left parameterized the coproduct with dst_{1}. In this case the distributor d_{1} = dst_{1}(b_{0}, b_{1}) : C × (A + B) ⟶ (C × A) + (C × B) is enough to characterize the parameterization.

Of course, left parameterizing a construct implies the category is right parameterized in that construct as well. Thus, theoretically it suffices to consider a one-sided parameterization. Practically it may be advantageous to have both sides.

A distributive category can be axiomatized as follows (where the usual type constraint on composition and product and coproduct pairs is assumed):

Associativity: x.(y.z) = (x.y).z

Identity: x.i = i.x = x

Final: x.! =!

Projection: ⟨x, y⟩.p_{0} = x, ⟨x, y⟩.p_{1} = y

Product pairing: ⟨x.p_{0}, x.p_{1}⟩ = x

Embedding: b_{0}.⟨x; y⟩ = x, b_{1}.⟨x; y⟩ = y

Coproduct pairing: ⟨b_{0}.x; b_{1}.x⟩ = x

Distribution:

d_{0}.⟨⟨p_{0}.b_{0}, p_{1}⟩; ⟨p_{0}.b_{1}, p_{1}⟩⟩ = i
⟨⟨p_{0}.b_{0}, p_{1}⟩; ⟨p_{0}.b_{1}, p_{1}⟩⟩.d_{0} = i

The notation used for the maps above is what shall be called categorical combinator notation. An interesting aspect of this notation is that, as the type information is suppressed, it is polymorphic. When specialized to the distributive category setting we shall call them distributive category combinators.

The main purpose of this paper is to obtain an equivalent equational calculus together with translation mechanisms both ways. Equational notation has a considerable advantage as it eliminates the projection combinators. However, it is also impossible to express common subexpressions equationally and this makes it clumsy as a programming language if left unadorned. On the other hand, the combinator language is very expressive in this respect; but it is almost unreadable! A hybrid language would therefore be a useful compromise. The translation mechanisms which are described below make this possible.

The following are elementary results for distributive categories:

Lemma 2.1

(i) ⟨x.b_{0}, y⟩.d_{0} = ⟨x, y⟩.b_{0}

(ii) ⟨x.b_{1}, y⟩.d_{0} = ⟨x, y⟩.b_{1}

(iii) ⟨x, y⟩.d_{0} = ⟨x, i⟩.d_{0}.⟨⟨p_{0}, p_{1}.y⟩.b_{0}; ⟨p_{0}, p_{1}.y⟩.b_{1}⟩.

Free distributive categories have a terminating confluent rewriting system for their elements. Also the equality of maps in such categories is decidable.

3 Distributive Logic

A distributive theory, D = (S, F, E), consists of a set of primitive types, S, a set of function symbols, F, and a set of equations. The types of a distributive theory are generated from the primitive types. Each function symbol has a domain and a codomain in the types. The terms of a distributive theory are generated from the function symbols, F, some basic functions and the variables.

3.1 Types

To construct the theory it is first necessary to describe the types. The types, F_{+,×}(S), of a distributive theory are given by the following recursive definition which builds on the primitive types:

(i) 1 is a type,

(ii) a primitive type, s, is a type,

(iii) if s_{0} and s_{1} are types then (s_{0} × s_{1}) is a type,

(iv) if s_{0} and s_{1} are types then (s_{0} + s_{1}) is a type.

A type, s, is a product type if s = s_{0} × s_{1}. If s is not a product type then it is a sum type; explicitly it is either of the form s_{0} + s_{1} or is primitive.

3.2 Variables and variable bases

Every sum type, s, has associated with it a stock of variables:

x_{1}^{s}, x_{2}^{s}, ….

A product type does not have any associated variables but has variable bases. These are constructed as follows:

(i) () is a variable base for 1, (ii) a variable x_{i}^{s} is a variable base for its sum type s, (iii) if e_{0} and e_{1} are variable bases having no common variables for s_{0} and s_{1}, then (e_{0}, e_{1}) is a

variable base for s_{0} × s_{1}.

3.3 Terms

The function symbols, F, are indexed by pairs of types:

⟨dom, codom⟩ : F ⟶ F_{+,×}(S) × F_{+,×}(S)

and are used to build the terms. Each term has an associated type and these are given in the following recursive specification:

(i) () is a term of type 1, (ii) a variable x_{i}^{s} is a term of type s, (iii) if t_{0} and t_{1} are terms of type s_{0} and s_{1} respectively, then (t_{0}, t_{1}) is a term of type s_{0} × s_{1}, (iv) if t is a term of type s_{0} × s_{1}, then p_{0}(t) is a term of type s_{0} and p_{1}(t) is a term of type s_{1},

(v) if t is a term of sort s, then b_{0}(t) and b_{1}(t) are terms of type s + s′ and s′ + s respectively, where s′ can be any type,

(vi) if f : s_{0} ⟶ s_{1} is a function symbol and t is a term of type s_{0}, then f(t) is a term of type s_{1}, (vii) if t_{0} and t_{1} are terms of type s, t is a term of type s_{0} + s_{1}, and e_{0} and e_{1} are variable bases

for s_{0} and s_{1}, then

[ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (t)

is a term of type s. The term enclosed in square braces is called a coproduct function. Only the last term construction rule is at all unusual. The construct represents a map from a

coproduct. In the term the variables in the variable bases e_{0} and e_{1} are bound with scope the term to which they are assigned. In this respect the logic is significantly different from equational logic.

3.4 Free variables and substitution

As there are bound variables it becomes important to be clear about which variables are free and which are bound. This can be determined recursively by:

(i) vars(()) = {}

(ii) vars(x_{i}^{s}) = {x_{i}^{s}}

(iii) vars((t_{0}, t_{1})) = vars(t_{0}) ∪ vars(t_{1})

(iv) vars(p_{0}(t)) = vars(p_{1}(t)) = vars(t)

(v) vars(b_{0}(t)) = vars(b_{1}(t)) = vars(t)

(vi) vars(f(t)) = vars(t)

(vii)

vars ([ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (t)) = (vars(t_{0}) − vars(e_{0})) ∪ (vars(t_{1}) − vars(e_{1})) ∪ vars(t).

We shall loosely refer to a variable as being in a term when that variable occurs as a free variable in the term. The bound variables are invisible and can be renamed without changing the meaning of the term.

The notation σ_{e:=t′}(t) where e is a variable base for t and t′ is a term of the same type as e is a way of indicating the term obtained by substituting the variables of t by the appropriate component of t′.

While it is obvious what is meant by substitution it will be useful in the sequel to have a systematic way of discussing substitution. We therefore provide a recursive definition:

(i) σ_{e:=t′}(()) = ()

(ii) σ_{x:=t′}(x) = t′ σ_{(e_{0},e_{1}):=(t′_{0},t′_{1})}(x) = σ_{e_{0}:=t′_{0}}(x), if x ∈ e_{0} σ_{(e_{0},e_{1}):=(t′_{0},t′_{1})}(x) = σ_{e_{1}:=t′_{1}}(x), if x ∈ e_{1}

(iii) σ_{e:=t′}((t_{0}, t_{1})) = (σ_{e:=t′}(t_{0}), σ_{e:=t′}(t_{1}))

(iv) σ_{e:=t′}(f(t)) = f(σ_{e:=t′}(t)) where f is a function symbol or any of the projections or embeddings,

(v)

σ_{e:=t′}([ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (t)) = [ \begin{matrix}b_{0}(e_{0}) & ↦ & σ_{(e_{0},e):=(e_{0},t′)}(t_{0}) \\ b_{1}(e_{1}) & ↦ & σ_{(e_{1},e):=(e_{1},t′)}(t_{1}) \end{matrix} ] (σ_{e:=t′}(t)).

3.5 Abstract maps and equations

An abstract map is a pair [e ↦ t] where e is a variable base and t is a term such that the variables of e contain the free variables of t.

An equation, strictly speaking, is a pair of abstract maps:

[e_{0} ↦ t_{0}] = [e_{1} ↦ t_{1}]

where e_{0} and e_{1} are variable bases of the same type and t_{1} and t_{2} have the same type. We may always rename the variables in one of the abstract maps to make e_{0} = e_{1}. When this is done it is sensible to write the equation subscripting the equal sign with the common variable base. This gives the following notation:

t_{0} =_{e} t_{1}.

Use of this notation should not, however, be regarded as a commitment to the names of the variables but simply a convenience to avoid the above expanded form.

In proofs using equations the form of the variable base is unimportant. If the base contains no more than the free variables in the terms, then it shall be omitted as any variable base would then suffice.

3.6 Axioms and inference rules

All the equations in E are treated as axioms. In addition there are the following axioms which are always present:

Reflexivity:

t =_{e} t

Projection:

p_{0}(t_{1}, t_{2}) =_{e} t_{1}, p_{1}(t_{1}, t_{2}) =_{e} t_{2}

Product pairing:

(p_{0}(t), p_{1}(t)) = t

Embedding:

[ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (b_{0}(t)) =_{e} σ_{(e_{0},e):=(t,e)}(t_{0})

[ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (b_{1}(t)) =_{e} σ_{(e_{1},e):=(t,e)}(t_{1})

where σ_{e:=t′}(t) is substitution of the variables of e in t with the appropriate component(s) of t′.

Distributive coproduct pairing:

[ \begin{matrix}b_{0}(e_{0}) & ↦ & σ_{(z,e):=(b_{0}(e_{0}),e)}(t) \\ b_{1}(e_{1}) & ↦ & σ_{(z,e):=(b_{1}(e_{1}),e)}(t) \end{matrix} ] (z) =_{(z,e)} t.

The rules of inference are as follows: Symmetry:

\frac{[t_{1} =_{e} t_{2}]}{t_{2} =_{e} t_{1}}

Transitivity:

\frac{[t_{1} =_{e} t_{2}, t_{2} =_{e} t_{3}]}{t_{1} =_{e} t_{3}}

Substitution:

\frac{[t_{1} =_{e_{1}} t_{2}, t′_{1} =_{e_{2}} t′_{2}]}{σ_{e_{1}:=t′_{1}}(t_{1}) =_{e_{2}} σ_{e_{1}:=t′_{2}}(t_{2})}

where e_{1}, t′_{1}, and t′_{2} are of the same type and σ_{e:=t′}(t) is substitution of the variables of e in t with the appropriate component(s) of t′.

Lemma 3.1 (i)

([ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (t_{0}), t) =_{e} [ \begin{matrix}b_{0}(e_{0}) & ↦ & (t_{0}, t) \\ b_{1}(e_{1}) & ↦ & (t_{1}, t) \end{matrix} ] (t_{0})

(ii)

f([ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (t)) =_{e} [ \begin{matrix}b_{0}(e_{0}) & ↦ & f(t_{0}) \\ b_{1}(e_{1}) & ↦ & f(t_{1}) \end{matrix} ] (t)

where f is a projection, embedding, function symbol, or coproduct function.

Proof. There is only one minor difficulty in the proofs below and this arises as f, t, t_{0}, or t_{1} might contain the variable z, which is to be split for the coproduct. However, this can be circumvented by changing all occurrences of z in these maps to z′ and later substituting z for z′. Thus, we may assume that z does not occur in any of the above maps.

The first proof follows the pattern set by the second proof:

f([ \begin{matrix}b_{0}(z_{0}) & ↦ & t_{0} \\ b_{1}(z_{1}) & ↦ & t_{1} \end{matrix} ] (z))

=_{(z,e)} [ \begin{matrix}b_{0}(z_{0}) & ↦ & σ_{(z,e):=(b_{0}(z_{0}),e)}(f([ \begin{matrix}b_{0}(z_{0}) & ↦ & t_{0} \\ b_{1}(z_{1}) & ↦ & t_{1} \end{matrix} ] (z))) \\ b_{1}(z_{1}) & ↦ & σ_{(z,e):=(b_{0}(z_{0}),e)}(f([ \begin{matrix}b_{0}(z_{0}) & ↦ & t_{0} \\ b_{1}(z_{1}) & ↦ & t_{1} \end{matrix} ] (z))) \end{matrix} ] (z)

=_{(z,e)} [ \begin{matrix}b_{0}(z_{0}) & ↦ & f([ \begin{matrix}b_{0}(z_{0}) & ↦ & t_{0} \\ b_{1}(z_{1}) & ↦ & t_{1} \end{matrix} ] (b_{0}(z_{0}))) \\ b_{1}(z_{1}) & ↦ & f([ \begin{matrix}b_{0}(z_{0}) & ↦ & t_{0} \\ b_{1}(z_{1}) & ↦ & t_{1} \end{matrix} ] (b_{1}(z_{1}))) \end{matrix} ] (z)

=_{(z,e)} [ \begin{matrix}b_{0}(z_{0}) & ↦ & f(t_{0}) \\ b_{1}(z_{1}) & ↦ & f(t_{1}) \end{matrix} ] (z).
□

4 The equivalence of combinators to equational logic

In order to show that this logic is equivalent to the combinator representation of distributive categories, it is necessary to provide translation mechanisms between the two formulations. It is then necessary to show that the translations are consistent and inverse. To show that a translation is consistent it is necessary to show that equivalence expressions of the domain are taken to equivalent expressions of the codomain.

4.1 Translation to combinators

In this section we show that there is a consistent translation from distributive logic into the categorical combinators of a distributive category. To do this we must first describe the translation procedure which we shall denote by C:

(i)

C([e ↦ ()]) = !

(ii)

C([x ↦ x]) = i
C([(e_{0}, e_{1}) ↦ x]) = p_{0}.C([e_{0} ↦ x]), if x ∈ e_{0}
C([(e_{0}, e_{1}) ↦ x]) = p_{1}.C([e_{1} ↦ x]), if x ∈ e_{1}

(iii)

C([e ↦ (t_{0}, t_{1})]) = ⟨C([e ↦ t_{0}]), C([e ↦ t_{1}])⟩

(iv)

C([e ↦ p_{0}(t)]) = C([e ↦ t]).p_{0}
C([e ↦ p_{1}(t)]) = C([e ↦ t]).p_{1}

(v)

C([e ↦ b_{0}(t)]) = C([e ↦ t]).b_{0}
C([e ↦ b_{1}(t)]) = C([e ↦ t]).b_{1}

(vi)

C([e ↦ f(t)]) = C([e ↦ t]).f

(vii)

C([e ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (t)])

= ⟨C([e ↦ t]), i⟩.d_{0}.⟨C([(e_{0}, e) ↦ t_{0}]); C([(e_{1}, e) ↦ t_{1}])⟩.

We may now state the desired result:

Theorem 4.1 C gives a consistent translation from distributive logic into distributive category combinators.

The proof involves checking all the axioms and inference rules for consistency. In order to simplify notation we shall omit explicit mention of the translation function C, thus by [e ↦ t] shall be meant the translation of this into combinators.

It is useful to start the proof by proving an essential result which shows that substitution is really just composition:

Lemma 4.2 (Substitution is composition)

[e ↦ t].[e′ ↦ t′] = [e ↦ σ_{e′:=t}(t′)].

Proof. The proof works by a structural induction on the complexity of the terms. The induction works by assuming the result holds for subterms and proving that this means it holds for the whole term. Essentially the proof follows the definition of substitution:

(i) If t′ = () then the result is clear.

(ii) If t′ = x then [e ↦ σ_{e′:=t′}(x)] breaks into three subcases. The last two subcases, however, are almost identical so that we shall handle the first two:

• e′ = x in which case σ_{e′:=t}(x) = t and we have

[e ↦ t].[x ↦ x] = [e ↦ t]

which is certainly the case.

• e′ = (e_{0}, e_{1}) and t′ = (t_{0}, t_{1}) and x ∈ e_{0} in which case:

σ_{(e_{0},e_{1}):=(t_{0},t_{1})}(x) = σ_{e_{0}:=t_{0}}(x)

and

[e ↦ (t_{0}, t_{1})].[(e_{0}, e_{1}) ↦ x]
= ⟨[e ↦ t_{0}], [e ↦ t_{1}]⟩.p_{0}.[e_{0} ↦ x]
= [e ↦ t_{0}].[e_{0} ↦ x].
(iii) If t′ = (t_{0}, t_{1}) then
[e ↦ t].[e′ ↦ (t_{0}, t_{1})]
= [e ↦ t].⟨[e′ ↦ t_{0}], [e′ ↦ t_{1}]⟩
= ⟨[e ↦ t].[e′ ↦ t_{0}], [e ↦ t].[e′ ↦ t_{1}]⟩
= ⟨[e ↦ σ_{e′:=t}(t_{0})], [e ↦ σ_{e′:=t}(t_{1})]⟩
= [e ↦ σ_{e′:=t}((t_{0}, t_{1}))].

(iv) If t′ = f(t_{0}) where f is a function symbol, projection, or embedding then:

[e ↦ t].[e′ ↦ f(t_{0})]
= [e ↦ t].[e′ ↦ t′].f
= [e ↦ σ_{e′:=t}(t′)].f
= [e ↦ f(σ_{e′:=t}(t′))].

(v) If t′ is a coproduct term then we have the following:

[e ↦ t].[e′ ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (t_{2})]

= [e ↦ t].⟨[e′ ↦ t_{2}], i⟩.d_{0}.⟨[(e_{0}, e′) ↦ t_{0}]; [(e_{1}, e′) ↦ t_{1}]⟩
= ⟨[e ↦ σ_{e′:=t}(t_{2})], [e ↦ t]⟩.d_{0}.⟨[(e_{0}, e′) ↦ t_{0}]; [(e_{1}, e′) ↦ t_{1}]⟩
= ⟨[e ↦ σ_{e′:=t}(t_{2})], i⟩.d_{0}.⟨⟨p_{0}, p_{1}.[e ↦ t]⟩.[(e_{0}, e′) ↦ t_{0}]; ⟨p_{0}, p_{1}.[e ↦ t]⟩.
[(e_{1}, e′) ↦ t_{1}]⟩
= ⟨[e ↦ σ_{e′:=t}(t_{2})], i⟩.d_{0}.⟨[(e_{0}, e) ↦ (e_{0}, t)].[(e_{0}, e′) ↦ t_{0}]; [(e_{1}, e) ↦ (e_{1}, t)].
[(e_{1}, e′) ↦ t_{1}]⟩
= ⟨[e ↦ σ_{e′:=t}(t_{2})], i⟩.d_{0}.⟨[(e_{0}, e) ↦ σ_{(e_{0},e′):=(e_{0},t)}(t_{0})]; [(e_{1}, e) ↦ σ_{(e_{1},e′):=(e_{1},t)}(t_{1})]⟩
= [e ↦ σ_{e′:=t}([ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (t_{2}))].
□

This allows us to complete the proof that the translation to combinators is consistent:

Proof (4.1 continued). It is immediate that reflexivity, projection, and product pairing are all consistently translated. Similarly, the inference rules of symmetry, transitivity, and substitution (given in the above lemma) are consistently translated. The only difficulties arise with embedding and distributive pairing. The proof for the first embedding is as follows:

[e ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (b_{0}(t))]

= ⟨[e ↦ b_{0}(t)], i⟩.d_{0}.⟨[(e_{0}, e) ↦ t_{0}]; [(e_{1}, e) ↦ t_{1}]⟩
= ⟨[e ↦ t].b_{0}, i⟩.d_{0}.⟨[(e_{0}, e) ↦ t_{0}]; [(e_{1}, e) ↦ t_{1}]⟩
= ⟨[e ↦ t], i⟩.b_{0}.⟨[(e_{0}, e) ↦ t_{0}]; [(e_{1}, e) ↦ t_{1}]⟩
= ⟨[e ↦ t], i⟩.[(e_{0}, e) ↦ t_{0}]
= [e ↦ (t, e)].[(e_{0}, e) ↦ t_{0}]
= [e ↦ σ_{(e_{0},e):=(t,e)}(t_{0})].

The proof for the second embedding is similar.

The proof of the consistency of distributive pairing is as follows:

[(z, e) ↦ [ \begin{matrix}b_{0}(e_{0}) ↦ σ_{(z,e):=(b_{0}(e_{0}),e)}(t) \\ b_{1}(e_{1}) ↦ σ_{(z,e):=(b_{1}(e_{1}),e)}(t) \end{matrix} ] (z)]

= ⟨[(z, e) ↦ z], i⟩.d_{0}.⟨[(e_{0}, (z, e)) ↦ σ_{(z,e):=(b_{0}(e_{0}),e)}(t)]; [(e_{1}, (z, e)) ↦ σ_{(z,e):=(b_{1}(e_{1}),e)}(t)]⟩
= ⟨p_{0}, i⟩.d_{0}.⟨[(e_{0}, (z, e)) ↦ (b_{0}(e_{0}), e)].[(z, e) ↦ t]; [(e_{1}, (z, e)) ↦ (b_{1}(e_{1}), e)].[(z, e) ↦ t]⟩
= ⟨p_{0}, i⟩.d_{0}.⟨⟨p_{0}.b_{0}, p_{1}.p_{1}⟩; ⟨p_{0}.b_{1}, p_{1}.p_{1}⟩⟩.[(z, e) ↦ t]
= ⟨p_{0}, p_{1}⟩.[(z, e) ↦ t]
= [(z, e) ↦ t].
□

4.2 Translation from combinators

It is possible to translate in the opposite direction. We shall denote this translation L but then, as above, omit it to reduce notation. The translation process is given by following the specification of a category.

In giving the translation it is convenient to use some notational conveniences. They are:

• L(x) = [e ↦ L_{e}(x)] where e is a variable base for the domain of x,

• [e ↦ t].[e′ ↦ t′] = [e ↦ σ_{e′:=t}(t′)]

• ⟨[e ↦ t_{0}], [e′ ↦ t_{1}]⟩ = [e ↦ (t_{0}, σ_{e′:=e}(t_{1})]

• ⟨[e_{0} ↦ t_{0}]; [e_{1} ↦ t_{1}]⟩ = [ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (z).

Using this notation we have:

(i) L(x.y) = L(x).L(y) (ii) L(⟨x, y⟩) = ⟨L(x), L(y)⟩ (iii) L(⟨x; y⟩) = ⟨L(x); L(y)⟩ (iv) L(i) = [e ↦ e] where e is a variable base for the object for which i is the identity.

(v) if f is a function symbol, projection, or embedding:

L(f) = [e ↦ f(e)]

where e is a variable base for the domain of f, (vi)

L(d_{0}) = [(x, e) ↦ [ \begin{matrix}b_{0}(x_{0}) & ↦ & (x_{0}, e) \\ b_{1}(x_{1}) & ↦ & (x_{1}, e) \end{matrix} ] (x)].

Our purpose is now to prove:

Proposition 4.3 L is a consistent translation scheme from distributive category combinators to distributive logic abstract maps.

It is clearly useful to know that substitution is associative:

Lemma 4.4 (Substitution is associative)

σ_{e_{2}:=t_{1}}(σ_{e_{3}:=t_{2}}(t_{3})) = σ_{e_{3}:=σ_{e_{2}:=t_{1}}} (t_{3}).

Proof. The proof is a structural induction on the term t_{3} with a simpler structural induction on the structure of the variable base e_{2}.

Start by supposing that t_{3} = x, a variable. There are two cases to check: e_{3} = x, a straight substitution of the variable or, e_{3} = (e_{0}, e_{1}), a complex substitution. In the latter case there are two subcases depending on whether x occurs in e_{0} or e_{1}. However, these cases are similar so we may assume x occurs in e_{0}:

σ_{e_{2}:=t_{1}}(σ_{x:=t_{2}}(x))
= σ_{e_{2}:=t_{1}}(t_{2})
= σ_{x:=σ_{e_{2}:=t_{1}} (t_{2})}(x)
σ_{e_{2}:=t_{1}}(σ_{(e_{0},e_{1}):=(t_{20},t_{21})}(x)), x ∈ e_{0}
= σ_{e_{2}:=t_{1}}(σ_{e_{0}:=t_{20}}(x))
= σ_{e_{0}:=σ_{e_{2}:=t_{1}} (t_{20})}(x)
= σ_{(e_{0},e_{1}):=σ_{e_{2}:=t_{1}} ((t_{20},t_{21}))}(x).

Next we consider product pairing. First notice that for () the result is obvious. Now consider t_{3} = (t_{30}, t_{31}):

σ_{e_{2}:=t_{1}}(σ_{e_{3}:=t_{2}}((t_{30}, t_{31})))
= (σ_{e_{2}:=t_{1}}(σ_{e_{3}:=t_{2}}(t_{30})), σ_{e_{2}:=t_{1}}(σ_{e_{3}:=t_{2}}(t_{31})))
= (σ_{e_{3}:=σ_{e_{2}:=t_{1}} (t_{2})}(t_{30}), σ_{e_{3}:=σ_{e_{2}:=t_{1}} (t_{2})}(t_{31}))
= σ_{e_{3}:=σ_{e_{2}:=t_{1}} (t_{2})}((t_{30}, t_{31})).

For function symbols, projections, and embeddings we have:

σ_{e_{2}:=t_{1}}(σ_{e_{3}:=t_{2}}(f(t)))
= f(σ_{e_{2}:=t_{1}}(σ_{e_{3}:=t_{2}}(t))
= f(σ_{e_{3}:=σ_{e_{2}:=t_{1}} (t_{2})}(t)
= σ_{e_{3}:=σ_{e_{2}:=t_{1}} (t_{2})}(f(t))

Finally for coproduct functions we have:

σ_{e_{2}:=t_{1}}(σ_{e_{3}:=t_{2}}([ \begin{matrix}b_{0}(e_{0}) & ↦ t′_{0} \\ b_{1}(e_{1}) & ↦ t′_{1} \end{matrix} ] (t)))

= σ_{e_{2}:=t_{1}}([ \begin{matrix}b_{0}(e_{0}) & ↦ & σ_{(e_{0},e_{3}):=(e_{0},t_{2})}(t′_{0}) \\ b_{1}(e_{1}) & ↦ & σ_{(e_{1},e_{3}):=(e_{1},t_{2})}(t′_{1}) \end{matrix} ] (σ_{e_{3}:=t_{2}}(t)))

= [ \begin{matrix}b_{0}(e_{0}) & ↦ & σ_{(e_{0},e_{2}):=(e_{0},t_{1})}(σ_{(e_{0},e_{3}):=(e_{0},t_{2})}(t′_{0})) \\ b_{1}(e_{1}) & ↦ & σ_{(e_{1},e_{2}):=(e_{1},t_{1})}(σ_{(e_{1},e_{3}):=(e_{1},t_{2})}(t′_{1})) \end{matrix} ] (σ_{e_{2}:=t_{1}}(σ_{e_{3}:=t_{2}}(t)))

= [ \begin{matrix}b_{0}(e_{0}) & ↦ & σ_{(e_{0},e_{3}):=σ_{(e_{0},e_{2}):=(e_{0},t_{1})}((e_{0},t_{2}))}(t′_{0}) \\ b_{1}(e_{1}) & ↦ & σ_{(e_{1},e_{3}):=σ_{(e_{1},e_{2}):=(e_{1},t_{1})}((e_{1},t_{2}))}(t′_{1}) \end{matrix} ] (σ_{e_{3}:=σ_{e_{2}:=t_{1}} (t_{2})}(t))

= [ \begin{matrix}b_{0}(e_{0}) & ↦ & σ_{(e_{0},e_{3}):=(e_{0},σ_{e_{2}:=t_{1}} (t_{2}))}(t′_{0}) \\ b_{1}(e_{1}) & ↦ & σ_{(e_{1},e_{3}):=(e_{1},σ_{e_{2}:=t_{1}} (t_{2}))}(t′_{1}) \end{matrix} ] (σ_{e_{3}:=σ_{e_{2}:=t_{1}} (t_{2})}(t))

= σ_{e_{3}:=σ_{e_{2}:=t_{1}} (t_{2})}([ \begin{matrix}b_{0}(e_{0}) & ↦ t′_{0} \\ b_{1}(e_{1}) & ↦ t′_{1} \end{matrix} ] (t))

where we observed:

σ_{(e_{0},e_{3}):=σ_{(e_{0},e_{2}):=(e_{0},t_{1})}((e_{0},t_{2}))}(t′_{0}) = σ_{(e_{0},e_{3}):=(e_{0},σ_{e_{2}:=t_{1}} (t_{2}))}(t′_{0})

as e_{0} contains no variables in common with t_{1}.

□

Proof (4.3 continued). The only identities which present any difficulties are the distribution identities:

d_{0}.⟨⟨p_{0}.b_{0}, p_{1}⟩; ⟨p_{0}.b_{1}, p_{1}⟩⟩
= [(z, e) ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, e) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] (z)].[w ↦ [ \begin{matrix}b_{0}(e_{0}, e) & ↦ & (b_{0}(e_{0}), e) \\ b_{1}(e_{1}, e) & ↦ & (b_{1}(e_{1}), e) \end{matrix} ] (w)]

= [(z, e) ↦ [ \begin{matrix}b_{0}(e_{0}, e) & ↦ & (b_{0}(e_{0}), e) \\ b_{1}(e_{1}, e) & ↦ & (b_{1}(e_{1}), e) \end{matrix} ] ([ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, e) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] (z))].

Substituting b_{0}(e_{0}) and b_{1}(e_{1}) for z in the term and using distributive coproduct pairing we obtain:

= [(z, e) ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & (b_{0}(e_{0}), e) \\ b_{1}(e_{1}) & ↦ & (b_{1}(e_{1}), e) \end{matrix} ] (z)]

= [(z, e) ↦ ([ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}) \end{matrix} ] (z), e)]
= [(z, e) ↦ (z, e)].

For the second identity:

⟨⟨p_{0}.b_{0}, p_{1}⟩; ⟨p_{0}.b_{1}, p_{1}⟩⟩
= [w ↦ [ \begin{matrix}b_{0}(e_{0}, e) & ↦ & (b_{0}(e_{0}), e) \\ b_{1}(e_{1}, e) & ↦ & (b_{1}(e_{1}), e) \end{matrix} ] (w)].[(z, e) ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, e) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] (z)]

= [w ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, p_{1}([ \begin{matrix}b_{0}(e_{0}, e) & ↦ & (b_{0}(e_{0}), e) \\ b_{1}(e_{1}, e) & ↦ & (b_{1}(e_{1}), e) \end{matrix} ] (w))) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, p_{1}([ \begin{matrix}b_{0}(e_{0}, e) & ↦ & (b_{0}(e_{0}), e) \\ b_{1}(e_{1}, e) & ↦ & (b_{1}(e_{1}), e) \end{matrix} ] (w))) \end{matrix} ]

(p_{0}([ \begin{matrix}b_{0}(e_{0}, e) & ↦ & (b_{0}(e_{0}), e) \\ b_{1}(e_{1}, e) & ↦ & (b_{1}(e_{1}), e) \end{matrix} ] (w)))]

= [w ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, [ \begin{matrix}b_{0}(e_{0}, e) & ↦ & e \\ b_{1}(e_{1}, e) & ↦ & e \end{matrix} ] (w))) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, [ \begin{matrix}b_{0}(e_{0}, e) & ↦ & e \\ b_{1}(e_{1}, e) & ↦ & e \end{matrix} ] (w))) \end{matrix} ]

([ \begin{matrix}b_{0}(e_{0}, e) & ↦ & b_{0}(e_{0}) \\ b_{1}(e_{1}, e) & ↦ & b_{1}(e_{1}) \end{matrix} ] (w))]

= [w ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, e) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] ([ \begin{matrix}b_{0}(e_{0}, e) & ↦ & b_{0}(e_{0}) \\ b_{1}(e_{1}, e) & ↦ & b_{1}(e_{1}) \end{matrix} ] (w)))]

= [w ↦ [ \begin{matrix}b_{0}(e_{0}, e) & ↦ & [ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, e) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] (b_{0}(e_{0})) \\ b_{1}(e_{1}, e) & ↦ & [ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, e) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] (b_{1}(e_{1})) \end{matrix} ] (w)))]

= [w ↦ [ \begin{matrix}b_{0}(e_{0}, e) & ↦ & b_{0}(e_{0}, e) \\ b_{1}(e_{1}, e) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] (w)))]
= [w ↦ w].
□

Finally we can prove the equivalence:

Theorem 4.5 (Distributive combinator and logic equivalence) C and L gives an equivalence between distributive category combinators and distributive logic.

Proof. Let us consider C(L(x)). It suffices to show that the primitive terms and constructions are preserved over the construction:

C(L(i)) = C([e ↦ e]) = i
C(L(!)) = C([e ↦ ()]) =!
C(L(x.y)) = C(L(x).L(y)) = C(L(x)).C(L(y))
C(L(⟨x, y⟩)) = C(⟨L(x), L(y)⟩) = ⟨C(L(x)), C(L(y))⟩
C(L(f)) = C([e ↦ f(e)]) = f

for f a function symbol projection, or embedding.

The two remaining constructions require some non-trivial manipulation. Notice that the translation symbols are suppressed in line with our earlier convention.

C(L(⟨x; y⟩))
= C(⟨L(x); L(y)⟩)
= C([z ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & L_{e_{0}}(x) \\ b_{1}(e_{1}) & ↦ & L_{e_{1}}(y) \end{matrix} ] (z)])

= ⟨i, i⟩.d_{0}.⟨[(e_{0}, z) ↦ L_{e_{0}}(x)]; [(e_{1}, z) ↦ L_{e_{1}}(y)]⟩
= ⟨i, i⟩.d_{0}.⟨p_{0}.[e_{0} ↦ L_{e_{0}}(x)]; p_{0}.[e_{1} ↦ L_{e_{1}}(y)]⟩
= ⟨i, i⟩.d_{0}.⟨⟨p_{0}.b_{0}, p_{1}⟩; ⟨p_{0}.b_{0}, p_{1}⟩⟩.p − 0.⟨[e_{0} ↦ L_{e_{0}}(x)]; [e_{1} ↦ L_{e_{1}}(y)]⟩
= ⟨[e_{0} ↦ L_{e_{0}}(x)]; [e_{1} ↦ L_{e_{1}}(y)]⟩
= ⟨x; y⟩.

The last thing we need to check is the effect on d_{0}:

C(L(d_{0})) = C([(z, e) ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, e) \\ b_{0}(e_{1}) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] (z)])
= ⟨p_{0}, i⟩.d_{0}.⟨[(e_{0}, (z, e)) ↦ b_{0}(e_{0}, e)]; [(e_{1}, (z, e)) ↦ b_{1}(e_{1}, e)]⟩
= ⟨p_{0}, i⟩.d_{0}.⟨⟨p0, p_{1}.p_{1}⟩.b_{0}; ⟨p_{0}, p_{1}.p_{1}⟩.b_{1}⟩
= ⟨p_{0}, p_{1}⟩.d_{0}.⟨b_{0}; b_{1}⟩
= d_{0}.

Now consider L(C([e ↦ t])). We shall do a structural induction on t and e. For t = x and e = x we have:

L(C([x ↦ x])) = [y ↦ y]

which, up to renaming of variables, is an equivalence. For

L(C([(e_{0}, e_{1}) ↦ x])), x ∈ e_{0}
= L(p_{0}.C([e_{0} ↦ x]))
= L(p_{0}).L(C([e_{0} ↦ x]))
= [(e′_{0}, e′_{1}) ↦ e′_{0}].[e_{0} ↦ x]
= [(e′_{0}, e′_{1}) ↦ x′].

It is clear that substitution is preserved. This fact can be used to replace the recursive term construction using:

L(C([e ↦ f(e)])) = L(f) = [e′ ↦ f(e′)]

and substitution.

Obviously () is preserved. For product pairing we have:

L(C([e ↦ (t_{0}, t_{1})])) = L(⟨C([e ↦ t_{0}]), C([e ↦ t_{1}])⟩)
= L(⟨C([e ↦ t_{0}]), C([e ↦ t_{1}])⟩)
= [e′ ↦ L_{e′}(C([e ↦ t_{0}]), C([e ↦ t_{1}]))]
= [e′ ↦ σ_{e:=e′}(t_{0}, t_{1})].

Finally for coproduct functions we have:

L(C([e ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{0}(e_{1}) & ↦ & t_{1} \end{matrix} ] (z)]))

= L(⟨[e ↦ z], i⟩.d_{0}.⟨[(e_{0}, e) ↦ t_{0}]; [(e_{1}, e) ↦ t_{1}]⟩)

= [e ↦ (z, e)].[(w, e) ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, e) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] (w)].[k ↦ [ \begin{matrix}b_{0}(e_{0}, e) & ↦ & t_{0} \\ b_{1}(e_{1}, e) & ↦ & t_{1} \end{matrix} ] (k)]

= [e ↦ (z, e)].[(w, e) ↦ [ \begin{matrix}b_{0}(e_{0}, e) & ↦ & t_{0} \\ b_{1}(e_{1}, e) & ↦ & t_{1} \end{matrix} ] ([ \begin{matrix}b_{0}(e_{0}) & ↦ & b_{0}(e_{0}, e) \\ b_{1}(e_{1}) & ↦ & b_{1}(e_{1}, e) \end{matrix} ] (w))]

= [e ↦ (z, e)].[(w, e) ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (w)]

= [e ↦ [ \begin{matrix}b_{0}(e_{0}) & ↦ & t_{0} \\ b_{1}(e_{1}) & ↦ & t_{1} \end{matrix} ] (z)].

□