Explicação intuitiva da forma neutra / normal no cálculo lambda

É possível distinguir termos normais que não contêm beta redex como uma sub-expressão, de outros como esses

data WithBound a = Var | Other a

data Normal a
  = Neutral (Neutral a)
  | Abstract (Normal (WithBound a))

data Neutral a
  = Variable a
  | Apply (Neutral a) (Normal a)

Existe alguma explicação intuitiva sobre por que essa propriedade seria válida? Pode ser totalmente evidente de alguma forma, depois que você o olha por tempo suficiente, mas não me aparece diretamente a partir de agora.

Posso garantir que essa propriedade não é imediatamente evidente por si mesma. Ao tentar descrever / enumerar o conjunto de formas normais, a principal observação necessária é a seguinte:

• Abstração preserva formas normais: se $t$ é normal, então $\lambda x.t$.

• O aplicativo não preserva as formas normais: se$t$ e $u$ são normais $t\ u$ pode conter um redex!

Queremos caracterizar os formulários normais para os quais não podemos criar redexes ao executar aplicativos . Obviamente, isso ocorre se$t$ é um $\lambda$-abstração. Em particular, podemos tomar$u$ ser o que quisermos, desde que esteja na forma normal.

Para $t$, precisamos de uma variável ou de um aplicativo, já em forma normal. Isso permite uma definição recursiva conveniente para$t$, que chamaremos de neutros :

$$t=x$$ ou $$t=t_1\ t_2$$ com $t_2$ qualquer forma normal e $t_1\ t_2$ também na forma normal, ou seja, $t_1$ também um termo neutro.

Mas esta é exatamente a sua definição de Neutral!

Pode-se levar adiante esse processo para caracterizar exatamente os termos de normalização (resp. Normalização fortemente), se permitirmos, além disso, expansões fracas da cabeça .