| Abstract: | Categorical combinators form a formal system similar to Curry's combinatory logic. The original system was developed by Curien, inspired by the equivalence of the theories of typed λ-calculus and Cartesian closed categories, as shown by Lambek and Scott. A new system for categorical combinators was introduced by the author. This system uses a more compact notation for the code and needs a smaller set of rewriting rules. The aim of this paper is to analyse these two different rewriting systems for categorical combinators as a basis for implementation of applicative languages, and compare them with the classical approach due to Turner, using combinatory logic. |
