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))$? – Andrej Bauer 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. – Andrej Bauer 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. – Andrej Bauer 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. – Andrej Bauer Jun 23 '17 at 11:00