0

In the $\lambda$-calculus expression:

$$ (\lambda x.\lambda y.xy)(f(f(a))) $$

Can the subexpression $(f(f(a))$ be split into two terms, $M$ and $N$? (Maybe, via $\alpha$-conversion?) If so, what could those two terms be? $f$ and $fa$? $ff$ and $a$?

Suppose it is possible. Then we'd have $(\lambda xy.xy)(MN)$. Are the following steps valid?:

\begin{align} (\lambda xy.xy)(MN) \\ (\lambda xy.xy)MN \\ ((\lambda xy.xy)[x:=M])N \\ (\lambda y.My)N \\ (\lambda y.My)[y:=N] \\ MN \end{align}

Is the second step above valid? I.e. is it valid to go from $(\lambda xy.xy)(MN)$ to $(\lambda xy.xy)MN$?

joseville
  • 1,477
  • 1
    There's default parenthesis association rules in λ-calculus and also default application sequence for curried function abstraction, order matters. What rule or reference you can backup your step 2? Without your step 2, the result is totally different and still have λ redex. – cinch Oct 23 '21 at 03:43
  • Application is left-associative so $(\lambda xy.xy)MN$ means $((\lambda xy.xy)M)N$? I guess step 2 is invalid. Would the correct $\beta$-reduction of $(\lambda xy.xy)(MN)$ be $(\lambda xy.xy)[x:=MN]$? I'm new to it, so not sure I understand "default application sequence for curried function abstractions". I do understand that $\lambda xy.xy$ is shorthand for $\lambda x.(\lambda y.xy)$ though. – joseville Oct 23 '21 at 03:53

1 Answers1

1

You're almost right in above comment. Application is left-associative so to be ensured one can arrive at a normal form (but in some cases may not be necessary). "$λxy.xy$ is shorthand for $λx.(λy.xy)$" this is what I mean a "curried function abstraction". Yes, the result should be $λy.(MN)y$, which is $λy.((MN)y)$ strictly speaking for your example. If you're new, you'd better always add default parenthesis when confused, never delete though.

cinch
  • 1,648
  • 1
  • 4
  • 12
  • thanks! And re: $(f(f(a)))$. Can you confirm that it can be expressed as $MN$ where $M = f$ and $N = f(a) = fa$? And can you confirm that $(f(f(a)))$ cannot be expressed as $MN$ where $M = f(f)= ff$ and $N = a$? I have been playing around with Church number where $f(f(f...(a)...)))$ is common as you know. Is there a shorthand for repeated application of a term like that? Maybe $f(f(f(a)))$ can be shorthanded as $f^3(a)$? – joseville Oct 23 '21 at 04:11
  • 1
    @joseville Very similar to functional programming, $M=f=λx.Mx$ which is a higher-order function, while $N=f(a)$ is just a variable term. Thus if defined as such, of course it makes sense to write $f(f(a))=MN$ (the result is not a function), but your other defs cannot well form an equivalent term. As for Church encoding in the reference, you can use symbol $f^{0n}$ for the n-fold composition of a function itself... – cinch Oct 23 '21 at 04:19
  • thanks. Does $M = \lambda x.Mx$ in general? – joseville Oct 23 '21 at 04:45
  • 1
    @joseville yes, see ref here for example. – cinch Oct 23 '21 at 06:57