Lambda Calculus: Why is the second equation more general than the first?

64 Views Asked by At

I was reading up on lambda calculus from Introduction to Lambda Calculus by Henk Barendregt and Erik Barendsen and came across this:

$(λ~x.f[\textbf{x}])\textbf{x} = f[\textbf{x}]$ more generally one has $(λ~x.f[\textbf{x}])\textbf{N} = f[\textbf{N}]$

Why is the second equation more general than the first?

1

There are 1 best solutions below

3
On BEST ANSWER

My guess in the comment seems to be correct: In

$$(λ\vec x.f[\vec x])\vec x = f[\vec x]$$

the λ-expression is being applied to a list of variables $\vec x$, but in

$$(λ\vec x.f[\vec x])\vec N = f[\vec N]$$

it is being applied to a list of arbitrary terms $\vec N$.

A single variable is the simplest possible special case of a term, as explained in definition 2.1 on page 9.