1

In lambda calculus, application is left associative. That is, if M, N, and P are expressions, then we parse MNP1 as (MN)P. But if we want the "alternative" parsing, we can get it using parentheses/grouping: M(NP).

Conversely, abstraction is right associative. That is, if x and y are variables, then we parse λx.λy.M2 as λx.(λy.M). Is there an "alternative" parsing to λx.λy.M? Does (λx.λy).M makes sense? If not, can you give an example of a valid "alternative" parsing of chained abstractions where parenthesis would have to be used to the get the "alternative" parsing?

1 My understanding is that when we see two expressions next to each other as in MN there is an implied application operator between them which says "apply M to N" or more verbosely "feed N as input to M". Is this correct? If so, a phrase like "M something N" is desirable so we can read lambda expressions left to right. Maybe "M consumes N"?

2 In this case it looks like the dot (.) is acting as the abstraction operator. Is there a way to verbalize λx.M left to right? Something like "function (λ) taking x outputing (.) M"?

joseville
  • 1,477

1 Answers1

2

No. A term in the lambda calculus is either:

  • A variable -- that is an identifier
  • An application -- that is a pair of two terms
  • A lambda abstraction -- that is a term depending on a chosen identifier

So concretely, a term is represented by a tree where leaves are always variables, binary nodes are applications, and unary nodes (indexed by an identifier) are lambda abstractions. For example: $$\texttt{Lam}(x,\texttt{Lam}(y,M))$$ where $M$ may depend on $x,y$, or $$\texttt{Lam}(y,\texttt{App}(\texttt{Lam}(x,\texttt{Var}(x)),\texttt{Var}(y))).$$

This means that $\lambda x. t$ is just a way of writing $\texttt{Lam}(x,t)$, and the dot has no semantic value.

But now let's consider an alternative way of representing terms. A term is now either:

  • A variable -- that is an identifier
  • An application -- that is a pair of two terms
  • A lambda abstraction -- that is a term valued function

The key difference now is that a lambda abstraction is given by a lambda abstraction $ x\mapsto M$ in the meta-language, so we might as well write $x . M$ and the examples above are now:

$$\texttt{Lam}(x . \texttt{Lam}(y . M))$$ and $$\texttt{Lam}(y.\texttt{App}(\texttt{Lam}(x . \texttt{Var}(x)), \texttt{Var}(y))).$$ So now, $\lambda x . t$ could be parsed $\lambda (x . t)$, where $x . t$ is a function $x \mapsto t$ in the meta language.

Furthermore, if $f$ is a function producing a term, it would also be valid to write $\lambda f$, which in turn is equivalent to $\lambda (x\mapsto (f x))$, which we may write $\lambda(x.(f x))$ or $\lambda x. (f x)$.

Couchy
  • 2,722
  • thanks. I'm trying to understand. Lam(x, Lam(y, M)) is λx.λy.M. Do I have the following correct?: 1. If M = Var(x), then the tree is: https://bit.ly/3B7zudA 2. If M = Var(y), then the tree is: https://bit.ly/2XwHIy6 3. If M = App(Var(x), Var(y)), then the tree is: https://bit.ly/3GbsboU 4. If M = Var(z), then the tree is: https://bit.ly/3m20JSA – joseville Oct 21 '21 at 17:58
  • again thanks. Would the tree for (,((,()),())) look like this: https://bit.ly/3E1cnmS, or more verbosely, but equivalent: https://bit.ly/2ZkGrep. – joseville Oct 21 '21 at 18:06
  • What is the significance of the meta language? – joseville Oct 21 '21 at 18:12
  • 1
    @joseville This is the right way to look at it: https://bit.ly/3m3lvRH. Again, the dot is just syntactic sugar, it is not a node in the tree. The reason the arrows shouldn't have $Var$ is that they are not indexed by variables, but by identifiers. The meta language is the language of discourse, ie. that you use when doing mathematics. – Couchy Oct 21 '21 at 19:09
  • 1
    @joseville Looking back at your diagrams, I think you may be confusing the parse (concrete syntax) tree and abstract syntax tree. The trees I am referring to are abstract syntax trees. The parse tree is a verbatim representation of the symbols you write (hence the dot is significant), whereas this is abstracted away in the abstract syntax tree. – Couchy Oct 21 '21 at 19:29
  • thanks. Is "(.()" missing the closing paren? In the notation (,((,()),())), and represent binary operations - the two operands are separated by comma (,) and represents a unary operation. Furthermore, the first operand of and the only operand of must be a variable (or identifier?). Is there a distinction between variable and identifier? Is () the variable whilst is the identifier (is not considered a variable)? – joseville Oct 21 '21 at 19:48
  • 1
    The distinction between an identifier and a variable is that a variable is a term, and an identifier (or string) is not. So while $Lam$ is binary, the first argument is an identifier, not a term, so it behaves like a unary node on terms. Yes, $x$ is an identifier, while $Var(x)$ is the variable. For more consistency, https://bit.ly/3lYaiSt is more accurate because the circles are all terms. – Couchy Oct 21 '21 at 19:52
  • Going from the first notation to the second (e.g. (.((.()),())) ), it looks like the only transformation is that the comma (,) in all ( , ) gets replaced with a dot (.). Both these notations are along the same line as prefix notation where the binary operator is written, followed by the two operands. The final notation (e.g. y.((x.x)y)) seems to mix prefix notation for abstractions (if is considered the binary operator) and implicit infix notation for the applications (MN <=> (M, N)) . – joseville Oct 21 '21 at 19:57