2
$\begingroup$

According to Categorifying CCCs: Computation as a Process, computation or β-reduction process in untyped-lambda calculus is in fact a 2-morphism in category theory.

Can someone please describe me how is it so and elaborate on it?

P.S. I understand that category theory is a mathematical concept but since this specific question is about β-reduction and lambda calculus I have posted it in computer science section.

$\endgroup$
2
$\begingroup$

Here is a new paper that covers a similar topic. The idea is that by doing algebra in enriched categories (2-categories are like categories enriched in categories), you can talk about more fine grained semantic structure on the algebra. (I haven't read through the whole paper myself, but I know enough to see some of the ideas behind it.)

The way it relates to your question is thus: ordinary categories are, "set enriched," meaning the homs are sets. When giving a categorical semantics of a type theory (say), the (open) terms are interpreted as arrows, the idea being that the domain of an arrow is the context, and the codomain is the type of the open term.

$$ Γ ⊢ e : T \ \ \ \ \ \Longleftrightarrow\ \ \ \ \ e \in Hom(Γ, T)$$

The important thing is that both the terms in the language and the semantics of those terms will form (enriched) categories, and the interpretation of those terms into the semantics will be functors that must preserve the structure of the hom collections. For sets, the structure is just equality of elements. So, equal terms must be assigned equal semantic values.

However, this means set enrichment isn't very good at letting us have structured semantic requirements. If we have β equivalent terms:

$$ (λ x → (x, x))\ e\\ (e,e) $$

then with set enrichment, we have two choices:

  1. They are not equal, so the semantic values assigned can be totally unrelated.
  2. They are equal, so the semantic values must be the same.

However, option 2 basically means that our syntactic category has arrows that are β equivalence classes of terms (or whatever equivalence you wish to require of the semantics). We have pre-quotiented the syntax by all the reductions that hold.

Instead, think about poset enrichment (which is like a 2-category in which there is at most one 2-morphism between any two 1-morphisms). Now there is an additional partial order $\prec$ on elements of the sets, and the semantic assignment must respect that partial order. Now we have a third option, which is to say these two terms are not equal, but they are related:

$$(λ x → (x, x))\ e \prec (e, e)$$

And the semantics can no longer assign them completely unrelated values, they must assign them values that are 'connected' in the semantics.

With posets we are basically only able to represent whether or not a term is reducible to another. With enrichment in a category (like a 2-category), we are able (I think) to keep track of multiple potentially different ways in which reductions can occur, and how to compose them. Vertical composition is like:

$$ e_1 \rightsquigarrow e_2 ∧ e_2 \rightsquigarrow e_3 ⇒ e_1 \rightsquigarrow e_3$$

And horizontal composition is rather like:

$$f_1 \rightsquigarrow f_2 ∧ x_1 \rightsquigarrow x_2 ⇒ f_1 x_1 \rightsquigarrow f_2 x_2$$

Although you should take that with a grain of salt, because that gets into the part of the paper I haven't really read yet.

So, by using 2-categories or enriched categories, we can explicitly represent richer structure on our terms, and talk about semantics that preserves that structure.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.