# Recursive definitions, How it is done?

I read that recursive definitions, refer to the definition of a function in that function body, cannot be done in $\lambda$-calculus, but recursion can be achieved by using $Y$ combinator.

As I know, nominal logic is the theory of handling bindings. So wondering how it handles recursive definition of functions? Does it still use combinators as it is done in $\lambda$-calculus? nominal logic

I think higher-order abstract syntax takes the same approach taken by $\lambda$-calculus, since it is based on $\lambda$-calculus. am I right?

If there is a good technique for handling recursive definition different than using a combinator as mentioned above, Please point it out. I want to know. What is the common way to handle recursion?

Could anyone clarify these to me, please? Thanks in advance.

• Do you realize that the $Y$ combinator can be defined in $\lambda$-calculus as $Y = \lambda f . (\lambda x . f (x x)) (\lambda x . f (x x))$? Jun 22 '17 at 16:50
• I do not understand what you're asking. What do you mean by "handle recursive definitions"? How to express them? How to compute fixed points? Please be more specific. Jun 22 '17 at 16:51
• @AndrejBauer I know that $Y$ combinator can be defined and used to implement recursion in $\lambda$-calculus. I am asking that is this the case for nominal logic? How recursion defined in nominal logic? Does it use $Y$ Combinator as well?
– alim
Jun 22 '17 at 17:35
• In that case it would be helpful if you give a reference to a specific nominal logic as you could have in mind any number of variants. Jun 22 '17 at 20:17
• Ok, so you are referring to Andy Pitt's nominal logic. Please note that this is not a calculus of functions, i.e., it's not comparable to $\lambda$-calculus in a direct way. Instead it's a kind of non-standard set theory. As such it does not support unrestricted recursion. But there is nominal domain theory, which does, you can look that up. Jun 23 '17 at 11:00