Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
I saw in this question a reference to $\mu$-recursive functions or $\mu$-calculus as some computation model equivalent to Turing machines and $\lambda$-calculus. I know about these two but never heard of $\mu$-calculus. Can you briefly describe it and compare it with the other models? Bonus points for link references and books for beginners. Thanks in advance.
Edit: Ok, just for clarification i'm interested in both $\mu$-recursive functions and $\mu$-calculus.
If it is the μ-recursive functions you are interested in (and not the μ-calculus, which is a totally different thing as slimton pointed out) it makes the most sense if you start looking at the primitive recursive functions (PRFs). The set of PRFs is interesting in it self and it turns out that the μ-recursive functions can be introduced by an extension of it.
Here are some slides that seems to be a relatively gentle introduction: Link
The two topics are, as mentioned, quite different. The $\mu$-recursive functions occur in computability theory. The $\mu$-calculus is a logic. Here is a very simple (I hope) description, in keeping with your request.
Regarding $\mu$-recursion: you can ask, if we viewed Turing machines as defining mathematical functions, what kind of functions do you have? The machine has a value $x$ on its input tape and writes a value $f(x)$ on its output tape. A Turing machine is not guaranteed to terminate. What does this mean for the function represented? It means that Turing machines encode partial functions. Which class of partial functions? Do they have a nice inductive definition, built up from simpler functions and composition operations? The answer to both these questions is given by the class of $\mu$-recursive functions. I assume most computability textbooks will contain details. The book by Boolos Burgess and Jeffrey worked for me.
Now for the $\mu$-calculus. Think of the behaviour of a discrete dynamic system like a program or any computing device. The device has a state consisting of the current control location and the contents of various data storage mechanisms. The behaviour of the device is encoded by a transition relation between states. This is exactly the transition relation, if you have a finite automation. For more complex devices, it is the relation between two states when the device makes a step. Suppose you want to logically specify the behaviour of such a device.
One way to think of this is to label states. For example, if you have a pushdown automaton and are interested in states where a symbol $a$ is on top of the stack, you could label such states "$aTop$". Say you want to logically express the set of states from which you can reach a state with $a$ on top of the stack. Modal logic has an operator $\Diamond$, pronounced "next". The formula $\Diamond \theta$ is true in a state $s$ if $s$ has a successor satisfying $\theta$. The set of states that in up to $2$ steps lead to $a$ on top of the stack are $(aTop \vee \Diamond aTop \vee \Diamond \Diamond aTop)$. You can keep nesting formulae to express reaching a state with $a$ on top in $k$ steps. To capture all such states, one introduces recursion and writes: $\mu X. (aTop \vee \Diamond X)$.
A $\mu$-calculus is a system of function symbols with fixed point operators. The most popular $\mu$-calculus is the modal $\mu$-calculus, an extension of modal logic with fixed point operators. The survey by Bradfield and Stirling is a good introduction.
