Strong Categorical Datatypes II : A term logic for categorical programming

J. Robin B. Cockett Dwight Spencer

Dept. of Computer Science Dept. of Computer Science and Engineering University of Calgary Oregon Graduate Institute

Calgary, Alberta T2N 1N4, Canada Beaverton, Oregon 97006-1999 cockett@cpsc.ucalgary.ca dwights@cse.ogi.edu

May 12, 1992

Abstract

This paper lifts the category-theoretic results of [4] to the level of an abstract language suitable for basing categorical programming language implementations. The earlier work built a fibration-based strongly-normalizing categorical combinator reduction system based entirely on functorial strength that allows the distribution of context to the interior of a strong data structure. Strong type-forming functors accompanied by (1) a collection of constructor combinators (initial datatypes) or destructor combinators (final datatypes) and (2) a capability for building new state-transforming combinators that operate with structures of the datatypes formed by these functors can be abstractly declared in a Hagino-Wraith style to form a reasonably expressive computing environment.

However, the high complexity of programming exclusively in combinators warrants the development of categorical programming languages that are isomorphic to the distributive category settings in which strong datatypes can be declared. Towards this goal, a distributive term logic is developed and proven consistent with and equivalent to the combinator theory. Due to its basis in strength higher-order operations, such as generalized map operators, are directly expressible in this first-order language. The term logic forms the underlying base of the Charity categorical programming system. The resulting categorical programming paradigm of structurally inductive state transforms is illustrated by several examples that accompany the term logic reduction rules.

1 Introduction

We recall from Part I [4] that we may build a categorical setting for strength-based, or strong, initial and final datatypes by selecting a cartesian category theory (i.e. finite products) and successively adding to it collections of special combinators for each datatype as it is adjoined to the theory. The adjoining is accomplished by declaration; the two declarative formats are shown below with Charity [3] code. They portray the factorizer versions of the Hagino “right” and “left” forms of datatype declaration [5] done in a style similar to that suggested by Wraith [12]. Wraith’s style allows translation of the resulting category theory into the polymorphic lambda calculus and thereby allowing the theory to inherit the calculus’ strong normalization property.

data C ⟶ R(A) =  data L(A) ⟶ C =
d_{1} : C ⟶ E_{1}(A, C)  c_{1} : E_{1}(A, C) ⟶ C
…  …
d_{n} : C ⟶ E_{n}(A, C).  c_{n} : E_{n}(A, C) ⟶ C.

The “left” declaration delivers a strong initial datatype-forming endofunctor L in which L(A) is a datatype of structures whose basic, or structurally internal, data are elements of the parameter type A. L is strong because it arrives paired with a parametrized combinator (natural transformation) called a strength

θ_{A,X}^{L} : L(A) × X ⟶ L(A × X)

that distributes the environment or context X throughout the data structure L(A). This allows the context to be accessible for processing by actions on basic data in the structure. The labels “c_{i}” refer to combinators, termed constructors,

c_{i} : E_{i}(A, L(A)) ⟶ L(A)

that are canonical embeddings which build the data structure L(A) from its component structures E_{i}(A, L(A)). In fact, L(A) is the categorical coproduct of the E_{i}(A, L(A)) via the c_{i}.

The “left” declaration code itself asserts that any map from the new type L(A) to a state or result type C is to be determined uniquely by a set of n parametric programmer-chosen maps or state-transformers from E_{i}(A, C) to C. That is, a new combinator that operates on L(A) data structures, called a fold factorizer and denoted fold^{L}, becomes available simply by specifying a collection of n state transformers that employ only the theory generated by earlier declarations.

Analogously, the “right” declaration format acts dually to also provide a type-forming functor possessing a strength. In this case, a set of canonical destructors d_{i} : R(A) ⟶ E_{i}(A, L(A)), by which R(A) is the categorical product of the E_{i}(A, L(A)), is spawned. A destructor d_{i} essentially projects the i-th “field” of a right data structure having type R(A). The declaration also allows building new combinators that produce R(A) data structures from a state or input type C. Such an R data structure-producing combinator is called an unfold factorizer and denoted unfold^{R}. Each unfold factorizer is built by specifying a collection of n parametric programmer-chosen state de-transformers from C to E_{i}(A, C).

The labels c_{i} and d_{i} name only the canonical operations and should not be confused with the programmer-chosen maps. These constructors and destructors are universally associated with their respective datatypes and in one-to-one correspondence with the programmer-chosen maps used for building each factorizer. By this discussion it is now clear that the “right” definition declares a final datatype and the “left” an initial datatype.

The chosen parameter type variable A usually ranges over a power of a given parameter datatype category A. However, we shall take the interpretation that it simply ranges over some category and assume the typing E_{i} : A × C ⟶ C where C serves as an approporiate category of state types.

The strong initial and final datatypes were required in Part I to satisfy respectively universal strong initiality diagrams

[figure: E_{i}(A, L(A)) × X; c_{i} × id_{X}; L(A) × X; ⟨θ_{2}^{E_{i}}, p_{1}⟩; E_{i}(A, L(A) × X) × X; fold^{L}{hs}; E_{i}(A, fold^{L}{hs}) × id_{X}; E_{i}(A, C) × X; h_{i}; C]

and universal strong finality diagrams

[figure: C × X; ⟨g_{i}, p_{1}⟩; E_{i}(A, C) × X; θ_{2}^{E_{i}}; unfold^{R}{gs}; E_{i}(A, C × X); E_{i}(A, unfold^{R}{gs}); R(A); d_{i}; E_{i}(A, R(A))]

from which rewrite rules for the fold and unfold factorizers were directly derived.

Additional specializations of these factorizers were also defined to provide a reasonable combinator tool-kit for programming. The case factorizer case^{L} carries out a single operation on an initial data structure to produce a state. The record factorizer record^{R} does a single operation on a state to produce a final data structure. The map factorizers map^{L} and map^{R}, respectively for initial and final datatypes, perform the same operation on each basic datum of a data structure while being recursively driven by that same structure. Thus the special factorizers operate in the same way as the familiar like-named functions used in conventional functional programming systems.

With the assumptions that an initial datatype declaration provides for n constructors that build structures of a datatype L(A) of parametric arity m, the set of generated rewriting rules that are selected to augment the previously declared theory become:

c_{i} × id_{X} ; fold^{L}{h_{1}, …, h_{n}} ⟹ ⟨map^{E_{i}}{p_{0}, fold^{L}{h_{1}, …, h_{n}}}, p_{1}⟩; h_{i}
c_{i} × id_{X}; case^{L}{h_{1}, …, h_{n}} ⟹ h_{i}
c_{i} × id_{X} ; map^{L}{f_{1}, …, f_{m}} ⟹ map^{E_{i}}{(f_{1}, …, f_{m}), map^{L}{f_{1}, …, f_{m}}}; c_{i}

Similarly, the rules brought forth for augmentation by a declaration of the datatype R(A) are:

unfold^{R}{g_{1}, …, g_{n}}; d_{i} ⟹ ⟨g_{i}, p_{1}⟩; map^{E_{i}}{p_{0}, unfold^{R}{g_{1}, …, g_{n}}}
record^{R}{g_{1}, …, g_{n}}; d_{i} ⟹ g_{i}
map^{R}{f_{1}, …, f_{m}}; d_{i} ⟹ d_{i} × id_{X} ; map^{E_{i}}{(f_{1}, …, f_{m}), map^{R}{f_{1}, …, f_{m}}}

As in the earlier paper, the combinator sequence θ^{F} ; F (f_{1}, …, f_{k}) is represented as the combinator map^{F} {f_{1}, …, f_{k}} for any strong functor F. The collections {h_{i}} and {g_{i}} represent the programmer-chosen maps that respectively parameterize the fold^{L} and unfold^{R} combinators. The collection {f_{i}} are the programmer-chosen mapping actions.

The standard set of cartesian rewriting rules combined with the new rules accumulated by any datatype declarations form a confluent and terminating polymorphic reduction system for evaluating programs that compute with the declared datatypes.

Definitions of some useful strong datatypes are given below. The less familiar ones likely warrant some explanation. The DBTree datatype permits node data and leaf data to have different structures. Colists capture all non-empty finite lists as well as the infinite lists. In fact, the cotail destructor is partial: the tail of a length-1 list does not exist. Similarly, the Cotree type contains all finite binary trees as well as infinite binary trees, and its cobranch destructor is partial. Bushes are unbounded-branching-factor tree structures.

Booleans  Natural Numbers  Finite Lists

data Bool ⟶ C = true : 1 ⟶ C false : 1 ⟶ C.

data Nat ⟶ C =
zero : 1 ⟶ C
succ : C ⟶ C.

data List(A) ⟶ C = nil : 1 ⟶ C cons : A × C ⟶ C.

Finite Binary Trees  Infinite Binary Trees  Infinite Lists

data Btree(A) ⟶ C = bleaf : A ⟶ C bnode : C × C ⟶ C.

data DBTree(A, B) ⟶ C = dbleaf : A ⟶ C dbnode : B × (C × C) ⟶ C. data C ⟶ Inftree(A) =

root : C ⟶ A

branch : C ⟶ (C × C).

data C ⟶ Cotree(A, B) = coroot : C ⟶ A cobranch : C ⟶ 1 + (C × C). data C ⟶ Inflist(A) =

head : C ⟶ A tail : C ⟶ C.

data C ⟶ Colist(A) = cohead : C ⟶ A cotail : C ⟶ 1 + C.

Finite Products  Finite Sums  Bushes
data C → Nprod(A_{1}, …, A_{n}) =
field1 : C ⟶ A_{1}

… fieldn : C ⟶ A_{n}.

data Nsum(A_{1}, …, A_{n}) → C =
tag1 : A_{1} ⟶ C

… tagn : A_{n} ⟶ C. data Bush(A, B) ⟶ C =

fruit : A → C

fork : B × (List(C) × List(C)) → C.

data C ⟶ InfBush(A, B) = limb : C → A + B × (List(C) × List(C)).

An infinitude of type-instantiations and hybrids of these datatypes are evidently available. For example, data structures similar to

data C ⟶ Syntaxtree(Binding, Token) =

phraselook : C ⟶ Binding × (Token × (C + list(C))).

have been employed as abstract syntax trees for language compilation.

A prototypical, yet versatile, categorical programming language (term logic) for all such strong datatypes whose computation semantic is isomorphic to these combinator rules is built in Section 2. It is intended to be an abstract language over which categorically-based functional languages supporting strong datatypes may be designed. In fact, one such language implementation — Charity — is currently an operational testbed for categorical programming using mixtures of eager initial and lazy final datatypes (Cockett and Fukushima [3]). The functional completeness and correctness of the term logic is exhibited in Section 3 as an equivalence between it and a cartesian category theory closed under the adjoining of strong datatypes. The equivalence is expressed as a pair of translations going in opposite directions. The categorical programming paradigm brought forth by the term logic is demonstrated by coding examples in Section 4.

2 Term Logic

Coding solely with categorical combinators is an intimidating and unintuitive style of programming. In this sense, raw combinators are an overly detailed mode of categorical computation. This section presents a higher-level programming language in the form of a term logic that eliminates the plenitude of projections occurring within combinator expressions. These projections appear naturally because of the distributivity properties of our categorical setting. In particular, the projections perform the distribution of the environment, or context, in this strong setting. The term logic will be shown to correspond exactly to these basic distributive structures.

We proceed by augmenting a “seed” cartesian theory that corresponds to a cartesian category, i.e. one possessing finite products, with terms and rules that reflect the new processing available by the addition of a finite sequence of strong datatypes to the original cartesian category. Our construction generalizes the term logic development presented for predistributive categories in Cockett [1].

The definition of the term logic is motivated by considering how programs in the logic should be translated or compiled into categorical combinators. The overall picture that will be arise from the forthcoming definitions is to treat a program t with context v as the unit of translation and represent it as a special binding operator

{v ↦ t}

called a closed abstract map where t is a term and v is a variable-binding expression — a variable base — containing all the free variables of t. This form permits the binding of variables in t for substitution by the component variables of the variable base whenever the program is applied to a term t′ having the same type as that possessed by the base.

2.1 The Cartesian Theory

The familiar manipulation of data built from products is generalized here to introduce the term notation and to provide a precise foundation for adding later some strong datatypes to a cartesian logic.

A specification of a cartesian theory, D_{0} = (T_{0}, F_{0}, S_{0}, E_{0}), consists of a set T_{0} of primitive types, a set F_{0} of function symbols, a signature S_{0} for the function symbols, and a set E_{0} of equations between programs with like-typed contexts. The signature is a map

S_{0} : F_{0} → T_{0} × T_{0} .

that provides, via projections, the domain and codomain primitive types for each function symbol. Using the sets of rules below, the full cartesian theory can be generated.

Types:

The collection of types for the cartesian theory is defined inductively starting from the primitive types:

(i) If τ ∈ T_{0} then τ is a type. (ii) 1 is a type. (iii) If τ_{0} and τ_{1} are types then τ_{0} × τ_{1} is a type.

Variables and Variable Bases: With every type τ there is assumed to be a countable collection of variables:

v_{τ} , v_{τ}^{(1)}, v_{τ}^{(2)}, v_{τ}^{(3)}, …, v_{τ}^{i} , …

For clarity the superscripting will often be omitted and the typing abbreviated, with both being inferable from discussion context. For example, v_{i} will typically mean v_{τ_{i}} for some assumed indexed collection of types {τ_{i}}. In addition to isolated variables, variable bases are specially provided as a well-needed programming convenience to carry out two oft-desired tasks: (1) to bind more than one distinct variable at one time within a single expression and (2) to provide direct binding access (i.e. avoid use of projections) to component data of a structure having a product datatype. These tasks are often combined and treated as the problem of pattern matching bound variables to an operand in a function application. Variable bases with their type associations are defined as follows:

(i) () is variable base of type 1. (ii) A variable v_{τ}^{i} is a variable base for its type τ. (iii) If v_{τ_{0}} and v_{τ_{1}} are variable bases for τ_{0} and τ_{1}, respectively, having no variables in common then

(v_{τ_{0}}, v_{τ_{1}}) is a variable base for τ_{0} × τ_{1}.

A variable base is also said to have the type for which it is a base.

Terms:

The variables, function symbols, and all projections of all product types producible in the theory are available for building terms. The signature mapping is assumed to be extended inductively to encompass all term and type constructions. The inductive definition of terms and their associated types are given below:

(i) Singleton Term: () is a term of type 1. (ii) Variable Term: A variable v_{τ} is a term of type τ. (iii) Pair Term: If t_{0} and t_{1} are terms of type τ_{0} and τ_{1}, respectively, then (t_{0}, t_{1}) is a term of type

τ_{0} × τ_{1}. (iv) Projection Terms: If t is a term of the product type τ_{0} × τ_{1} then p_{0}(t) is a first projection term of

type τ_{0} and p_{1}(t) is a second projection term of type τ_{1}, where the symbols p_{0} and p_{1} are added to the collection of function symbols and are given the signatures of the projections associated with τ_{0} × τ_{1}.

(v) Function Terms: If f is any non-projection function symbol with domain of type τ and codomain of type τ′, and t is a term of type τ, then f(t) is a term of type τ′.

(vi) Application Terms: If t is a term of type τ, t′ a term of type τ′, and v a variable base of type τ′ then the abstract map t applied to t′, i.e.

{v ↦ t}(t′)

is a term of type τ. The term t is referred to as an abstracted term.

Some cautionary words are appropriate here. An abstract map is not a term by itself because it cannot be evaluated. Its strong suggestion as a map or function should be tempered by the fact that maps and functions are not values in the first-order logic we will develop. Also, an abstract map need not necessarily be closed. A closed abstract map is called a program. Secondly, variable bases are not terms as well. Nevertheless, we will employ identical notation for both a variable base within an abstracted term and the term formed from the same variables under the same sequence of pairings. For example, ((v_{1}, (v_{2}, (v_{3}, v_{4}))), v_{5}) is usable as either a (non-term) variable base or as a term built from variables. The usage will be clear from the expression context. Also, the occurences of pairs in expressions will frequently be abbreviated by omitting the outermost parentheses: e.g f((a, b)) becomes f(a, b).

Free Variables: Since we have pronounced a binding operator, viz. the abstract map, free and bound variables are consequently definable. The free variables of terms are determined inductively by the rules below.

(i) fvars(()) = ∅. (ii) If v is a variable, then fvars(v) = {v}. (iii) fvars(t_{0}, t_{1}) = fvars(t_{0}) ∪ fvars(t_{1}). (iv) If f is any function symbol (including any amended projections), then fvars(f(t)) = fvars(t).

(v) fvars({v ↦ t}(t′)) = fvars(t′) ∪ (fvars(t) − fvars(v)).

If an abstract map expression {v ↦ t′} occurs in a term t, the occurrence of a free variable in t′ that occurs also in v is said to be bound in t′ or local in t′. Clearly the determination of bound-ness can be carried on throughout all variable occurrences of t. A variable occurrence not judged bound is said to be unbound or global. It is easy to show that the collection of unbound variables of a term within the empty context forms its set of free variables. The reader should note that our brevity causes v in rule (v) to be treated on the left side as a variable base and on the right as a term. We shall conventionally refer to a variable as being in a term when that variable occurs freely in the term. Bound variables will be treated as invisible variables that can be renamed without changing the semantics of the term. We hereafter assume, again for brevity, that all variables in a concerned expression have been previously determined to be either bound or unbound.

Substitution: With the definitions of terms and free variables, we can inductively define the meaning of applying a simultaneous substitution σ to a term t′. More precisely, writing

σ_{v:=t}(t′)

where v is a variable base for the type of the term t, means that the component variables of v be pattern-matched with the appropriate component values of t and then substituted simultaneously into like-named free variables of t′. The result has its type equal to the type of t′. The pattern-matching is performed inductively on the structure of the substitution operand by essentially invoking projections precisely according to the substitution rules below. Since variables may substituted by terms containing variables, we hereafter implicitly assume for all substitution rules that renaming is performed in parallel with the substitution. The renaming prevents any variable clashes that would cause substituted free variables to become bound; doing it in parallel allows substitution proofs to be correctly built as structurally inductive ones (see [8]).

(i) σ_{v:=t}(()) = (). (ii) For each variable x occuring in t′, then

(1) If x does not occur in v, then σ_{v:=t}(x) = x,

(2) else if x is bound and x = v then σ_{v:=t}(x) = x,

(3) else if x is unbound and x = v then σ_{v:=t}(x) = t,

(4) else if v = (v_{τ_{0}}, v_{τ_{1}}) and x occurs in v_{τ_{i}}, then σ_{v:=t}(x) = σ_{v_{τ_{i}}:=p_{i}(t)}(x).

(iii) σ_{v:=t}(t_{0}, t_{1}) = (σ_{v:=t}(t_{0}), σ_{v:=t}(t_{1})) (iv) If f is any function symbol, then σ_{v:=t}(f(t′)) = f(σ_{v:=t}(t′))

(v) σ_{v:=t}({v′ ↦ t′}(t′′)) = {v′ ↦ σ_{v:=t}(t′)}(σ_{v:=t}(t′′))

The last sub-rule of rule (ii) is used to complete the pattern matching of the variable base v with the term t by breaking down t, if necessary, with projections to fit, type-wise, into the variables of v. Thus

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

differs substitutively from

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

due to the latter’s better-fitting pattern-match.

Axioms and Inference Rules: A set of axioms and rules are used to construct a variable-base-indexed family of equivalence relations (=_{v_{τ}}) among programs (closed abstract maps) of the general form {v_{τ} ↦ t} where v_{τ} is a variable base of type τ such that fvars(v_{τ}) ⊃ fvars(t). We say that v_{τ} is a variable base for t. The equivalences will hold up to renaming via the substitution rules above. This assumption will be implemented by the following axiom:

• Equivalence of Identities: For a fixed type τ, all programs of the form {v_{τ} ↦ v_{τ} } are equal.

With respect to all the other rules already presented and to come, this axiom can be shown as equivalent to an explicit formalization of renaming the variables of a program, as well as to extensionality properties for abstract maps and programs. This axiom also yields the surjective pairing property for programs, making the theory really “cartesian”. Nevertheless, we select this axiomization in lieu of all these alternatives to avoid distracting from the critical role of substitution in the cartesian theory and its augmentations. By virtue of its equivalence to extensionality, this axiom justifies the use of the notation

t_{0} =_{v_{τ}} t_{1}

to signify equality between any program renaming-equivalent to {v_{τ} ↦ t_{0}} and any program renaming-equivalent to {v_{τ} ↦ t_{1}} where v_{τ} is an explicit variable base for both t_{0} and t_{1}. The remaining rules for =_{v_{τ}} are as follows:

• Unit:

\frac{t is of type 1 v_{τ} is a variable base for t}{t =_{v_{τ}} ()}

• Projection:

\frac{v_{τ} is a variable base for p_{0}(t_{0}, t_{1})}{p_{0}((t_{0}, t_{1})) =_{v_{τ}} t_{0}}

\frac{v_{τ} is a variable base for p_{0}(t_{0}, t_{1})}{p_{1}(t_{0}, t_{1}) =_{v_{τ}} t_{1}}

• Application:

\frac{v_{τ} is a variable base for \{v′ ↦ t\}(t′)}{\{v′ ↦ t\}(t′) =_{v_{τ}} σ_{v′:=t′}(t)}

• Congruence:

\frac{t_{1} =_{v_{τ}} t_{2} t′_{1} =_{v′_{τ}} t′_{2} v′_{1} and v′_{2} are τ′−typed variable bases of t′_{1} and t′_{2} type(t_{1}) = τ′}{σ_{v′_{1}:=t_{1}}(t′_{1}) =_{v_{τ}} σ_{v′_{2}:=t_{2}}(t′_{2})}

We now form the equivalence relation =_{v_{τ}} for each variable base v_{τ} by letting it be the the symmetric transitive closure of this congruence relation generated by these rules.

With the eventual goal of showing an isomorphism of the cartesian theory with the standard combinator theory for a cartesian category in mind, the associative composition of categorical combinators must be reflected in the cartesian theory by the properties of substitution. The concept of composing programs can be expressed by the composition definition where the types of v_{1} and t_{0} match:

{v_{0} ↦ t_{0}}; {v_{1} ↦ t_{1}} ≡ {v_{0} ↦ σ_{v_{1}:=t_{0}}(t_{1})} .

Its well-definedness up to =_{v_{0}}-equivalence is straightforwardly derivable from the equivalence-of-identities axiom.

The requirement of associativity up to equivalence then becomes

({v_{0} ↦ t_{0}}; {v_{1} ↦ t_{1}}) ; {v_{2} ↦ t_{2}} = {v_{0} ↦ t_{0}}; ({v_{1} ↦ t_{1}}; {v_{2} ↦ t_{2}})

where substitution is now forced by the composition rule to satisfy:

σ_{v_{1}:=t_{0}}(σ_{v_{2}:=t_{1}}(t_{2})) =_{v_{0}} σ_{v_{2}:=σ_{v_{1}:=t_{0}}(t_{1})}(t_{2}) .

This requirement is fulfulled as a corollary of the following elementary substitution property of the cartesian theory:

Lemma 2.1 Associativity of Substitution:

Let t_{2} be any term whose bound variables have been fully determined by its expression context. Then

σ_{v_{1}:=t_{0}}(σ_{v_{2}:=t_{1}}(t_{2})) =_{v_{0}} σ_{v_{2}:=σ_{v_{1}:=t_{0}}(t_{1})}(t_{2})

whenever the variables of v_{2} contain the unbound variables of t_{2}.

With associativity we can also quickly derive Lemma 2.2 Simultaneity of Substitution Composition:

Let t_{2} be any term whose bound variables have been fully determined by its expression context. Then

σ_{v_{1}:=t_{0}}(σ_{v_{2}:=t_{1}}(t_{2})) =_{v_{0}} σ_{(v_{2},v_{1}):=(σ_{v_{1}:=t_{0}}(t_{1}),t_{0})}(t_{2})

whenever the variables of v_{2} contain the unbound variables of t_{2}.

In the following subsections, the cartesian theory will undergo augmentations that consist of adding new =_{v_{τ}} -relation rules. The corresponding renaming-transparent congruent equivalences are then generated as above using the enlarged =_{v_{τ}} -relations. The associativity of substitution is routinely extendable for each augmentation.

2.2 Augmenting a Theory with a Strong Initial Datatype

Expanding a theory to include a new strong initial datatype requires the addition of new term logic machinery to reason about terms of that type. This section explains the incremental aspects of adding a sequence of initial datatypes to a cartesian theory.

We will assume that the parametrized datatype L(A) being added is built using earlier-specified datatypes E_{i}, i = 1, …, n, with its components in the E_{i}(A, L(A)), and that the parametric arity of L equals m, that is, A = (A_{1}, …, A_{m}). The precise augmentation to the previously built theory is itemized below:

Types:

If τ_{1}, …, τ_{m} are types then L(τ_{1}, …, τ_{m}) is a type.

Variables and Variable Bases: L(τ_{1}, …, τ_{m}) has a countable collection {v_{L(τ_{1},...,τ_{m})}^{i}} of variables available. Because there are no mechanisms via projections or destructors to ease the general binding access to initial datatypes in the manner described earlier for product types, the collection of variable bases for the datatype L(τ_{1}, …, τ_{m}) will be constituted only with isolated variables.

Terms:

(i) If c_{1}, …, c_{n} are the constructors associated with L(τ_{1}, …, τ_{m}) then if t is a term of type E_{i}((τ_{1}, …, τ_{m}), L(τ_{1}, …, τ_{m})) then c_{i}(t) is a constructor term of type L(τ_{1}, …, τ_{m}).

(ii) If t is a term of type L(τ_{1}, …, τ_{m}), v_{i} is a variable base of type E_{i}((τ_{1}, …, τ_{m}), τ) for

i = 1, …, n and all the t_{i}, i = 1, …, n, are terms of a common type τ then

\{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (t)

is a fold-from-L term of type τ.

(iii) If t is a term of type L(τ_{1}, …, τ_{m}), v_{i} is a variable base of the component type E_{i}((τ_{1}, …, τ_{m}), L(τ_{1}, …, τ_{m})) for i = 1, …, n and all the t_{i}, i = 1, …, n, are terms of a common type τ then

\{ \begin{matrix}c_{1}(v_{1}) ↦ t_{1} \\ … \\ c_{n}(v_{n}) ↦ t_{n} \end{matrix} \} (t)

is a case-from-L term of type τ.

(iv) If t is a term of type L(τ_{1}, …, τ_{m}), w_{i} is a variable base of the parameter type τ_{i} for i = 1, …, m, and t_{i} is a term of type τ_{i}′ for i = 1, …, m, then

L[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (t)

is a map-on-L term of type L(τ_{1}′, …, τ_{m}′)

In the case/fold/map term definitions the variables in each variable base bind with scope equal only to the term assigned to the base. Each line in these three kinds of terms is called a phrase because it behaves, intuitively, as an abstract map that is “run” sequentially with respect to the others. The phrase may possibly have variables not bound by its variable base, allowing the entry of outside context into the abstracted term. Therefore phrases act as program subroutines with parameters.

Free Variables: The free variable rules are below. The definition of bound variable is extended in the expected way for each of the abstracted terms in the phrases.

(i) fvars(c_{i}(t)) = fvars(t) for i = 1, …, n

(ii)

fvars(\{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (t)) = (⋃_{i=1}^{n}(fvars(t_{i}) − fvars(v_{i}))) ∪ fvars(t)

(iii)

fvars(\{ \begin{matrix}c_{1}(v_{1}) ↦ t_{1} \\ … \\ c_{n}(v_{n}) ↦ t_{n} \end{matrix} \} (t)) = (⋃_{i=1}^{n}(fvars(t_{i}) − fvars(v_{i}))) ∪ fvars(t)

(iv)

fvars(L[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (t)) = (⋃_{i=1}^{m}(fvars(t_{i}) − fvars(w_{i}))) ∪ fvars(t)

Substitution:

(i) σ_{v:=t}(c_{i}(t′)) = c_{i}(σ_{v:=t}(t′)) for i = 1, …, n

(ii)

σ_{v:=t}(\{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (t′)) = \{| \begin{matrix}c_{1} : v_{1} ↦ σ_{v:=t}(t_{1}) \\ … \\ c_{n} : v_{n} ↦ σ_{v:=t}(t_{n}) \end{matrix} |\} (σ_{v:=t}(t′))

(iii)

σ_{v:=t}(\{ \begin{matrix}c_{1}(v_{1}) ↦ t_{1} \\ … \\ c_{n}(v_{n}) ↦ t_{n} \end{matrix} \} (t′)) = \{ \begin{matrix}c_{1}(v_{1}) ↦ σ_{v:=t}(t_{1}) \\ … \\ c_{n}(v_{n}) ↦ σ_{v:=t}(t_{n}) \end{matrix} \} (σ_{v:=t}(t′))

(iv)

σ_{v:=t}(L[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (t′)) = L[ \begin{matrix}w_{1} ↦ σ_{v:=t}(t_{1}) \\ … \\ w_{m} ↦ σ_{v:=t}(t_{m}) \end{matrix} ] (σ_{v:=t}(t′))

Axioms and Inference Rules: The =_{v} relations are amended by the rules below. Each rule is accompanied by its counterpart examples for both finite lists List(A) and database trees DBTree(A, B) as declared in the introduction’s table of datatype examples. The examples have been abstracted only on context to show clearly how the basic data (shown as a and b) of lists and database trees are processed. All variables are shown in the examples as annotations of the notation v; all other symbols are to be regarded as general terms whose only possible free variables are context variables.

(i) Fold-from-L:

\{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (c_{i}(t)) =_{v_{X}} \{v_{i} ↦ t_{i}\}(E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (w_{L}) \end{matrix} ] (t))

List(A): \{| \begin{matrix}nil : () ↦ t_{1} \\ cons : (v_{A}, v_{C}) ↦ t_{2} \end{matrix} |\} (nil()) =_{v_{X}} t_{1}

\{| \begin{matrix}nil : () ↦ t_{1} \\ cons : (v_{A}, v_{C}) ↦ t_{2} \end{matrix} |\} (cons(a, l)) =_{v_{X}} \{(v_{A}, v_{C}) ↦ t_{2}\}(a, \{| \begin{matrix}nil : () ↦ t_{1} \\ cons : (v_{A}, v_{C}) ↦ t_{2} \end{matrix} |\} (l))

DBTree(A,B):

\{| \begin{matrix}dbleaf : v_{A} ↦ t_{1} \\ dbnode : (v_{B}, (v_{C}, v′_{C})) ↦ t_{2} \end{matrix} |\} (dbleaf(a)) =_{v_{X}} \{v_{A} ↦ t_{1}\}(a)

\{| \begin{matrix}dbleaf : v_{A} ↦ t_{1} \\ dbnode : (v_{B}, (v_{C}, v′_{C})) ↦ t_{2} \end{matrix} |\} (dbnode(b, (t, t′))) =_{v_{X}} \{(v_{B}, (v_{C}, v′_{C})) ↦ t_{2}\}(b, (\{|…|\}(t), \{|…|\}(t′)))

(ii) Case-from-L:

\{ \begin{matrix}c_{1}(v_{1}) ↦ t_{1} \\ … \\ c_{n}(v_{n}) ↦ t_{n} \end{matrix} \} (c_{i}(t)) =_{v_{X}} \{v_{i} ↦ t_{i}\}(t)

List(A):

\{ \begin{matrix}nil() ↦ t_{1} \\ cons(v_{A}, v_{List(A)}) ↦ t_{2} \end{matrix} \} (nil()) =_{v_{X}} t_{1}

\{ \begin{matrix}nil() ↦ t_{1} \\ cons(v_{A}, v_{List(A)}) ↦ t_{2} \end{matrix} \} (cons(a, l)) =_{v_{X}} \{(v_{A}, v_{List(A)}) ↦ t_{2}\}(a, l)

DBTree(A,B):

\{ \begin{matrix}dbleaf(v_{A}) ↦ t_{1} \\ dbnode(v_{B}, (v_{DBTree}, v′_{DBTree})) ↦ t_{2} \end{matrix} \} (dbleaf(a)) =_{v_{X}} \{v_{A} ↦ t_{1}\}(a)

\{ \begin{matrix}dbleaf(v_{A}) ↦ t_{1} \\ dbnode(v_{B}, (v_{DBTree}, v′_{DBTree})) ↦ t_{2} \end{matrix} \} (dbnode(b, (t, t′))) =_{v_{X}} \{(v_{B}, (v_{DBTree}, v′_{DBTree})) ↦ t_{2}\}(b, (t, t′))

(iii) Map-on-L:

L[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (c_{i}(t)) =_{v_{X}} c_{i}(E_{i}[ \begin{matrix}… \\ w_{i} ↦ t_{i} \\ … \\ w_{L} ↦ L[ \begin{matrix}… \\ w_{i} ↦ t_{i} \\ … \end{matrix} ] (w_{L}) \end{matrix} ] (t))

List(A):

List [v_{A} ↦ t](nil()) =_{v_{X}} nil()
List [v_{A} ↦ t](cons(a, l)) =_{v_{X}} cons(t(a), List [v_{A} ↦ t](l))

DBTree(A,B):

DBTree[ \begin{matrix}v_{A} ↦ t_{1} \\ v_{B} ↦ t_{2} \end{matrix} ] (dbleaf(a)) =_{v_{X}} dbleaf(t_{1}(a))

DBTree[ \begin{matrix}v_{A} ↦ t_{1} \\ v_{B} ↦ t_{2} \end{matrix} ] (dbnode(b, (t, t′))) =_{v_{X}} dbnode(t_{2}(b), (DBTree[…](t), DBTree[…](t′)))

(iv) L Fold Uniqueness:

\frac{∀_{i=1}^{n} \{v_{L} ↦ t\}(c_{i}(t′)) =_{v_{X}} \{v_{i} ↦ t_{i}\}(E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{v_{L} ↦ t\}(w_{L}) \end{matrix} ] (t′))}{\{v_{L} ↦ t\}(t′′) =_{v_{X}} \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (t′′)}

List(A):

\frac{t(nil()) =_{v_{X}} t_{1} and t(cons(a, l)) =_{v_{X}} t_{2}(a, t(l))}{t(l) =_{v_{X}} \{| \begin{matrix}nil : () ↦ t_{1} \\ cons : (v_{A}, v_{C}) ↦ t_{2} \end{matrix} |\} (l)}

DBTree(A,B):

\frac{t(dbleaf(a)) =_{v_{X}} t_{1}(a) and t(dbnode(b, (t′, t′′))) =_{v_{X}} t_{2}(b, t(t′), t(t′′))}{t(t′) =_{v_{X}} \{| \begin{matrix}dbleaf : v_{A} ↦ t_{1} \\ dbnode : (v_{A}, (v_{C}, v′_{C})) ↦ t_{2} \end{matrix} |\} (t′)}

The axioms imitate exactly the corresponding rewrite rules listed in the introduction. The distribution, i.e. global scope, of context is reflected in the permitted occurrences of context variables in all phrases of the fold terms. This distribution of context will be exhibited by the strong final datatypes as well.

The reader may also compare the substitution rules and the non-recursive cases of the case and fold axioms with those of the Sum datatype shown in Cockett [1] to see more clearly the generalizations made here.

The reader may also easily verify that associativity of substitution easily extends to the augmentation.

The term logic analogy of the X-sum lemma [4] arises directly from the fold uniqueness rule:

Theorem 2.3 The terms (c_{i}(v_{i}), v_{X}) are “parametrized embedding terms” in the term logic, i.e. if there exists for each i a term t_{i} of type C such that the disjoint bases v_{i} and v_{X} together contain the free variables of t_{i} then there also exists uniquely (up to provable equality) a term t of type C such that

{v_{L} ↦ t}(c_{i}(v_{i})) =_{(v_{i},v_{X})} t_{i}

and in fact

t =_{(v_{L},v_{X})} \{ \begin{matrix}c_{1}(v_{1}) ↦ t_{1} \\ … \\ c_{n}(v_{n}) ↦ t_{n} \end{matrix} \} (v_{L})

where v_{L} does not occur in v and any t_{i}.

Proof. It is routine to verify that the expression for t in the theorem satisfies the embedding property.

For uniqueness, assume t is any term that satisfies the embedding property. The L fold uniqueness rule can be shown applicable for ”t” set to (v_{L}, t) and “t_{i}” set to

\{v_{i} ↦ (c_{i}(v_{i}), t_{i})\}(E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ (w_{L}, w_{C}) ↦ w_{L} \end{matrix} ] (v_{i}))

Thus (v_{L}, t) is uniquely determined. So by second projection and congruence, t is unique.

□

The results below show that the augmentation process could have been alternately expressed entirely in terms of the fold-from-L term. However, the separate presentation of case/fold/map terms is desirable both for clarity and for the reason that all are usefully expressive in programming.

Theorem 2.4 The case-from-L is determined by the fold-from-L:

\{ \begin{matrix}… \\ c_{i}(v_{i}) ↦ t_{i} \\ … \end{matrix} \} (v_{L}) =_{(v_{L},v_{X})} p_{1}(\{ ; | \begin{matrix}… \\ c_{i} : v_{i} ↦ \{v_{i} ↦ (c_{i}(v_{i}), t_{i})\}(E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ (w_{L}, w_{C}) ↦ w_{L} \end{matrix} ] (v_{i})) \\ … \end{matrix} | ; \} (v_{L}))

Proof. The L fold uniqueness rule is applicable where “t” is set to

(v_{L} , \{ \begin{matrix}… \\ c_{i}(v_{i}) ↦ t_{i} \\ … \end{matrix} \} (v_{L}))

and “t_{i}” to

\{v_{i} ↦ (c_{i}(v_{i}), t_{i})\}(E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ (w_{L}, w_{C}) ↦ w_{L} \end{matrix} ] (v_{i}))

□

Theorem 2.5 The map-on-L is determined by the fold-from-L:

L[ \begin{matrix}… \\ w_{j} ↦ t_{j} \\ … \end{matrix} ] (v_{L}) =_{(v_{L},v_{X})} \{ ; | \begin{matrix}… \\ c_{i} : v_{i} ↦ \{v_{i} ↦ (c_{i}(v_{i}))\}(E_{i}[ \begin{matrix}… \\ w_{j} ↦ t_{j} \\ … \\ w_{L} ↦ w_{L} \end{matrix} ] (v_{i})) \\ … \end{matrix} | ; \} (v_{L})

Proof. The L fold uniqueness rule is applicable where “t” is set to

L[ \begin{matrix}… \\ w_{j} ↦ t_{j} \\ … \end{matrix} ] (v_{L})

and “t_{i}” to

\{v_{i} ↦ (c_{i}(v_{i}))\}(E_{i}[ \begin{matrix}… \\ w_{j} ↦ t_{j} \\ … \\ w_{L} ↦ w_{L} \end{matrix} ] (v_{i}))

□

2.3 Augmenting a Theory with a Strong Final Datatype

Often computational complexity is drastically reduced by incorporating opportunities for lazy evaluation into a reduction system. This section quickly tours the process of adding strong final datatypes that parallels the development of the preceding section and discloses how the lazy evaluation of terms acting over such datatypes, e.g. infinite lists, is accomplished.

Types:

If τ_{1}, …, τ_{m} are types then R(τ_{1}, …, τ_{m}) is a type.

Variables and Variable Bases: R(τ_{1}, …, τ_{m}) has a countable collection {v_{R(τ_{1},...,τ_{m})}^{i}} of variables available.

Just as for the initial datatypes. the variable bases for the datatype R(τ_{1}, …, τ_{m}) are only the isolated variables. This is due to the subtlety in that (as will be explained) unlike ordinary product datatypes, general final data using a common set of destructors can be built either in one step or recursively. This means that the application of a destructor function to access a component of such a datum will yield different results according to how the datum was built. Consequently, easy access of “components” of final data values for binding purposes becomes problematic.

Terms:

(i) If d_{1}, …, d_{n} are the destructors associated with R(τ_{1}, …, τ_{m}) and t is a term of type R(τ_{1}, …, τ_{m}) then d_{i}(t) is a destructor term of type E_{i}((τ_{1}, …, τ_{m}), R(τ_{1}, …, τ_{m})).

(ii) If t is a term of type C, v_{C} is a variable base of type C scoped simultaneously to all the t_{i}, and each t_{i} is a term of type E_{i}((τ_{1}, …, τ_{m}), C) then

(| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t)

is an unfold-to-R term of type R(τ_{1}, …, τ_{m}).

(iii) If t is a term of type C and each t_{i} is a term of type E_{i}((τ_{1}, …, τ_{m}), R(τ_{1}, …, τ_{m})) then

( \begin{matrix}d_{1} : t_{1}(t) \\ … \\ d_{n} : t_{n}(t) \end{matrix} )

is a record-to-R term of type R(τ_{1}, …, τ_{m}).

(iv) If t is a term of type R(τ_{1}, …, τ_{m}), w_{i} is a variable base of the parameter type τ_{i} that is scoped only to the corresponding t_{i} for i = 1, …, m, and t_{i} is a term of type τ_{i}′ for i = 1, …, m, then

R[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (t)

is a map-on-R term of type R(τ_{1}′, …, τ_{m}′)

The lines in the unfold and record terms can be considered as abstract maps, possibly not closed, that act simultaneously, or concurrently, on its copy of the data entering via the common variable base v_{C}. We call each line a thread since its processing is independent of the others. This independence is evident from the reduction rules to be presented later in this section.

Free Variables:

We abbreviate the rules by showing only those for the destructors and the unfold term. The rules for the remaining record and map terms are completely analogous. The definition of bound variable is also extended over the abstracted terms of the threads.

(i) fvars((| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t)) = (⋃_{i=1}^{n} fvars(t_{i}) − fvars(v_{C})) ∪ fvars(t)

(ii) fvars(d_{i}((| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t))) = (fvars(t_{i}) − fvars(v_{C})) ∪ fvars(t)

for i = 1, …, n

Substitution:

The substitution rules involving tuples imitate closely the rules for pairs in the cartesian theory and are consequently not listed here. Thus the rules are similarly abbreviated to only the destructor and unfold term cases.

(i) σ_{v:=t}(d_{i}(t′)) = d_{i}(σ_{v:=t}(t′)) for i = 1, …, n

(ii) σ_{v:=t}((| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t′)) = (| \begin{matrix}d_{1} : σ_{v:=t}(t_{1}) \\ v_{C} ↦ … \\ d_{n} : σ_{v:=t}(t_{n}) \end{matrix} |) (σ_{v:=t}(t′))

Axioms and Inference Rules: The rules below are added to the =_{v} relations. Each rule is accompanied by its corresponding examples for the infinite lists Inflist(A) and the co-lists Colist(A) as declared in the introduction. As before for the initial datatype augmentation, the examples have been abstracted only on context to show clearly how the “seed” term, represented as c, are processed to produce infinite lists and colists.

(i) Unfold-to-R:

d_{i}((| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t)) =_{v_{X}} E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{C} ↦ (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (w_{C}) \end{matrix} ] (\{v_{C} ↦ t_{i}\}(t))

Inflist(A):

head ((| \begin{matrix}v_{C} ↦ head : t_{1} \\ tail : t_{2} \end{matrix} |) (c)) =_{v_{X}} \{v_{C} ↦ t_{1}\}(c)

tail ((| \begin{matrix}v_{C} ↦ head : t_{1} \\ tail : t_{2} \end{matrix} |) (c)) =_{v_{X}} (| \begin{matrix}v_{C} ↦ head : t_{1} \\ tail : t_{2} \end{matrix} |) (\{v_{C} ↦ t_{2}\}(c))

Colist(A):

cohead ((| \begin{matrix}v_{C} ↦ cohead : t_{1} \\ cotail : t_{2} \end{matrix} |) (c)) =_{v_{X}} \{v_{C} ↦ t_{1}\}(c)

cotail ((| \begin{matrix}v_{C} ↦ cohead : t_{1} \\ cotail : b_{0}(()) \end{matrix} |) (c)) =_{v_{X}} b_{0}(())

cotail ((| \begin{matrix}v_{C} ↦ cohead : t_{1} \\ cotail : b_{1}(t′_{2}) \end{matrix} |) (c)) =_{v_{X}} b_{1}((| \begin{matrix}v_{C} ↦ cohead : t_{1} \\ cotail : b_{1}(t′_{2}) \end{matrix} |) (\{v_{C} ↦ t′_{2}\}(c)))

(ii) Record-to-R:

d_{i}(( \begin{matrix}d_{1} : t_{1}(t) \\ … \\ d_{n} : t_{n}(t) \end{matrix} )) =_{v_{X}} \{v_{C} ↦ t_{i}\}(t)

Inflist(A):

head (( \begin{matrix}head : t_{1}(c) \\ tail : t_{2}(c) \end{matrix} )) =_{v_{X}} \{v_{C} ↦ t_{1}\}(c)

tail (( \begin{matrix}head : t_{1}(c) \\ tail : t_{2}(c) \end{matrix} )) =_{v_{X}} \{v_{C} ↦ t_{2}\}(c)

Colist(A):

cohead (( \begin{matrix}cohead : t_{1}(c) \\ cotail : t_{2}(c) \end{matrix} )) =_{v_{X}} \{v_{C} ↦ t_{1}\}(c)

cotail (( \begin{matrix}cohead : t_{1}(c) \\ cotail : b_{0}(()) \end{matrix} )) =_{v_{X}} b_{0}(())

cotail (( \begin{matrix}cohead : t_{1}(c) \\ cotail : b_{1}(t′_{2}(c)) \end{matrix} )) =_{v_{X}} b_{1}(\{v_{C} ↦ t′_{2}\}(c))

(iii) Map-on-R:

d_{i}(R[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (t)) =_{v_{X}} E_{i}[ \begin{matrix}… \\ w_{i} ↦ t_{i} \\ … \\ w_{R} ↦ R[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (w_{R}) \end{matrix} ] (d_{i}(t))

Inflist(A):

head (Inflist[v_{A} ↦ t]((| \begin{matrix}v_{C} ↦ head : t_{1} \\ tail : t_{2} \end{matrix} |) (c))) =_{v_{X}} t(t_{1}(c))

head (Inflist[v_{A} ↦ t](( \begin{matrix}head : t_{1}(c) \\ tail : t_{2}(c) \end{matrix} ))) =_{v_{X}} t(t_{1}(c))

tail (Inflist[v_{A} ↦ t]((| \begin{matrix}v_{C} ↦ head : t_{1} \\ tail : t_{2} \end{matrix} |) (c))) =_{v_{X}}

Inflist[…]((| \begin{matrix}v_{C} ↦ head : t_{1} \\ tail : t_{2} \end{matrix} |) (t_{2}(c))

tail (Inflist[v_{A} ↦ t](( \begin{matrix}head : t_{1}(c) \\ tail : t_{2}(c) \end{matrix} )) =_{v_{X}} Inflist[…](t_{2}(c)))

Colist(A):

cohead (Colist [ v_{A} ↦ t] ((| \begin{matrix}v_{C} ↦ cohead : t_{1} \\ cotail : t_{2} \end{matrix} |) (c))) =_{v_{X}} t(t_{1}(c))

cohead (Colist [ v_{A} ↦ t] (( \begin{matrix}cohead : t_{1}(c) \\ cotail : t_{2}(c) \end{matrix} ))) =_{v_{X}} t(t_{1}(c))

cotail (Colist [ v_{A} ↦ t] ((| \begin{matrix}v_{C} ↦ cohead : t_{1} \\ cotail : b_{0}(()) \end{matrix} |) (c))) =_{v_{X}} b_{0}(())

cotail (Colist [ v_{A} ↦ t] (( \begin{matrix}cohead : t_{1}(c) \\ cotail : b_{0}(()) \end{matrix} ))) =_{v_{X}} b_{0}(())

cotail (Colist [ v_{A} ↦ t] ((| \begin{matrix}v_{C} ↦ cohead : t_{1} \\ cotail : b_{1}(t′_{2}) \end{matrix} |) (c))) =_{v_{X}}

b_{1}(Colist […]((| \begin{matrix}v_{C} ↦ cohead : t_{1} \\ cotail : b_{1}(t′_{2}) \end{matrix} |) (t′_{2}(c))))

cotail (Colist [ v_{A} ↦ t] (( \begin{matrix}cohead : t_{1}(c) \\ cotail : b_{1}(t′_{2}(c)) \end{matrix} ))) =_{v_{X}} b_{1}(Colist […](t′_{2}(c))

(iv) R Unfold Uniqueness:

\frac{∀_{i=1}^{n} d_{i}(\{v_{C} ↦ t\}(t′)) =_{v_{X}} E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{C} ↦ \{v_{C} ↦ t\}(w_{C}) \end{matrix} ] (\{v_{C} ↦ t_{i}\}(t′))}{\{v_{C} ↦ t\}(t′′) =_{v_{X}} (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t′′)}

Inflist(A):

\frac{head (t(c)) =_{v_{X}} t_{1}(c) and tail (t(c)) =_{v_{X}} t(t_{2}(c))}{t(c) =_{v_{X}} (| \begin{matrix}v_{C} ↦ head : t_{1} \\ tail : t_{2} \end{matrix} |) (c)}

Colist(A):

\frac{cohead (t(c)) =_{v_{X}} t_{1}(c) and either cotail (t(c)) =_{v_{X}} b_{0}(()) or cotail (t(c)) =_{v_{X}} b_{1}(t(t′_{2}(c)))}{t(c) =_{v_{X}} (| \begin{matrix}v_{C} ↦ cohead : t_{1} \\ cotail : t_{2} \end{matrix} |) (c)}

By comparison with the axioms for initial datatypes, the opportunity for “lazy” usage of final datatypes can be intuitively inferred. In the substitution rule for the unfold-to-R, processing is essentially using the recursive mapping operation “on the outside” once to build the outermost base data of the R-structure while deferring the building of the remaining pieces of the R-structure. This allows the possible use of a destructor to extract this outermost data. On the other hand, the fold-from-L rule forces all recursion to complete before the data structure can be examined since the mapping occurs “inside” the data structure at the base data level.

As expected, most of the counterparts of the strong initial datatype properties are operative for the final strong datatypes: associativity of substitution and definability of the strong final datatype record and map terms by means of the unfold term. These results are left to the reader to be found by closely imitating the techniques used to establish the corresponding initial datatype results.

The notion analogous to X-sum (i.e. “parametrized projection terms” in the term logic) does not carry over to the strong final datatypes.

2.4 Example: parametricity

Reynolds’ abstraction theorem [7] has been specialized by Wadler [9] as a “free parametricity result” to give a more direct tool for proving program equivalences. Due to the totally parametrized development of the term logic, it is expected that the abstraction theorem holds in our setting as well. The theorem is particularized below in the style of Wadler for the case of fold-from-List terms. What is instructive is the apparent need for structural induction in its proof, an indication that such instantiations of the abstraction theorem are not really “free”. The general necessity for structural induction in proving parametric theorems was first pointed out by Mairson [6].

Theorem 2.6 Fold-from-List Parametricity

Suppose for datatypes A, A′, B, and B′ that t_{A′}, t_{B′}, u_{B}, u_{B′}, s_{B}, and s_{B′} are terms of their respective annotated types. Assume also the coherence conditions

(i) {v_{B} ↦ u_{B}}; {v_{B} ↦ t_{B′}} = {v_{B} ↦ u_{B′}}
(ii) {(v_{A}, v_{B}) ↦ s_{B}}; {v_{B} ↦ t_{B′}} = {(v_{A}, v_{B}) ↦ (t_{A′}, t_{B′})}; {(v_{A′}, v_{B′}) ↦ s_{B′}}

Then for any term t_{L} of List(A) we have

\{| \begin{matrix}nil : () ↦ u_{B′} \\ cons : (v_{A′}, v_{B′}) ↦ s_{B′} \end{matrix} |\} (List[v_{A} ↦ t_{A′}](t_{L}))

= \{v_{B} ↦ t_{B′}\}(\{| \begin{matrix}nil : () ↦ u_{B} \\ cons : (v_{A}, v_{B}) ↦ s_{B} \end{matrix} |\} (t_{L}))

Proof. We proceed by structural induction on t_{L} and assume without loss that t_{L} is of the form c_{i}(t_{∗}) where c_{1} = nil and c_{2} = cons.

(i) Let t_{L} = nil(). Then both sides quickly reduce to showing

u_{B′} =_{v_{B}} σ_{v_{B}:=u_{B}}(t_{B′})

which merely rephrases assumption (i).

(ii) Let t_{L} = cons(a, l). Thus

\{| \begin{matrix}nil : () ↦ u_{B′} \\ cons : (v_{A′}, v_{B′}) ↦ s_{B′} \end{matrix} |\} (List[v_{A} ↦ t_{A′}](cons(a, l)))

= \{| \begin{matrix}nil : () ↦ u_{B′} \\ cons : (v_{A′}, v_{B′}) ↦ s_{B′} \end{matrix} |\} (cons(σ_{v_{A}:=a}(t_{A′}), List[v_{A} ↦ t_{A′}](l)))

= \{(v_{A′}, v_{B′}) ↦ s_{B′}\}(Prod[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{| \begin{matrix}nil : () ↦ u_{B′} \\ cons : (v_{A′}, v_{B′}) ↦ s_{B′} \end{matrix} |\} (w_{L}) \end{matrix} ] (σ_{v_{A}:=a}(t_{A′}), List[v_{A} ↦ t_{A′}](l)))

= \{(v_{A′}, v_{B′}) ↦ s_{B′}\}(σ_{v_{A}:=a}(t_{A′}), \{| \begin{matrix}nil : () ↦ u_{B′} \\ cons : (v_{A′}, v_{B′}) ↦ s_{B′} \end{matrix} |\} (List[v_{A} ↦ t_{A′}](l)))
= \{(v_{A′}, v_{B′}) ↦ s_{B′}\}(σ_{v_{A}:=a}(t_{A′}), \{v_{B} ↦ t_{B′}\}(\{| \begin{matrix}nil : () ↦ u_{B} \\ cons : (v_{A}, v_{B}) ↦ s_{B} \end{matrix} |\} (l)))
= \{(v_{A′}, v_{B′}) ↦ s_{B′}\}(\{(v_{A}, v_{B}) ↦ (t_{A′}, t_{B′})\}(a, \{| \begin{matrix}nil : () ↦ u_{B} \\ cons : (v_{A}, v_{B}) ↦ s_{B} \end{matrix} |\} (l)))
= \{v_{B} ↦ t_{B′}\}(\{(v_{A}, v_{B}) ↦ s_{B}\}(a, \{| \begin{matrix}nil : () ↦ u_{B} \\ cons : (v_{A}, v_{B}) ↦ s_{B} \end{matrix} |\} (l)))

= \{v_{B} ↦ t_{B′}\}(\{(v_{A}, v_{B}) ↦ s_{B}\}(Prod[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{| \begin{matrix}nil : () ↦ u_{B} \\ cons : (v_{A}, v_{B}) ↦ s_{B} \end{matrix} |\} (w_{L}) \end{matrix} ] (a, l)))

= \{v_{B} ↦ t_{B′}\}(\{| \begin{matrix}nil : () ↦ u_{B} \\ cons : (v_{A}, v_{B}) ↦ s_{B} \end{matrix} |\} (cons(a, l)))

The required induction occurs in the fourth step and the application of assumption (ii) in the

sixth. □

3 The Equivalence of Combinators and Term Logic

An equivalence between a categorical combinator theory and an equational programming logic is expressed by a pair of mutually inverse consistent, or well-defined, translations: combinators-to-programs and programs-to-combinators. Consistency simply means that a translation preserves equality.

A cartesian combinator theory C has the specification (T , F, S, E) where T is a collection of primitive types, F is a collection of pre-determined maps or combinators, S is the set of type signatures of the combinators, and E is a set of equations between combinators.

The types are given by the same rules used earlier for generating the cartesian theory types. The combinators are generated inductively by

• For every type τ there is an identity combinator id_{τ} : τ ⟶ τ.

• For every type τ there is a final combinator !_{τ} : τ ⟶ 1.

• If f ∈ F has signature (τ_{1}, τ_{2}), then f : τ_{1} ⟶ τ_{2} is a combinator.

• For every pair of types τ_{0} and τ_{1}, there are projection combinators p_{0}^{τ_{0},τ_{1}} : τ_{0} × τ_{1} ⟶ τ_{0} and p_{1}^{τ_{0},τ_{1}} : τ_{0} × τ_{1} ⟶ τ_{1}.

• If c_{0} : τ ⟶ τ_{0} and c_{1} : τ ⟶ τ_{1} are combinators, then their pairing ⟨c_{0}, c_{1}⟩ : τ ⟶ τ_{0} × τ_{1} is a combinator.

• If c_{0} : τ_{0} ⟶ τ_{1} and c_{1} : τ_{1} ⟶ τ_{2} are combinators, then their composition c_{0} ; c_{1} : τ_{0} ⟶ τ_{2} is a combinator.

The symmetric transitive closure of the relation defined by the fundamental axioms and inference rules below give the congruence relation among combinators possessing the same domain and codomain types:

• (c_{0} ; c_{1}) ; c_{2} ≡ c_{0} ; (c_{1} ; c_{2}).

• id ; c ≡ c ≡ c; id.

• ⟨c_{0}, c_{1}⟩; p_{0} ≡ c_{0}.

• ⟨c_{0}, c_{1}⟩; p_{1} ≡ c_{1}.

• ⟨c; p_{0} , c; p_{1}⟩ ≡ c.

• c; ! ≡ !.

• If c_{0} ≡ c′_{0} and c_{1} ≡ c′_{1} then c_{0} ; c_{1} ≡ c′_{0} ; c′_{1}.

• If c_{0} = c_{1} in E then c_{0} ≡ c_{1}.

This relation constitutes the minimal set of equations to be contained in E for a cartesian theory.

3.1 Translating Programs to Combinators

A translation, herein denoted C, of closed abstracted terms, or programs, to combinators and a proof of its consistency is presented in this section. We first define below the translation of programs in the cartesian theory. The notation

C[[v ↦ t]]

represents the application of the translation C to any member of the =_{v_{τ}} -equivalence class of the program {v ↦ t}. The definition proceeds inductively on the construction of the abstracted term representing the program:

(i) C[[v_{τ} ↦ ()]] = !_{τ} (ii) If v_{τ} is a variable then C[[v_{τ} ↦ v_{τ}]] = id_{τ} (iii) If v_{0} and v_{1} are variable bases then C[[(v_{0}, v_{1}) ↦ v]] = p_{0} ; C[[v_{0} ↦ v]] if v ∈ fvars(v_{0})) and C[[(v_{0}, v_{1}) ↦ v]] = p_{1} ; C[[v_{1} ↦ v]] if v ∈ fvars(v_{1})

(iv) C[[v ↦ {v′ ↦ t}(t′)]] = ⟨C[[v ↦ t′]], id⟩; C[[(v′, v) ↦ t]]

(v) If f is a function symbol (including any amended projections) then C[[v ↦ f(t)]] = C[[v ↦ t]] ; f

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

The rest of this section is devoted to showing the well-defineness of this translation. Appropriately, the generating set of given equations E in the target cartesian combinator theory should extend the ≡-relation defined above and be exactly the translation images of those in E_{0}, the equations of the cartesian theory.

Whenever strong datatypes are appended to the theory, the translation requires an extension to the new terms generated by the addition of the associated constructors and factorizers. It is technically necessary to define the extension for only the constructed terms and either the fold terms (for an initial datatype) or the unfold terms (for a final datatype) since the remaining terms are expressible in terms of folds and unfolds, respectively. Yet it is instructive to see the development for the case and map terms as well and therefore appropriate to be presented here. Shown below is the incremental extension to be used for adding a strong initial datatype L:

(i) C[[v ↦ c_{i}(t)]] = C[[v ↦ t]] ; c_{i}

(ii)

C [[v_{X} ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (t)]] = ⟨C[[v_{X} ↦ t]], id⟩; fold^{L}\{C[[(v_{1}, v_{X}) ↦ t_{1}]], …, C[[(v_{n}, v_{X}) ↦ t_{n}]]\}

(iii)

C \begin{matrix}[ \\ [ & v_{X} ↦ \{ \begin{matrix}c_{1}(v_{1}) ↦ t_{1} \\ … \\ c_{n}(v_{n}) ↦ t_{n} \end{matrix} \} (t) & ] \\ ] \end{matrix} = ⟨C[[v_{X} ↦ t]], id⟩; case^{L}\{C[[(v_{1}, v_{X}) ↦ t_{1}]], …, C[[(v_{n}, v_{X}) ↦ t_{n}]]\}

(iv)

C \begin{matrix}[ \\ [ & v_{X} ↦ L[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (t) & ] \\ ] \end{matrix} = ⟨C[[v_{X} ↦ t]], id⟩; map^{L}\{C[[(w_{1}, v_{X}) ↦ t_{1}]]), …, C[[(w_{m}, v_{X}) ↦ t_{m}]]\}

Next are the translation rules to be added when adjoining a new strong final datatype R:

(i) C[[v ↦ d_{i}(t)]] = C[[v ↦ t]] ; d_{i}

(ii)

C [[v_{X} ↦ (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t)]] = ⟨C[[v_{X} ↦ t]], id⟩; unfold^{R}\{C[[(v_{C}, v_{X}) ↦ t_{1}]], …, C[[(v_{C}, v_{X}) ↦ t_{n}]]\}

(iii)

C \begin{matrix}[ \\ [ & v_{X} ↦ ( \begin{matrix}d_{1} : t_{1}(t) \\ … \\ d_{n} : t_{n}(t) \end{matrix} ) & ] \\ ] \end{matrix} = ⟨C[[v_{X} ↦ t]], id⟩; record^{R}\{C[[(v_{C}, v_{X}) ↦ t_{1}]], …, C[[(v_{C}, v_{X}) ↦ t_{n}]]\}

C \begin{matrix}[ \\ [ & v_{X} ↦ R[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (t) & ] \\ ] \end{matrix} = ⟨C[[v_{X} ↦ t]], id⟩; map^{R}\{C[[(w_{1}, v_{X}) ↦ t_{1}]], …, C[[(w_{m}, v_{X}) ↦ t_{m}]]\}

The following lemma is helpful in showing the consistency of this translation:

Lemma 3.1 For the logic-to-combinator translation C,

(i) If v_{L} does not occur freely in any of the t_{i} then

C [[(v_{L}, v_{X}) ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (v_{L})]] = fold^{L}\{C[[(v_{1}, v_{X}) ↦ t_{1}]], …, C[[(v_{n}, v_{X}) ↦ t_{n}]]\}

(ii) If v_{L} does not occur freely in any of the t_{i} then

C \begin{matrix}[ \\ [ & (v_{L}, v_{X}) ↦ \{ \begin{matrix}c_{1}(v_{1}) ↦ t_{1} \\ … \\ c_{n}(v_{n}) ↦ t_{n} \end{matrix} \} (v_{L}) & ] \\ ] \end{matrix} = case^{L}\{C[[(v_{1}, v_{X}) ↦ t_{1}]], …, C[[(v_{n}, v_{X}) ↦ t_{n}]]\}

(iii) If v_{L} does not occur freely in any of the t_{i} then

C \begin{matrix}[ \\ [ & (v_{L}, v_{X}) ↦ L[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (v_{L}) & ] \\ ] \end{matrix} = map^{L}\{C[[(w_{1}, v_{X}) ↦ t_{1}]]), …, C[[(w_{m}, v_{X}) ↦ t_{m}]]\}

(iv) If v′_{C} does not occur freely in any of the t_{i} then

C [[(v′_{C}, v_{X}) ↦ (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (v′_{C})]] = unfold^{R}\{C[[(v_{C}, v_{X}) ↦ t_{1}]], …, C[[(v_{C}, v_{X}) ↦ t_{n}]]\}

(v) If v′_{C} does not occur freely in any of the t_{i} then

C \begin{matrix}[ \\ [ & (v′_{C}, v_{X}) ↦ ( \begin{matrix}d_{1} : t_{1}(v′_{C}) \\ … \\ d_{n} : t_{n}(v′_{C}) \end{matrix} ) & ] \\ ] \end{matrix} = record^{R}\{C[[(v_{C}, v_{X}) ↦ t_{1}]], …, C[[(v_{C}, v_{X}) ↦ t_{n}]]\}

(vi) If v_{R} does not occur freely in any of the t_{i} then

C \begin{matrix}[ \\ [ & (v_{R}, v_{X}) ↦ R[ \begin{matrix}w_{1} ↦ t_{1} \\ … \\ w_{m} ↦ t_{m} \end{matrix} ] (v_{R}) & ] \\ ] \end{matrix} = map^{R}\{C[[(w_{1}, v_{X}) ↦ t_{1}]], …, C[[(w_{m}, v_{X}) ↦ t_{m}]]\}

Proof. The lemma simply states the effect of freely expanding the abstraction of the major augmentation terms. The derivation for only the fold-from-L term is given below where the key step, distributing id ×p_{1}, arises from the naturality of strength transformations. The remaining cases have analogous proofs: the derivation for the unfold-to-R term also depends on the naturality of strength, the case-from-L on the naturality of c_{i} × id, the record-to-R directly on the universality property, and both map terms on the naturality of strength.

C [[(v_{L}, v_{X}) ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (v_{L})]] =

= ⟨C[[(v_{L}, v_{X}) ↦ v_{L}]], id⟩; fold^{L}{…, C[[(v_{i}, (v_{L}, v_{X})) ↦ t_{i}]], …}
= ⟨p_{0}, id⟩; fold^{L}{…, C[[(v_{i}, (v_{L}, v_{X})) ↦ t_{i}]], …}
= ⟨p_{0}, id⟩; fold^{L}{…, (id ×p_{1}) ; C[[(v_{i}, v_{X}) ↦ t_{i}]], …}
= ⟨p_{0}, id⟩; (id ×p_{1}) ; fold^{L}{…, C[[(v_{i}, v_{X}) ↦ t_{i}]], …}
= fold^{L}{…, C[[(v_{i}, v_{X}) ↦ t_{i}]], …}
□

We establish the consistency of this translation for any finite sequence of augmentations of the cartesian theory whereby each augmentation made be built for either a strong initial datatype or a strong final datatype. More precisely, since each augmentation depends on the prior specification of datatypes that produced earlier augmentations, we want to establish consistency for (1) the cartesian theory T_{0} having no strong datatypes (other than products) and (2) any theory T_{n} resulting from an augmentation of any consistently translatable theory built from a sequence of n − 1 augmentations starting from T_{0}.

The consistency result depends heavily on the following lemma that shows substitution in the programming logic corresponds exactly to composition in the category.

Lemma 3.2 Composition is substitution:

C[[v ↦ t]] ; C[[v′ ↦ t′]] = C[[v ↦ σ_{v′:=t}(t′)]]

Proof. The proof proceeds by a structural induction on the complexity of the term t′. The base case, i.e. the terms of the cartesian theory, has been practically shown in [1]. However, due to the fact that the cartesian theory presented here is a slight generalization of the original one in [1], we complete the base case proof by (1) noting renaming-equality is preserved by the straightforward result

C[[v_{τ} ↦ v_{τ}]] = id_{τ}

for any variable base v_{τ} and (2) by demonstrating the application term case:

Let t′ = {v_{0} ↦ t_{0}}(t_{1}). Then

C[[v ↦ t]] ; C[[v′ ↦ {v_{0} ↦ t_{0}}(t_{1})]]
= C[[v ↦ t]] ; ⟨C[[v′ ↦ t_{1}]], id⟩; C[[(v_{0}, v′) ↦ t_{1}]]
= ⟨C[[v ↦ t]] ; C[[v′ ↦ t_{1}]] , C[[v ↦ t]]⟩; …
= ⟨C[[v ↦ σ_{v′:=t}(t_{1})]] , C[[v ↦ t]]⟩; …
= C[[v ↦ (σ_{v′:=t}(t_{1}) , t)]] ; …
= C[[v ↦ σ_{(v_{0},v′):=(σ_{v′:=t}(t_{1}) , t)}(t_{0})]]
= C[[v ↦ σ_{v′:=t}(σ_{(v_{0},v′):=(t_{1},v′)}(t_{0}))]]
= C[[v ↦ σ_{v′:=t}(σ_{v_{0}:=t_{1}}(t_{0}))]]
= C[[v ↦ σ_{v′:=t}({v_{0} ↦ t_{0}}(t_{1}))]]

where associativity of substitution provides the critical third-from-last step.

Composition is now assumed to be substitution in the augmented theory T_{n−1}. For the case of an initial datatype augmentation, it suffices to show consistency for the new constructer terms and fold terms presented by T_{n}:

(i) Let t′ = c_{i}(t_{0}). Then

C[[v ↦ t]] ; C[[v′ ↦ c_{i}(t_{0})]]
= C[[v ↦ t]] ; C[[v′ ↦ t_{0}]] ; c_{i}
= C[[v ↦ σ_{v′:=t}(t_{0})]] ; c_{i}
= C[[v ↦ c_{i}(σ_{v′:=t}(t_{0}))]]
= C[[v ↦ σ_{v′:=t}(c_{i}(t_{0})))]]

(ii) Let

t′ = \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (t_{0})

and assume without loss of generality that t_{0} = c_{j}(t_{∗}). Then

C[[v ↦ t]] ; C [[v′ ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (t_{0})]]

= C[[v ↦ t]] ; ⟨C[[v′ ↦ t_{0}]], id⟩; fold^{L}{C[[(v_{1}, v′) ↦ t_{1}]], …, C[[(v_{n}, v′) ↦ t_{n}]]}
= C[[v ↦ t]] ; ⟨C[[v′ ↦ t_{∗}]], id⟩; ⟨map^{E_{j}}{p_{0}, fold^{L}{…}}, p_{1}⟩; C[[(v_{j}, v′) ↦ t_{j}]]
= ⟨C[[v ↦ σ_{v′:=t}(t_{∗})]] , C[[v ↦ t]]⟩; ⟨map^{E_{j}}{p_{0}, fold^{L}{…}}, p_{1}⟩; C[[(v_{j}, v′) ↦ t_{j}]]
= C[[v ↦ (σ_{v′:=t}(t_{∗}), t)]] ; ⟨map^{E_{j}}{p_{0}, fold^{L}{…}}, p_{1}⟩; C[[(v_{j}, v′) ↦ t_{j}]]
= …; ⟨map^{E_{j}}\{C[[(w_{A}, v′) ↦ w_{A}]], C [[(w_{L}, v′) ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (w_{L})]]\}, p_{1}⟩; …

= …; ⟨C[[(v′_{j}, v′) ↦ E_{j}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{|…|\}(w_{L}) \end{matrix} ] (v′_{j})]], p_{1}⟩; …
= …; C[[(v′_{j}, v′) ↦ (E_{j}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{|…|\}(w_{L}) \end{matrix} ] (v′_{j}), v′)]] ; …
= C[[v ↦ σ_{(v′_{j},v′):=(σ_{v′:=t}(t_{∗}),t)}(E_{j}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{|…|\}(w_{L}) \end{matrix} ] (v′_{j}), v′)]] ; …
= C[[v ↦ σ_{v′:=t}(σ_{(v′_{j},v′):=(t_{∗},v′)}(E_{j}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{|…|\}(w_{L}) \end{matrix} ] (v′_{j}), v′))]] ; …
= C[[v ↦ σ_{v′:=t}(E_{j}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{|…|\}(w_{L}) \end{matrix} ] (t_{∗}), t)]] ; …
= C[[v ↦ σ_{(v_{j},v′):=(σ_{v′:=t}(E_{j}[...](t_{∗}),t)}(t_{j})]]
= C[[v ↦ σ_{v′:=t}(σ_{v_{j}:=E_{j}[...](t_{∗})}(t_{j}))]]
= C [[v ↦ σ_{v′:=t}(\{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (t_{0}))]]

For augmenting with final datatypes, we analogously show consistency for the destructor terms and the unfold terms:

(i) For t′ = d_{i}(t_{0}), the proof parallels exactly the one for constructor terms.

(ii) Let

t′ = (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t_{0})

Then

C[[v ↦ t]] ; C [[v′ ↦ (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t_{0})]] ; d_{j}

= C[[v ↦ t]] ; ⟨C[[v′ ↦ t_{0}]], id⟩; unfold^{R}{C[[(v_{C}, v′) ↦ t_{1}]], …, C[[(v_{C}.v′) ↦ t_{n}]]}; d_{j}
= ⟨C[[v ↦ σ_{v′:=t}(t_{0})]], C[[v ↦ t]]⟩; ⟨C[[(v_{C}, v′) ↦ t_{j}]], p_{1}⟩; map^{E_{j}}{p_{0}, unfold{…}}
= C[[v ↦ (σ_{v′:=t}(t_{0}), t)]] ; C[[(v_{C}, v′) ↦ (t_{j}, v′)]] ; …
= C[[v ↦ σ_{(v_{C},v′):=(σ_{v′:=t}(t_{0}),t)}(t_{j}, v′)]] ; …
= C[[v ↦ σ_{v′:=t}(σ_{v_{C}:=t_{0}}(t_{j}), v′)]] ; …
= …; map^{E_{j}}\{C[[(w_{A}, v′) ↦ w_{A}]], C[[(w_{L}, v′) ↦ (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (w_{L})]]\}

= …; C \begin{matrix}[ \\ [ & (v_{j}, v′) ↦ E_{j}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ (|…|)(w_{L}) \end{matrix} ] (v_{j}) & ] \\ ] \end{matrix}
= C[[v ↦ σ_{(v_{j},v′):=(σ_{v′:=t}(σ_{v_{C}:=t_{0}} (t_{j})),t)}(E_{j}[…](v_{j}))]]
= C[[v ↦ σ_{v′:=t}(σ_{v_{j}:=σ_{v_{C}:=t_{0}} (t_{j})}(E_{j}[…](v_{j})))]]

= C [ ; [v ↦ σ_{v′:=t}(E_{j}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{C} ↦ (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (w_{C}) \end{matrix} ] (σ_{v_{C}:=t_{0}}(t_{j})))] ; ]

= C [[v ↦ σ_{v′:=t}(d_{j}((| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t_{0})))]]

= C [[v ↦ σ_{v′:=t}((| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t_{0}))]] ; d_{j}

□

The major consistency properties of the translation can now be stated and proven. The first theorem below is a specialization of the second, but it is stated due to its importance in studying basic distributive computation and explaining how the three primary combinators foldSum, caseSum, and mapSum for the strong initial datatype Sum, simply the coproduct of two datatypes, merge into essentially a common operation in the simplest of all predistributive theories.

Proposition 3.3 Suppose a cartesian theory is augmented with the Sum initial datatype to form a basic predistributive theory. Then C is a consistent translation from the predistributive theory into distributive categorical combinators.

Proof. This is a mild extension of the consistency result proven by Cockett [1] that included only the case-from-Sum axiom. It remains only to append that proof by showing translation consistency for the fold-from-Sum and map-on-Sum axioms.

The fold-from-Sum axiom is preserved because its translation differs from the case-from-Sum axiom translation only on the left side by their respective occurrences of the morphisms of the form foldSum{f_{1}, f_{2}} and caseSum{f_{1}, f_{2}}. Both morphisms are easily shown to be equal in a predistributive category.

The only difference between the translation of the map-on-Sum axiom using the assigned terms t_{0} and t_{1} and the case-from-Sum axiom using the assigned terms b_{0}(t_{0}) and b_{1}(t_{1}) (where b_{0} and b_{1} are the Sum constructors) are the respective occurrences on the left side of morphisms of the form mapSum{f_{1}, f_{2}} and caseSum{f_{1} ; b_{0}, f_{2} ; b_{1}}. These two morphisms can be quickly verified to be equal in a predistributive category.

□

We now state the major theorem of this section:

Proposition 3.4 For any theory built from a cartesian theory by a finite sequence of augmentations of strong initial datatypes and strong final datatypes, C is a consistent translation.

Proof. First we cover the initial datatype situation. Because the case-from-L and map-on-L terms can be expressed in terms of a fold-from-L term for any initial datatype L, it suffices to discuss consistency only for the fold-from-L axiom and the L fold uniqueness rule. An induction on augmentations has been obviated by the inductive proofs of Lemma 3.2. In fact, the proofs below follow those inductive proofs closely, indicating that consistency in this direction is reaffirming that composition-is-substitution.

(i) Fold-from-L axiom:

C [[v_{X} ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (c_{i}(t))]]

= ⟨C[[v_{X} ↦ c_{i}(t)]], id⟩; fold^{L}{C[[(v_{1}, v_{X}) ↦ t_{1}]], …, C[[(v_{n}, v_{X}) ↦ t_{n}]]}
= ⟨C[[v_{X} ↦ t]] ; c_{i} , id⟩; fold^{L}{C[[(v_{1}, v_{X}) ↦ t_{1}]], …, C[[(v_{n}, v_{X}) ↦ t_{n}]]}
= ⟨C[[v_{X} ↦ t]], id⟩; ⟨map^{E_{i}}{p_{0}, fold^{L}{…}}, p_{1}⟩; C[[(v_{i}, v_{X}) ↦ t_{i}]]
= C[[v_{X}) ↦ (t, v_{X})]] ; ⟨map^{E_{i}}{p_{0}, fold^{L}{…}}, p_{1}⟩; C[[(v_{i}, v_{X}) ↦ t_{i}]]
= …; ⟨map^{E_{i}}\{C[[(w_{A}, v_{X}) ↦ w_{A}]], C [[(w_{L}, v_{X}) ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (w_{L})]]\}, p_{1}⟩; …

= …; ⟨C \begin{matrix}[ \\ [ & v′_{i}, v_{X}) ↦ E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{|…|\}(w_{L}) \end{matrix} ] (v′_{i}) & ] \\ ] \end{matrix} , p_{1}⟩; …
= …; C[[v′_{i}, v_{X}) ↦ (E_{i}[…](v′_{i}), v_{X})]] ; …
= C[[v_{X} ↦ (E_{i}[…](t), v_{X})]] ; …
= C[[v_{X} ↦ σ_{v_{i},v_{X}):=(E_{i}[...](t),v_{X})}(t_{i})]]

= C [ ; [v_{X} ↦ \{v_{i} ↦ t_{i}\}(E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (w_{L}) \end{matrix} ] (t))] ; ]

(ii) L fold uniqueness:

In straightforward fashion the left-hand and right-hand sides of the antecedent translate into the equation of the universal initiality diagram. The consequent translates directly into the assertion that the unique action is the combinator fold^{L}.

Now we examine the essential final datatype cases.

(i) Unfold-to-R axiom:

C [[v_{X} ↦ d_{i}((| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t))]]

= C [[v_{X} ↦ (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (t)]] ; d_{i}
= ⟨C[[v_{X} ↦ t]], id⟩; unfold^{R}{C[[(v_{C}, v_{X}) ↦ t_{1}]], …, C[[(v_{C}, v_{X}) ↦ t_{n}]]}; d_{i}
= C[[v_{X} ↦ (t, v_{X})]] ; unfold^{R}{C[[(v_{C}, v_{X}) ↦ t_{1}]], …, C[[(v_{C}, v_{X}) ↦ t_{n}]]}; d_{i}
= C[[v_{X} ↦ (t, v_{X})]] ; ⟨C[[(v_{i}, v_{X}) ↦ t_{i}]], p_{1}⟩; map^{E_{i}}{p_{0}, unfold^{R}{…}}
= C[[v_{X} ↦ (t, v_{X})]] ; ⟨C[[(v_{i}, v_{X}) ↦ (t_{i}, v_{X})]] ; map^{E_{i}}{p_{0}, unfold^{R}{…}}
= C[[v_{X} ↦ (σ_{v_{i}:=t}(t_{i}), v_{X})]] ; map^{E_{i}}{p_{0}, unfold^{R}{…}}
= …; map^{E_{i}}\{C[[(w_{A}, v_{X}) ↦ w_{A}]], C [[(w_{R}, v_{X}) ↦ (| \begin{matrix}d_{1} : t_{1} \\ v_{C} ↦ … \\ d_{n} : t_{n} \end{matrix} |) (w_{R})]]\}

= …; C \begin{matrix}[ \\ [ & (v′_{i}, v_{X}) ↦ E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{R} ↦ (|…|)(w_{R}) \end{matrix} ] (v′_{i}) & ] \\ ] \end{matrix}
= C \begin{matrix}[ \\ [ & v_{X} ↦ σ_{v′_{i}:=σ_{v_{i}:=t}(t_{i})}(E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{R} ↦ (|…|)(w_{R}) \end{matrix} ] (v′_{i})) & ] \\ ] \end{matrix}
= C \begin{matrix}[ \\ [ & v_{X} ↦ E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{R} ↦ (|…|)(w_{R}) \end{matrix} ] (σ_{v_{i}:=t}(t_{i})) & ] \\ ] \end{matrix}
= C \begin{matrix}[ \\ [ & v_{X} ↦ E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{R} ↦ (|…|)(w_{R}) \end{matrix} ] (\{v_{i} ↦ t_{i}\}(t)) & ] \\ ] \end{matrix}

(ii) R unfold uniqueness:

Just as for the L fold uniqueness, the translation directly yields the universal finality diagram from the antecedent and the uniqueness of the unfold operator from the consequent.

□

3.2 Translating Combinators to Programs

We now present a consistent translation in the opposite direction. The translation of a combinator f will be denoted P[[f]]. Because we demand consistency, the definition of the translation must preserve, first of all, the definition of a cartesian category.

Naively, the translation of a combinator expression requires a choice of variable base up to variable-renaming for the resulting program. Thus the translation is first presented by using the following notational definitions of composition (“;”) and pairing (“,”) of programs to allow for combinations of variable bases that are type-equivalent but possibly syntactically unequal:

(i) P[[f]] ≡ {v ↦ P_{v}[[f]]} where v is any variable base for the domain of a combinator f

(ii) {v ↦ t}; {v′ ↦ t′} ≡ {v ↦ σ_{v′:=t}(t′)}

(iii) ⟨{v ↦ t_{0}}, {v′ ↦ t_{1}}⟩ ≡ {v ↦ (t_{0}, σ_{v′:=v}(t_{1}))}

Using this notation on the right-hand sides of the definitions below, the translation P for a cartesian category is defined as follows:

(i) P[[f; g]] = P[[f]] ; P[[g]]

(ii) P[[⟨f, g⟩]] = ⟨P[[f]], P[[g]]⟩

(iii) P[[id_{τ}]] = {v_{τ} ↦ v_{τ} }

(iv) P[[!_{τ}]] = {v_{τ} ↦ ()}

(v) If v is a variable base for the domain of the combinator whose symbol is f (including projection combinators) then P[[f]] = {v ↦ f(v)}. That is, for a function symbol f we have P_{v}[[f]] = f(v).

However, the notational definition immediately provides P[[f]] = {v ↦ P[[f]](v)} from the extensionality property of the target cartesian theory. This allows the equivalent re-expression of the P translation rules (i) and (ii) as

(i′) P[[f; g]] = {v ↦ P[[g]](P[[f]](v))}

(ii′) P[[⟨f, g⟩]] = {v ↦ (P[[f]](v), P[[g]](v))}

where v is any variable base of the appropriate domain type. We thereby remove the dependency of the translation on the explicit choice of variable base and make the new notation behave exactly the same as its conventional usage in the cartesian theory.

With the addition of a strong initial datatype to the category, the translation is extended to the new generating morphisms — the constructors and the fold factorizers. For clarity, the translation is redundantly presented below for all three factorizers. It is straightforward to establish the translation rules for the case factorizer and the map factorizer from the translation rule defined for the fold factorizer.

(i) P[[c_{i}]] = {v ↦ c_{i}(v)} where v is a variable base for the domain of c_{i}

(ii) P[[fold^{L}\{h_{1}, …, h_{n}\}]] = \{(v_{L}, v_{X}) ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ P[[h_{1}]](v_{1}, v_{X}) \\ … \\ c_{n} : v_{n} ↦ P[[h_{n}]](v_{n}, v_{X}) \end{matrix} |\} (v_{L})\}

(iii) P[[case^{L}\{h_{1}, …, h_{n}\}]] = \{(v_{L}, v_{X}) ↦ \{ \begin{matrix}c_{1}(v_{1}) ↦ P[[h_{1}]](v_{1}, v_{X}) \\ … \\ c_{n}(v_{n}) ↦ P[[h_{n}]](v_{n}, v_{X}) \end{matrix} \} (v_{L})\}

(iv) P[[map^{L}\{f_{1}, …, f_{m}\}]] = \{(v_{L}, v_{X}) ↦ L[ \begin{matrix}w_{1} ↦ P[[f_{1}]](w_{1}, v_{X}) \\ … \\ w_{m} ↦ P[[f_{m}]](w_{m}, v_{X}) \end{matrix} ] (v_{L})\}

Similarly, the extension of the combinator translation to include strong final datatypes is (redundantly) presented below:

(i) P[[d_{i}]] = {v ↦ d_{i}(v)} where v is a variable base for the domain of d_{i}

(ii) P[[unfold^{R}\{g_{1}, …, g_{n}\}]] = \{(v′_{C}, v_{X}) ↦ (| \begin{matrix}d_{1} : P[[g_{1}]](v_{C}, v_{X}) \\ v_{C} ↦ … \\ d_{n} : P[[g_{n}]](v_{C}, v_{X}) \end{matrix} |) (v′_{C})\}

(iii) P[[record^{R}\{g_{1}, …, g_{n}\}]] = \{(v′_{C}, v_{X}) ↦ ( \begin{matrix}d_{1} : P[[g_{1}]](v′_{C}, v_{X}) \\ … \\ d_{n} : P[[g_{n}]](v′_{C}, v_{X}) \end{matrix} )\}

(iv) P[[map^{R}\{f_{1}, …, f_{m}\}]] = \{(v_{R}, v_{X}) ↦ R[ \begin{matrix}w_{1} ↦ P[[f_{1}]](w_{1}, v_{X}) \\ … \\ w_{m} ↦ P[[f_{m}]](w_{m}, v_{X}) \end{matrix} ] (v_{R})\}

Theorem 3.5 For any cartesian category closed under strong initial datatypes and strong final datatypes, P is a consistent translation of combinators into programs.

Proof. The consistency for the cartesian combinator axioms was previously demonstrated in Cockett [1] using the naive form of the translation definition. The consistency of translating constructor combinators is immediate. Since all factorizers are expressible by fold or unfold factorizers, it remains only to show consistency for the rewriting reduction and the uniqueness of the fold and unfold factorizers.

The proofs employ an induction on the augmentation of strong datatypes. As before, all variables are assumed to have been renamed beforehand to avoid clashes.

L fold factorizer reduction:

P[[c_{i} × id_{X} ; fold^{L}{h_{1}, …, h_{n}}]]

= ⟨P[[p_{0}]] ; P[[c_{i}]] , P[[p_{1}]]⟩; P[[fold^{L}{h_{1}, …, h_{n}}]]
= \{(v_{i}, v_{X}) ↦ (c_{i}(p_{0}(v_{i}, v_{X})), p_{1}(v_{i}, v_{X}))\}; \{(v_{L}, v_{X}) ↦ \{| \begin{matrix}… \\ c_{i} : v_{i} ↦ P[[h_{i}]](v_{i}, v_{X}) \\ … \end{matrix} |\} (v_{L})\}

= \{(v_{i}, v_{X}) ↦ \{| \begin{matrix}… \\ c_{i} : v_{i} ↦ P[[h_{i}]](v_{i}, v_{X}) \\ … \end{matrix} |\} (c_{i}(v_{i}))\}
= \{(v_{i}, v_{X}) ↦ σ_{v_{i}:=E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{L} ↦ \{| \begin{matrix}… \\ c_{i} : v_{i} ↦ P[[h_{i}]](v_{i}, v_{X}) \\ … \end{matrix} |\} (w_{L}) \end{matrix} ](v_{i})}(P[[h_{i}]](v_{i}, v_{X}))\}

= \{(v_{i}, v_{X}) ↦ (E_{i}[ \begin{matrix}w_{A} ↦ P[[p_{0}]](w_{A}, v_{X}) \\ w_{L} ↦ P[[fold^{L}\{h_{1}, …, h_{n}\}]](w_{L}, v_{X}) \end{matrix} ] (v_{i}), v_{X})\}; \{(v_{i}, v_{X}) ↦ P[[h_{i}]](v_{i}, v_{X})\}
= ⟨P[[map^{E_{i}}{p_{0}, fold^{L}{h_{1}, …, h_{n}}}]], P[[p_{1}]]⟩; P[[h_{i}]]
= P[[⟨map^{E_{i}}{p_{0}, fold^{L}{h_{1}, …, h_{n}}}, p_{1}⟩; h_{i}]]

L fold factorizer uniqueness:

Suppose that for i = 1, …, n that

c_{i} × id_{X} ; h = ⟨map^{E_{i}}{p_{0}, h}, p_{1}⟩; h_{i} .

By induction on augmentations the translations of both combinator expressions are equal. The left-hand side translates exactly to the same form as the left-hand side of the antecedent of the L fold uniqueness rule, and likewise for the right-hand side. Applying that rule, it immediately follows that the translations of h and fold^{L}{h_{1}, …, h_{n}} are equal.

R unfold factorizer reduction:

P[[unfold^{R}{g_{1}, …, g_{n}}; d_{i}]]

= P[[unfold^{R}{g_{1}, …, g_{n}}]] ; P[[d_{i}]]
= \{(v′_{C}, v_{X}) ↦ (| \begin{matrix}… \\ v_{C} ↦ d_{j} : P[[g_{j}]](v_{C}, v_{X}) \\ … \end{matrix} |) (v′_{C})\}; \{v_{R} ↦ d_{i}(v_{R})\}

= \{(v′_{C}, v_{X}) ↦ d_{i}((| \begin{matrix}… \\ v_{C} ↦ d_{j} : P[[g_{j}]](v_{C}, v_{X}) \\ … \end{matrix} |) (v′_{C}))\}

= \{(v′_{C}, v_{X}) ↦ E_{i}[ \begin{matrix}w_{A} ↦ w_{A} \\ w_{R} ↦ (| \begin{matrix}… \\ v_{C} ↦ d_{j} : P[[g_{j}]](v_{C}, v_{X}) \\ … \end{matrix} |) (w_{C}) \end{matrix} ] (P[[g_{i}]](v′_{C}, v_{X})\}

= \{(v′_{C}, v_{X}) ↦ (P[[g_{i}]](v′_{C}, v_{X}), v_{X})\}; \{(v_{i}, v_{X}) ↦ E_{i}[ \begin{matrix}w_{A} ↦ P[[p_{0}]](w_{A}, v_{X}) \\ w_{R} ↦ P[[unfold^{R}\{g_{1}, …, g_{n}\}]](w_{C}, v_{X}) \end{matrix} ] (v_{i})\}
= ⟨P[[g_{i}]], P[[p_{1}]]⟩; P[[map^{E_{i}}{p_{0}, unfold^{R}{g_{1}, …, g_{n}}}]]
= P[[⟨g_{i}, p_{1}⟩; map^{E_{i}}{p_{0}, unfold^{R}{g_{1}, …, g_{n}}}]]

R unfold factorizer uniqueness:

The argument proceeds by induction on augmentations in exactly the same manner as the one given for L fold uniqueness.

□

We are finally positioned for proving the equivalence theorem upon which the translation and type-checking subsystems of Charity rest:

Theorem 3.6 C and P form an equivalence between a cartesian category that is closed under strong initial/final datatypes and the corresponding term logic containing all strong initial/final datatype augmentations.

Proof. Consider the translational composition C ∘ P. The argument proceeds by structural induction of combinator expressions. The cartesian cases were proved in [1]. The remaining non-trivial cases — the fold and unfold factorizers — both follow exactly the pattern of proof for the fold factorizer:

C[[P[[fold^{L}{h_{1}, …, h_{n}}]]]]

= C [[(v_{L}, v_{X}) ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ P[[h_{1}]](v_{1}, v_{X}) \\ … \\ c_{n} : v_{n} ↦ P[[h_{n}]](v_{n}, v_{X}) \end{matrix} |\} (v_{L})]]
= fold^{L}{…, C[[(v_{i}, v_{X}) ↦ P[[h_{i}]](v_{i}, v_{X})]], …}
= fold^{L}{…, C[[P[[h_{i}]]]], …}
= fold^{L}{…, h_{i}, …}

Now consider the composition P ∘ C. With comments analogous to those concerning the preceding derivation, we need to seriously look only at the proof pattern for the fold factorizer term:

P[[C[[v_{X} ↦ \{| \begin{matrix}c_{1} : v_{1} ↦ t_{1} \\ … \\ c_{n} : v_{n} ↦ t_{n} \end{matrix} |\} (t)]]]]

= P[[⟨C[[v_{X} ↦ t]], id⟩; fold^{L}{…, C[[(v_{i}, v_{X}) ↦ t_{i}]], …}]]
= P[[⟨C[[v_{X} ↦ t]], id⟩]] ; P[[fold^{L}{…, C[[(v_{i}, v_{X}) ↦ t_{i}]], …}]]
= ⟨P[[C[[v_{X} ↦ t]]]], P[[id]]⟩; \{(v_{L}, v_{X}) ↦ \{| \begin{matrix}… \\ c_{i} : v_{i} ↦ P[[C[[(v_{i}, v_{X}) ↦ t_{i}]]]](v_{i}, v_{X}) \\ … \end{matrix} |\} (v_{L})\}

= ⟨\{v_{X} ↦ t\}, \{v_{X} ↦ v_{X}\}⟩; \{(v_{L}, v_{X}) ↦ \{| \begin{matrix}… \\ c_{i} : v_{i} ↦ \{(v_{i}, v_{X}) ↦ t_{i}\}(v_{i}, v_{X}) \\ … \end{matrix} |\} (v_{L})\}

= \{v_{X} ↦ \{| \begin{matrix}… \\ c_{i} : v_{i} ↦ \{(v_{i}, v_{X}) ↦ t_{i}\}(v_{i}, v_{X}) \\ … \end{matrix} |\} (t)\}

= \{v_{X} ↦ \{| \begin{matrix}… \\ c_{i} : v_{i} ↦ t_{i} \\ … \end{matrix} |\} (t)\}

□

Remark 3.7 For the sake of compactness, the equivalence proof has been presented as an implicit amalgam of three levels of formal structure: sketches, theories, and categories. An alternative method for showing equivalences between theories using these levels explicitly is briefly outlined here.

By reviewing the proof, the reader can discover that our programs and combinators are generated from essentially the same primitive collections of sorts, function symbols, signatures, and equations. This common underlying base structure can be expressed in isolation as a precartesian sketch where finite “products” of sorts are available for forming signatures. We now consider starting the equivalence proof from a given precartesian sketch.

The (strong) equational type theory of a precartesian sketch can then be obtained as the cartesian theory built as according to Section 2.1 and augmented by the equations and inference rules for all strong initial and final datatypes.

The (strong) cartesian combinator theory of a precartesian sketch can also be standardly built as the combinator theory defined in Section 3, similarly augmented by the equations and inference rules corresponding to the initiality and finality diagrams explained in the introduction.

Either theory can be lifted to its syntactic category. For an equational type theory, sorts become objects, closed abstract maps become morphisms, and composition under congruence is defined as our program composition. For a combinator theory, the function symbols inductively generate the morphisms to include identity maps, final maps, projections, pairs, and composition as congruent juxtaposition of combinators. In both situations the equations are lifted directly to the category level.

Our alternative view can now be pictured as

[figure: syntactic category; syntactic category; equational type theory; precartesian sketch; cartesian combinator theory]

where the syntactic equivalence of the two theories, defined as the categorical equivalence of the respective syntactic categories, becomes our new focus.

We particularly note that half of the equivalence proof now falls immediately from observing that the syntactic category of a combinator theory is actually a generic model of the underlying precartesian sketch. That is, there is (1) an evident interpretation or model of the sketch in the combinator syntactic category via its construction, and (2) any other model of the sketch in any other category determines a unique model morphism from the combinator syntactic category to the other category. In our situation, the translation composition C ∘ P is a model morphism of the combinator syntactic category into itself and thus, by uniqueness, can only be the identity translation.

Further details and explanations of sketches, their models, and model morphisms are available to the reader in [11, 10]. The complete development of this particular method is presented in [2].

4 Conclusions and Future Work

The Charity project at Calgary has verified that significant algorithms can be coded, compiled, and run with its categorical programming language compiler built atop the term logic. Such programs include Ackermann’s function, eager and lazy versions of Quicksort, type unification, and an algorithmic approach for the CCS bisimulation relation. We expect to carry out considerable effort to design a robust user-level language that minimizes the programmer’s adjustment required to master the categorical programming paradigm. For example, a “monad” syntax for coding monadic computation programs easily is currently being investigated.

The categorical programming design approach combines top-down modular design at the routine level with bottom-up structurally inductive state-transform design at the code level. Our experience suggests this design strategy quickly becomes natural for newcomers to categorical programming. For example, freely mixing both term logic expressions and categorical combinators is a future implementation goal. The mutual presence of declarative eager and lazy datatypes should also be explored from a programming practicality point of view.

References

[1] J. R. B. Cockett. Distributive logic. Technical Report CS-89-01, University of Tennessee, 1989.

[2] J. R. B. Cockett. The term logic of precartesian categories. Draft manuscript, February 1992.

[3] J. R. B. Cockett and T. Fukushima. About Charity. Unpublished manuscript, 1991.

[4] J. R. B. Cockett and D. Spencer. Strong categorical datatypes. In R. A. G. Seely, editor, International Meeting on Category Theory 1991, Canadian Mathematical Society Proceedings. AMS, Montreal, 1992.

[5] T. Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, 1987.

[6] H. G. Mairson. Outline of a proof theory of parametricity. In 6th International Symposium on Functional Programming Languages and Computer Architecture, pages 313–327, 1991.

[7] J. C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513–523. North-Holland, 1983.

[8] A. Stoughton. Substitution revisited. Theoretical Computer Science, 59:317–325, 1988.

[9] P. Wadler. Theorems for free! In 4th International Symposium on Functional Programming Languages and Computer Architecture, London, U.K., September 1989.

[10] C. Wells. A generalization of the concept of sketch. Theoretical Computer Science, 70:159–178, 1990.

[11] C. Wells and M. Barr. The formal description of data types using sketches. In Mathematical Foundations of Programming Language Semantics, volume 298 of Lecture Notes in Computer Science, Tulane University, April 1987. Springer-Verlag.

[12] G. C. Wraith. A note on categorical datatypes, volume 389 of Lecture Notes in Computer Science, pages 118–127. Springer-Verlag, 1989.