Categorical Combinators
Pierre-Louis Curien · Birkhäuser Boston eBooks · 1993
In this chapter we introduce the operators (or combinators) of cartesian closed categories as a syntax, and we show that they can be used in a natural way for implementation purposes. The λ-calculus may be compiled in the algebra of first-order categorical terms. In turn, categorical terms may be interpreted through different sets of rewrite rules: so called strong rules simulate the β-reduction of the λ-calculus, while weak rules simulate evaluations with respect to an environment. The weak rules naturally induce an abstract machine, the categorical abstract machine (or CAM), where the categorical terms themselves, considered as machine code, act on a graph of values, with a stack to store pointers on this graph. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.