2
$\begingroup$

I'm trying to find a scheme to translate a functional language with let rec into a set of primitives called "generalized arrows", i.e. $\kappa$-calculus with extensions. The problem is that general recursion is not expressible in $\kappa$-calculus, so I had to extend it with minimization operator.

There is a previous question asking about translation of Ackerman function into $\mu$-recursive operators, but the solution of Klaus Draeger doesn't seem to me to be generalizable.

Is there any previous work on translating general recursion into a set of $\mu$-recursive operator applications?

|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ I'm not really familiar with generalized arrows, but the principle of that answer should be generalizable: what you need to do is encode the call stacks using pairing functions, define one-step evaluation (using projection and pairing for popping/pushing), define n-step evaluation via primitive recursion, and use mu-recursion to find the terminal state. $\endgroup$ – Klaus Draeger May 27 '14 at 12:41
  • $\begingroup$ @KlausDraeger Sounds great. Please, could you describe it a bit further as an answer? $\endgroup$ – polkovnikov.ph May 27 '14 at 13:23
  • $\begingroup$ @KlausDraeger I got it. We could just define a generalized algebraic data type $T$, where each constructor $C_i : Either\ T\ a_1 \rightarrow Either\ T\ a_2 \rightarrow \dots$ corresponds to original function $f_i : a_1 \rightarrow a_2 \rightarrow \dots$, then translate program into partially recursive function on that datatype. (Or something like that.) I'll try to figure it out in Haskell. $\endgroup$ – polkovnikov.ph May 27 '14 at 13:33
  • 2
    $\begingroup$ Please turn your comment into an answer. This can serve as a template for similar questions. $\endgroup$ – cody May 27 '14 at 18:33
  • $\begingroup$ (Back then I was actually looking for point-free representations of recursion, and asked this question to gain some intuition on the topic. There was a limit operation of type ((a \/ c) ~> (b \/ c)) -> (a ~> b) in generalized arrows for this purpose, I just couldn't realize it.) $\endgroup$ – polkovnikov.ph Feb 17 '18 at 15:08
1
$\begingroup$

Klaus Draeger’s method can be fairly easily generalized, we just need one more piece to make it fully functional - a code stack. If we add in a code stack to the state, we can suddenly push things, or run multiple functions in one stack machine. The code would have only a few basic operators, a push operation and functions that are externally paired with a mu-recursive function. The mu-recursive functions take in some number of items from the top of the stack and return some items to be pushed to the stack and some code to be pushed to the code stack. To illustrate all of this, here’s an example of an addition function being defined within the machine. We will use two functions, the successor function and the addition function itself. The successor function is easy enough to define, just S(n) = <[S(n)],[]>, where <,> is the pairing function, the lists are encoded in the obvious way, and the S(n) within the definition is the standard successor function. The first list in the pair is what is pushed to the stack, and the second list is what is pushed to the code stack. More interestingly, the addition function is defined as +(0,m) = <[m],[]> and +(S n,m) = <[n,m],[+,S]>. The push operation is defined in the obvious way, push x pushes x to the stack and removes the instruction, as with every other instruction. One may ask after all this, “why is this modification required for everything but the ackermann function?” Well, simply, if you use this method to encode the ackermann function, you see that the only thing in the code stack at any point is just a string of ackermann functions, so you can simplify in the ackermann case, assume there’s nothing in the code stack but an infinite string of ackermann functions, and then eliminate the code stack entirely, using the empty stack to let you know once it’s finished evaluating.

|cite|improve this answer
$\endgroup$
1
$\begingroup$

You seem to be looking for the origin of a theorem that allows the simplification of a set of recursive definitions to a single recursive function definition. Apologies if I misread that. On with answering the question I think you asked.

The crucial year seems to be 1969. Three teams (where I take the liberty of calling some individuals teams) came up with important contributions to the theory of recursion as it matters to program semantics. As I helped to write elsewhere:

"In general, recursion appears in the form of a system of so-called mutually recursive procedures, for instance, procedure $S$ with body $P (S,T)$ and procedure $T$ with body $Q (S,T)$. The semantics of $S$ can now be expressed by $$\mu X.P (X,\mu Y.Q (X,Y))$$ and, similarly, $T$ is characterized by $$ \mu Y.Q (\mu X.P (X,Y),Y)~,$$ a result of [Bekic69][1], [Scott.deBakker69][2], and [Park70][3]."

[1]: Hans Bekic. Definable operations in general algebra, and the theory of automata and flow charts. Unpublished notes, IBM Laboratory Vienna, 1969.

[2]: Dana S. Scott and Jaco W. deBakker. A theory of programs. Seminar notes, IBM Seminar, Vienna, 1969.

[3]: David M. R. Park. Fixpoint induction and proofs of program properties. Machine Intelligence, 5:59–78, 1969.

|cite|improve this answer
$\endgroup$

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.