Recently, I encountered terminologies such as primitive recursion and recursion combinator. One of the sources is here link I googled and read some, but missing the points of them. I know that recursion occurs when a function appears within its definition. While $\lambda$-calculus cannot express such recursive definitions directly, it can use combinators to implement recursion.So, what are Structural recursion, primitive recursion, recursion combinator and recursion principles? how each related to others?Hoping someone could explain these clearly, so I can go in the right direction. now I am struggling to figure out their points.Thanks in advance!
what are Structural recursion, primitive recursion, recursion combinator and recursion principles?
recursion;primitive recursion;variable binding
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:$$\begin{array}{l}nil : list \\cons : nat \to list \to list\end{array}$$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)$, andthe 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 definewhat 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.$$\begin{array}{l}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))\end{array}$$Usually this is called fold_right or 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.