1
$\begingroup$

I just realised that I have a very trivial/basic question concerning the syntax of Lambda Calculus.

Question 1: Is possible to have brackets between a lambda symbol, i.e., "$\lambda$" and a dot "$.$"?

That is, is possible to have such an expression: $$\lambda x (yz) p. M?$$

I would say yes, since we have to read the $(yz)$ in the example as one term. Thus, by considering two examples, in the first we have $$(\lambda x (yz) p. xyxzp)abc \rightarrow_\beta ayazc,$$ while in the second $$(\lambda x (yz) p. x(yz)p)abc \rightarrow_\beta abc,$$ since we are treating $yz$ as a single term, i.e., with $N \equiv yz$, we have $$(\lambda x (yz) p. x(yz)p)abc = (\lambda x N p. xNp)abc.$$

However, this leads me to a second question, namely:

Question 2: Is $$(\lambda x (yz) p. x(yz)p)abc$$ the same as $$(\lambda x (yz) p. xyzp)abc?$$

This time I would answer no, since an ideal machine would consider the $y$ and the $z$ as two separate terms in $(\lambda x (yz) p. xyzp)abc$. Hence, we would have $$(\lambda x (yz) p. xyzp)abc \rightarrow_\beta ayzc.$$


Thus, is my reasoning correct?

As always, any feedback will be greatly appreciated.
Thank you for your time.

$\endgroup$
3
$\begingroup$

You could maybe make something like this work depending on what you intended it to mean, but it is definitely not common syntax, and you likely have a misconception somewhere. I would recommend minimizing the use of notational shortcuts. Many people get tripped up over the notation of the lambda calculus, and often due the notational shorthands not the "formal" syntax itself. To answer your first question, with respect to virtually all presentations of the untyped lambda calculus, the answer to Question 1 is an unambiguous "no". Question 2 is thus meaningless.

The "official" syntax of a lambda calculus is usually something like $E::= x \mid (\lambda x.E) \mid (E E)$. From there, a variety of shorthands are introduced. The relevant one in this case is that $\lambda xyz.E$ is short for $\lambda x.\lambda y.\lambda z.E$. The "official" syntax simply does not allow anything but a variable to occur between "$\lambda$" and "$.$" (and only allows exactly one). The shorthand just mentioned merely saves the hassle of writing "$\lambda$" multiple times, but it does not change this fact.

There are two ways that I could see allowing something like your syntax, though one I'd handle differently and neither lead to the behavior you describe. First, you could just want to allow multi-character identifiers and the parentheses would indicate that the contents should be treated as one identifier. In programming/specification languages, e.g. Haskell, this is usually handled by requiring whitespace between identifiers though. For example, $\lambda x\ yz\ p.E$. Another possibility is that you are adding pattern matching or at least destructuring binds. Pattern matching allows more complex syntax to appear where $\lambda$-bound variables can appear, but it is usually restricted as otherwise you get into really hairy undecidable and ambiguous territory. In this case, something like $(\lambda (yz).E)b$ would mean $b$ would attempt to be pattern matched against the pattern $yz$, but this is usually not an acceptable pattern. If you are interested in one approach that is fairly flexible in this regard but is not a lambda calculus, you can look at the Pure Pattern Calculus.

$\endgroup$
  • $\begingroup$ Thanks a lot for your detailed answer. Actually I had in mind something related to programming, so your reference to Haskell is particularly nice, even if at the moment I don't know much about that language. Actually, at the beginning I thought that the answer to question 1 was no, but then it was thinking in terms of programming languages that I came with the idea that maybe the answer was going to be yes. $\endgroup$ – Kolmin Apr 27 '18 at 7:32
2
$\begingroup$

The answer to the first question is no, so the second question is meaningless. Let us see why the answer to the first question is negative.

The syntax of the $\lambda$-calculus is \begin{align} M, N ::= x \mid \lambda x.M \mid MN \end{align} which means that:

  • every variable is a term,
  • if $x$ is a variable and $M$ is a term then $\lambda x.M$ is a term,
  • if $M$ and $N$ are terms then $MN$ is a term,
  • anything else is a term.

There is no rule that allows you to say that if $M$ and $N$ are terms then $\lambda N.M$ is a term. So, strictly speaking, given a term $M$, $\lambda xy.M$ is not a term. Conventionally, we set $\lambda x_1 x_2\dots x_n.M$ as a shorthand of $\lambda x_1. \lambda x_2. \dots \lambda x_n.M$.

$\endgroup$
  • $\begingroup$ As always, thanks a lot as always for your answer. As I wrote above as a comment to Derek Elkins answer, funnily enough at the beginning I thought that the answer to question 1 was no, but then it was thinking in terms of programming languages that I came with the idea that maybe the answer was going to be yes. $\endgroup$ – Kolmin Apr 27 '18 at 7:33

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.