2
$\begingroup$

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!

$\endgroup$
3
$\begingroup$

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

  1. the base case $p(nil)$, and
  2. 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

  1. what is the result in base case, i.e. $f(nil) = a : A$
  2. 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.

$\endgroup$
  • $\begingroup$ Thanks for the answer. Could you explain the meaning of "as the "least" type admitting ", why least? I check books, but did not find why they use least word in many places. $\endgroup$ – alim Jul 24 '17 at 6:36
  • 1
    $\begingroup$ @alim That comes from domain theory, which deals with "least fixed points". The point is that there are many sets admitting a $nil$ and $cons$ operations. For instance take $N^*$ the set of finite natural sequences and $N^\infty$ the set of infinite natural sequences. Then $N^*$ admits the operations, but $N^*\cup N^\infty$ also admits them: $cons$ing over an infinite sequence simply prepends an element. Domain theory, under certain conditions, states there is a "least" set: $N^*$ in this case. This is what we are actually defining. $\endgroup$ – chi Jul 24 '17 at 8:27
  • 1
    $\begingroup$ @alim A more basic example: suppose we require operations $zero$ and $suc$-cessor. The set of natural numbers is the least set admitting those operations. But there are many others which admit those operations: $\mathbb{Z},\mathbb{Q},\mathbb{R}$. However, when in we define something inductively, we really mean the smallest $\mathbb{N}$. $\endgroup$ – chi Jul 24 '17 at 8:29
  • $\begingroup$ thanks :) now it is clear to me. basically to role out these what we don't want. $\endgroup$ – alim Jul 24 '17 at 8:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.