Well, let's have the various ways for representing recursive functions.
The crucial ingredient is the fix point operator, which allows to define
functions by recursions by doing that as a fix point of a suitable operator.
The fix point, you see, has a very simple syntax is enough to formulate
such a complicated concept.
There is another way of encoding the fix point recursive function and
this is by introducing suitable constance called the recursors, regulated
by special reduction rules, called d-reduction rules.
So suppose you introduce the special constance of natural numbers, as
a 0 and successor, then you can define a new constant a recursor, which,
given two parameters a and b, allows you to define a function on by recursion.
|
|