The recursion combinator you mention seems to be the recursor associated to an inductive (or recursive) data type. In the paper this seems to be the type describing the syntax of lambda terms. Here, I'll take lists as a simpler recursive type.
Note that the "lists of naturals type" can be intuitively described as the "least" type admitting these constructors:
nil : list \\
cons : nat \to list \to list
Recursive types as the one above have an associated induction principle. For instance, if we wanted to prove a property on all lists $p(l)$, it would suffice to prove
- the base case $p(nil)$, and
- the inductive case $p(l) \implies p(cons\ n\ l)$ for any $n,l$.
If we had more constructors, we would have move base or inductive cases, accordingly.
Similarly, we can define a function $f : list \to A$ by induction. That is to define $f(l)$ on all lists, all we have to do is to define
- what is the result in base case, i.e. $f(nil) = a : A$
- provided we already defined $f(l)$, we need to define $f(cons\ n\ l)$ for all $n,l$.
Note that step 2 amount to define a function $g : nat\to A \to A$, which takes $n:nat$ and $f(l):A$ and produces $g(n)(f(l)) = f(cons\ n\ l)$.
We can generalize this by crafting a combinator that given $a,g$ produces $f$ defined as above. This is called the (primitive) recursor.
rec : A \times (nat \to A \to A) \to (list \to A) \\
rec(a,g)(nil) = a \\
rec(a,g)(cons\ n\ l) = g(n)(rec(a,g)(l))
Usually this is called
foldr in functional programming languages.
Note how, roughly, $a$ replaces $nil$, and $g$ replaces $cons$. Indeed, in the general case, the recursor takes one argument for each constructor of the recursively defined type at hand.
If you have a general fixed point combinator like Church's $Y$, you can easily encode the above. However, in many type theories, you don't have that luxury, since $Y$ causes the inconsistency of the related logic. Instead, for any recursive type you define, you get a restricted version of $Y$ which is the recursor: each type has its own recursion combinator. This ensures the termination of the calculus, which is important to ensure the consistency of the logic.