Intuitive Erklärung der neutralen / normalen Form im Lambda-Kalkül

Es ist möglich, normale Begriffe, die Beta-Redex nicht als Unterausdruck enthalten, von anderen zu unterscheiden

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)

Gibt es eine intuitive Erklärung, warum diese Eigenschaft gelten würde? Es mag irgendwie völlig selbstverständlich sein, wenn man es lange genug betrachtet, aber es fordert mich ab sofort nicht direkt auf.

Ich kann Ihnen versichern, dass diese Eigenschaft nicht sofort selbstverständlich ist. Bei dem Versuch, die Menge der Normalformen zu beschreiben / aufzuzählen, ist folgende Hauptbeobachtung erforderlich:

• Bei der Abstraktion bleiben normale Formen erhalten: Wenn normal ist, ist dies auch .$t$$\lambda x.t$

• Die Anwendung bewahrt keine normalen Formen: Wenn und normal sind, kann einen Redex enthalten!$t$$u$$t\ u$

Wir möchten die normalen Formulare charakterisieren, für die wir bei der Ausführung von Anwendungen keine Redexes erstellen können . Offensichtlich tritt dies auf, wenn eine Abstraktion ist. Insbesondere können wir als alles betrachten, was wir wollen, solange es in normaler Form ist.$t$$\lambda$$u$

Für benötigen wir entweder eine Variable oder eine Anwendung, die sich bereits in normaler Form befindet. Dies ermöglicht eine bequeme rekursive Definition für , die wir neutral nennen werden : oder mit jeder normalen Form und auch in normaler Form, dh auch ein neutraler Term.$t$$t$

$$t=x$$ $$t=t_1\ t_2$$ $t_2$$t_1\ t_2$$t_1$

Aber das ist genau deine Definition von Neutral!

Man kann diesen Prozess weiter ausführen, um genau die normalisierenden (bzw. stark normalisierenden) Terme zu charakterisieren, wenn wir weiterhin schwache Kopfausdehnungen zulassen .