The Internal Operads of Combinatory Algebras

TL;DR

This paper demonstrates that operads serve as a unifying framework for various classes of combinatory algebras, establishing a canonical internal operad construction and deriving extensionality axioms.

Contribution

It introduces the internal operad construction for extensional combinatory algebras, providing a new categorical perspective and a left adjoint to the forgetful functor.

Findings

Every extensional combinatory algebra has a canonical internal operad.

The internal operad construction is a left adjoint to the forgetful functor.

Derived extensionality axioms for multiple classes of combinatory algebras.

Abstract

We argue that operads provide a general framework for dealing with polynomials and combinatory completeness of combinatory algebras, including the classical $\mathbf{SK}$-algebras, linear $\mathbf{BCI}$-algebras, planar $\mathbf{BI}(\_)^\bullet$-algebras as well as the braided $\mathbf{BC^\pm I}$-algebras. We show that every extensional combinatory algebra gives rise to a canonical closed operad, which we shall call the internal operad of the combinatory algebra. The internal operad construction gives a left adjoint to the forgetful functor from closed operads to extensional combinatory algebras. As a by-product, we derive extensionality axioms for the classes of combinatory algebras mentioned above.