Lambda Calculus: perché la seconda equazione è più generale della prima?

Question

Stavo leggendo il lambda calcolo da Introduzione al Lambda Calculus di Henk Barendregt ed Erik Barendsen e mi sono imbattuto in questo:

$(λ~x.f[\textbf{x}])\textbf{x} = f[\textbf{x}]$ più in generale si ha $(λ~x.f[\textbf{x}])\textbf{N} = f[\textbf{N}]$

Perché la seconda equazione è più generale della prima?

Answer 1

La mia ipotesi nel commento sembra essere corretta: In

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

l'espressione λ viene applicata a un elenco di variabili $\vec x$, ma in

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

viene applicato a un elenco di termini arbitrari $\vec N$.

Una singola variabile è il caso speciale più semplice possibile di un termine, come spiegato nella definizione 2.1 a pagina 9.