0
$\begingroup$

I encountered the following exercise in a textbook about logic:

$\lambda x \lambda Y(Y(x))(j)(M)$

It seems that the expected result from the textbook should be $M(j)$, since there were some type specifications on the variables. However, if I substitute $M$ for $x$, and $j$ for $Y$, then the result would become $j(M)$, which would be erroneous in terms of type.

I've seen elsewhere expressions such as:

(λa.λb.λs.λz. a s (b s z)) x y →
(λb.λs.λz. x s (b s z)) y →
λs.λz. x s (y s z)

which seems to have the same application order of arguments as the one desired by this exercise.

It actually seems to make sense if I think of function application in Haskell, but I still find it weird since I expect the rightmost argument to be substituted first for the leftmost lambda term.

Therefore, does the notation $\lambda x \lambda Y(Y(x))(j)(M)$ implicitly entail $\lambda x (\lambda Y(Y(x))(j)(M))$, which would yield the desired result? Is such implicit omission of brackets a normal convention in lambda calculus, and thus every such expression should be treated as such? Or did I misunderstand the order of argument application in lambda calculus after all?

$\endgroup$
  • $\begingroup$ That notation is quite unusual in my eye. It seems to require parentheses after the lambdas, instead of before them. In more common notation, that would be written as $(\lambda x\lambda Y. Y x) j M$. Note that in lambda-c. you often can't omit parentheses. It seems that your book (which one?) uses $\lambda x\lambda y.(body\ here)$ instead of the more common $(\lambda x\lambda y. body\ here)$. $\endgroup$ – chi Jan 25 '17 at 23:13
  • $\begingroup$ @chi This is a semantics book instead of a computer science one. So maybe it's possible that a different convention is more prevalent there. Gamut, L. T. F. Logic, Language, and Meaning: Intensional logic and logical grammar. Vol. 2. University of Chicago Press, 1991. p. 108/111. $\endgroup$ – xji Feb 2 '17 at 11:39
  • $\begingroup$ I see. By the way, I would definitely classify a semantics book as a computer science book. Computer science is quite wide and surely programming languages semantics is a classical area in CS. :) Still, the notation of the book is a bit different than some other books e.g. Barendregt. (Not a big deal, of course) $\endgroup$ – chi Feb 2 '17 at 18:06
3
$\begingroup$

It seems that your book uses the notation $$ \lambda x_1 \ldots \lambda x_n (M_1 \ldots M_k) $$ instead of the more commonly found (in my experience) $$ (\lambda x_1 \ldots \lambda x_n. M_1 \ldots M_k) $$ Both notations are used for logical quantifiers by different authors, so it's not completely surprising. E.g., compare $$ \exists x (P(x) \land Q(x)) \qquad {\rm vs} \qquad (\exists x. P(x) \land Q(x)) $$

In the second style, the scope of binders ($\lambda x$, $\exists x$) extends as far to the right as possible.


About application order: the notation of your book $$ \lambda x_1 \lambda x_2 \lambda x_3 (M) N_1 N_2 N_3 $$ stands for $$ (((\lambda x_1 (\lambda x_2 (\lambda x_3 (M)))) N_1) N_2) N_3 $$ It is correct that the outermost application is of $N_3$ but this does not get bound to $x_1$. To see where $M_3$ goes, one first needs to reduce the function $$ ((\lambda x_1 (\lambda x_2 (\lambda x_3 (M)))) N_1) N_2 $$ to a lambda, and this involves applying $N_2$ first. That will require applying $M_1$ first, in turn.

The net effect is that $N_i$ gets bound to $x_i$.

Since you mentioned the Haskell notation, it is basically the same thing, even if Haskell uses the other notation (binders extend to the right as possible).

$\endgroup$
  • 2
    $\begingroup$ Note the example from the book isn't using "." at all. Presumably the rule is $\lambda xyz$ means $(\lambda x.y)z$ in more common notation. With this rule the example is $(\lambda x.\lambda Y.Y x)jM$ using more common conventions. Incidentally, I've read at least one work that used "." generally for "scope as far right as possible" though using it was not required. It had expressions like $P\land . Q\lor R$ for $P\land(Q\lor R)$. I don't endorse such notation though. $\endgroup$ – Derek Elkins Jan 26 '17 at 4:48
  • $\begingroup$ Thanks for the explanation. So in your expression $(((\lambda x_1 (\lambda x_2 (\lambda x_3 (M)))) N_1) N_2) N_3$, does $M$ contains all the $M_1$ and $M_2$ etc. you mentioned later? $\endgroup$ – xji Feb 2 '17 at 11:37
  • $\begingroup$ @JIXiang In my second example $M$ can be anything, including the application $M_1 M_2 \ldots$. $\endgroup$ – chi Feb 2 '17 at 18:03

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.