2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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))$? $\endgroup$ – Andrej Bauer Jun 22 '17 at 16:50
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jun 22 '17 at 16:51
  • $\begingroup$ @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? $\endgroup$ – alim Jun 22 '17 at 17:35
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jun 22 '17 at 20:17
  • 3
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jun 23 '17 at 11:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.