Given that whole name binding thing is ultimately a story of how to describe a graph using a tree, I was primed to look for monoidal category-ish things, and sure enough the S and K combinators look very much like copy and delete operators; counit and comultiplication for a comonoid. That’s very vibe-based, anyone know of a formal version of this observation?

The author's previous post goes into details of a categorial connection:

  λ-Calculus, Combinatory Logic and Cartesian Closed Categories
  https://thma.github.io/posts/2021-04-04-Lambda-Calculus-Combinatory-Logic-and-Cartesian-Closed-Categories.html

  Categorical combinators, P.-L. Curien
  https://www.sciencedirect.com/science/article/pii/S001999588680047X