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?

• 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
• @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?
• 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