Let us consider the following lambda expression :

$ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$

so $ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$ can be seen as $ (\lambda func.(\lambda arg$ $( func$ $ arg))$ $\lambda x.x)$ and will be in a form $ (\lambda x$$.M) N$ form.

As such this can be perceived to be a function which is taking $ N $ as an argument . Hence here $ func $ takes the value of the argument .

Now $ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$ , if I am not wrong can also be seen as

$ (\lambda func.((\lambda arg$ $( func$ $ arg))$ $\lambda x.x))$ and can be seen in a form $ \lambda func.($ $( \lambda x .M)N$) thereby $x$ taking the value of the argument .

Now by church rosser theorem both the beta reductions should lead to equivalent expressions , however here the argument being taken up by two different bound variable makes me doubt the semantic consistency .

How is the semantic inconsistency , resolved ? (I think this might be stemming from some big gap in my understanding )

  • 1
    $\begingroup$ This has nothing to do with semantics, you need to get your syntax straight. To clarify the question please explain whether $(\lambda func . \lambda arg . (func \ arg) \lambda x . x)$ is supposed to mean $(\lambda func . (\lambda arg . (func \ arg)) (\lambda x . x))$ or $(\lambda func . (\lambda arg . ((func \ arg) (\lambda x . x)))$. Use lots of parentheses. Also, your notation is unreadable because you are using long names $func$ and $arg$. It would be better to write $\lambda f . \lambda a . (f a) (\lambda x . x))$. $\endgroup$ – Andrej Bauer Mar 8 '18 at 21:47
  • 1
    $\begingroup$ I guess my point is this: you are suggesting two different readings of an expression. The two different meanings arise from notational confusion which is caused by lack of parentheses. People like to leave out parentheses, but in case of confusion such parentheses must be put back in. If you do that for the two alternative readings of your expression, you will simply obtain two different expressions. There is nothing wrong with these two having different reduction sequences. There is no problem, other than a confusion on what your starting expression is supposed to be. $\endgroup$ – Andrej Bauer Mar 8 '18 at 21:55
  • $\begingroup$ @AndrejBauer You can turn this into an answer. $\endgroup$ – Aristu Mar 15 '18 at 12:45
  • $\begingroup$ @AndrejBauer : Sure Aandrej , how to do it ? Shall Ii post it myself or is there anywhere I can click to accept this as an answer ? $\endgroup$ – Agnivesh Singh Mar 17 '18 at 14:49

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.