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.