2
$\begingroup$

Let's take this lambda expression : $\lambda\:x \:\ast\:x\:2$ that "computes" x * 2.

From what I understand, $\ast$ is a constant operator, but since its nothing else than a symbol, how does that let us compute the multiplication x * 2?

I would have thought that we should have defined $\ast$ as some sort of recursive function for instance, but I can't understand why this is a constant and what is the point of using it if it doesn't directly compute the multiplication?

Thank you

$\endgroup$
  • 1
    $\begingroup$ It's most probably $\lambda x \ldotp 2x$. The dot separate the variable being bounded. In programming terms, it's akin to separating function signature to function body. You should consult a proper text again. $\endgroup$ – Apiwat Chantawibul Jan 30 '17 at 10:36
  • $\begingroup$ @Billiska No, from what I understand $\ast$ was here used as what they call a "constant operator", other papers seem to refer to it as "primitive operators" but the fact that their behaviour isn't defined as a function seems weird to me. $\endgroup$ – Trevör Jan 30 '17 at 10:36
  • $\begingroup$ It would help to show us your reference. As of now, I'm only thinking of basic untyped lambda calculus where a term is either [1] a variable [2] abstraction of term [3] application of terms $\endgroup$ – Apiwat Chantawibul Jan 30 '17 at 10:49
5
$\begingroup$

The “true” lambda calculus is defined by a syntax of terms: $$ M,N ::= x \;\mid\; \lambda x.M \;\mid\; M\,N $$ and a reduction rule called beta reduction: $$ (\lambda x.M)\,N \to M[x \leftarrow N] \tag{$\beta$} $$ (Plus context rules, plus the rules for alpha equivalence, but I'll omit them in this post.)

A lambda term is an object defined by the syntax above. What makes lambda terms interesting is the way they can be evaluated using the reduction rules.

It's possible, and common, to define extensions of the lambda calculus: languages that have additional syntactic forms and reduction rules. One common, simple extension is to add constants to the syntax of terms, and to add reduction rules called delta rules that allow evaluating these constants.

For example, we can define a new calculus which is the lambda calculus plus elementary arithmetic (LCPEA). If $n$ is a non-negative integer, I'll write $(n)_a$ for a constant in the LCPEA, so the LCPEA has constants $(0)_a$, $(1)_a$, $(42)_a$, etc. Note that what's in the parentheses is an integer, not a string: the constant is the same constant regardless of how the integer is written, so $(0)_a$, $(3-3)_a$, $(1+3-2*2)_a$, etc. are all the same constant.

$$ M_a,N_a ::= x \;\mid\; \lambda x.M_a \;\mid\; M_a\,N_a \;\mid\; (n)_a \;\mid\; \mathord{+}_a \;\mid\; \mathord{-}_a \;\mid\; \mathord{*}_a $$ $$ \begin{align} (\lambda x.M_a)\,N_a &\to M_a[x \leftarrow N_a] \tag{$\beta$} \\ \mathord{+}_a (n)_a \, (n')_a &\to (n+n')_a \tag{$\delta_+$} \\ \mathord{-}_a (n)_a \, (n')_a &\to (n-n')_a \qquad \text{if \(n \ge n'\)} \tag{$\delta_-$} \\ \mathord{*}_a (n)_a \, (n')_a &\to (n*n')_a \tag{$\delta_*$} \\ \end{align} $$

The delta rules directly translate the arithmetic operators into the LCPEA. So the LCPEA effectively contains elementary arithmetic. Note that these delta rules are necessary if we want the new constants we introduced to do anything useful. It would have been possible to define a different set of delta rules that caused $+_a$ to have nothing to do with addition and so on, but it would have been confusing.

It turns out that it is possible to define pure lambda terms (i.e. terms in the true lambda calculus) that reduce in the same way as corresponding terms in the LCPEA. That is, we can define a lambda term $\langle n\rangle$ for every natural integer $n$, as well as lambda terms $\langle\mathord{+}\rangle$, $\langle\mathord{-}\rangle$ and $\langle\mathord{*}\rangle$ such that $$ \begin{align} \langle\mathord{+}\rangle \, \langle n\rangle \, \langle n'\rangle &\leftrightarrow_\beta^* \langle n+n'\rangle \\ \langle\mathord{-}\rangle \, \langle n\rangle \, \langle n'\rangle &\leftrightarrow_\beta^* (n-n')_a \qquad \text{if \(n \ge n'\)} \\ \langle\mathord{*}\rangle \, \langle n\rangle \, \langle n'\rangle &\leftrightarrow_\beta^* (n*n')_a \\ \end{align} $$ The Church numerals are a classical example of a set of such terms; there are others.

There are several reasons why we may want to define something like the LCPEA.

  • One is that it is closer to how machines behave; this is important when using the lambda calculus to model compilers, but not when doing theory of computation.
  • Another reason, applicable even when doing theory of computation, is that we often don't care exactly how the integers are encoded. So we might define things like $\langle 3\rangle$ and $\langle\mathord{+}\rangle$ as lambda terms, and then forget their precise definition and just remember some reduction rules for them. So they're still pure lambda terms, but we treat them as if they were part of an extended language.
  • In a typed lambda calculus, encoding everything as functions is problematic, because we'd like to say that something like $1$ is “inert”, not like a function, and to say that $1 \, 2$ (“1 applied to 2”) is not well-typed and does not reduce to anything. With the pure lambda calculus, $\langle 1\rangle \, \langle 2\rangle$ does beta-reduce to something, but not to something useful. When we extend the language with constants, we don't define any reduction rule that would reduce $(1)_a \, (2)_a$.
  • There are extensions of the language that cannot be encoded as lambda terms at all. If we're interested in studying these, we have to extend the language.
$\endgroup$
  • 3
    $\begingroup$ This is so good it could actually be on the rather lacking wikibooks page of on lambda calculus. $\endgroup$ – Apiwat Chantawibul Jan 30 '17 at 19:32
  • 2
    $\begingroup$ @Trevör Anne Denise tl;dr. We are still unsure if you are asking about "true" syntax of lambda calculus or an extended one. So Gilles decided to explained both in details in relation to each other. $\endgroup$ – Apiwat Chantawibul Jan 30 '17 at 19:39
4
$\begingroup$

This particular example seems to have been constructed in an extended language w.r.t. the basic lambda calculus.

Probably your book is just pretending the language is extended with a custom $*$ symbol, which is postulated to perform multiplication.

Usually, arithmetic operators are either postulated (you introduce them as new symbols in the syntax, and you provide an adequate semantics to them) or defined in the language (if numbers are Church-encoded, for instance, one can actually define a $\lambda$-term $*$ which works as expected).

Without knowing the context it's hard to tell.

It's also fairly common to introduce the lambda calculus pretending, for the sake of illustration, that these operators exist. This is because our previous experience about functions is mostly about functions operating on numbers. So it's (arguably) easier to start from there and then work out higher-order functions, and then finally (if we work with the untyped lambda) self-application. At the beginning it can be hard to understand it's functions all the way down, so a gradual step-by-step approach can be beneficial.

$\endgroup$

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.