Beta Normalform - Beta normal form

In der Lambda-Rechnung liegt ein Term in Beta-Normalform vor, wenn keine Beta-Reduktion möglich ist. Ein Begriff liegt in Beta-Eta-Normalform vor, wenn weder eine Beta-Reduktion noch eine Eta-Reduktion möglich ist. Ein Begriff ist in Normalform Kopf , wenn es kein Beta-redex in Kopfposition .

Beta-Reduktion

In der Lambda-Rechnung ist ein Beta-Redex ein Begriff der Form:

${\ displaystyle (\ mathbf {\ lambda} xA) M}$ .

A redex ist in Kopflage in einer Laufzeit , wenn die folgende Form hat ( man beachte , dass die Anwendung eine höhere Priorität hat als Abstraktion, und dass die Formel unten ist gemeint , eine Lambda-Abstraktion, nicht eine Anwendung sein): ${\ displaystyle r}$${\ displaystyle t}$${\ displaystyle t}$

${\ displaystyle \ lambda x_ {1} \ ldots \ lambda x_ {n}. \ underbrace {(\ lambda xA) M_ {1}} _ {{\ text {the redex}} r} M_ {2} \ ldots M_ {m}}$ , wo und . ${\ displaystyle n \ geq 0}$${\ displaystyle m \ geq 1}$

Eine Beta-Reduktion ist eine Anwendung der folgenden Umschreiberegel auf einen in einem Begriff enthaltenen Beta-Redex:

${\ displaystyle (\ mathbf {\ lambda} xA) M \ longrightarrow A [x: = M]}$

Wo ist das Ergebnis des Ersetzens des Begriffs für die Variable im Begriff . ${\ displaystyle A [x: = M]}$${\ displaystyle M}$${\ displaystyle x}$${\ displaystyle A}$

Eine Kopf- Beta-Reduktion ist eine Beta-Reduktion, die in der Kopfposition angewendet wird, dh in der folgenden Form:

${\ displaystyle \ lambda x_ {1} \ ldots \ lambda x_ {n}. (\ lambda xA) M_ {1} M_ {2} \ ldots M_ {m} \ longrightarrow \ lambda x_ {1} \ ldots \ lambda x_ {n} .A [x: = M_ {1}] M_ {2} \ ldots M_ {m}}$ , wo und . ${\ displaystyle n \ geq 0}$${\ displaystyle m \ geq 1}$

Jede andere Reduzierung ist eine interne Beta-Reduzierung.

Eine normale Form ist ein Begriff, der kein Beta-Redex enthält, dh das nicht weiter reduziert werden kann. Ein Kopf Normalform ist ein Begriff, der kein beta redex in Kopfposition nicht enthält, dh , die durch einen Kopf Reduktion kann nicht weiter reduziert werden. Bei der Betrachtung des einfachen Lambda-Kalküls (dh ohne Hinzufügen von Konstanten- oder Funktionssymbolen, die durch eine zusätzliche Delta-Regel reduziert werden sollen) sind Kopfnormalformen die Begriffe der folgenden Form:

${\ displaystyle \ lambda x_ {1} \ ldots \ lambda x_ {n} .xM_ {1} M_ {2} \ ldots M_ {m}}$ , wo ist eine Variable, und . ${\ displaystyle x}$${\ displaystyle n \ geq 0}$${\ displaystyle m \ geq 0}$

Eine Kopfnormalform ist nicht immer eine Normalform, da die angewendeten Argumente nicht normal sein müssen. Das Gegenteil ist jedoch der Fall: Jede Normalform ist auch eine Kopfnormalform. Tatsächlich sind die Normalformen genau die Kopfnormalformen, in denen die Subterme selbst Normalformen sind. Dies gibt eine induktive syntaktische Beschreibung von Normalformen. ${\ displaystyle M_ {j}}$${\ displaystyle M_ {j}}$

Es gibt auch den Begriff der schwachen Kopfnormalform : Ein Begriff in schwacher Kopfnormalform ist entweder ein Begriff in Kopfnormalform oder eine Lambda-Abstraktion. Dies bedeutet, dass ein Redex in einem Lambda-Körper auftreten kann.

Reduktionsstrategien

Im Allgemeinen kann ein bestimmter Begriff mehrere Redexes enthalten, daher können mehrere verschiedene Beta-Reduktionen angewendet werden. Wir können eine Strategie festlegen, um zu entscheiden, welcher Redex reduziert werden soll.

• Reduktion normaler Ordnung ist die Strategie, bei der die Regel für die Beta-Reduktion der Kopfposition kontinuierlich angewendet wird, bis solche Reduzierungen nicht mehr möglich sind. Zu diesem Zeitpunkt liegt der resultierende Term in Kopfnormalform vor. Man setzt dann die Kopfreduktion in den Subtermen von links nach rechts fort. Anders ausgedrückt ist die Reduzierung normaler Ordnung die Strategie, die immer zuerst den äußersten äußersten linken Redex reduziert. ${\ displaystyle M_ {j}}$
• Im Gegensatz dazu wendet man bei der reduzierten Auftragsreduzierung zuerst die internen Reduzierungen an und wendet dann die Kopfreduzierung nur an, wenn keine internen Reduzierungen mehr möglich sind.

Die Reduktion normaler Ordnung ist vollständig, in dem Sinne, dass, wenn ein Begriff eine Kopfnormalform hat, die Reduktion normaler Ordnung sie schließlich erreichen wird. Nach der obigen syntaktischen Beschreibung von Normalformen bedeutet dies dieselbe Aussage für eine „vollständig“ normale Form (dies ist der Standardisierungssatz ). Im Gegensatz dazu kann die Reduzierung der anwendbaren Reihenfolge möglicherweise nicht beendet werden, selbst wenn der Begriff eine normale Form hat. Beispielsweise ist unter Verwendung der reduzierten Auftragsreduzierung die folgende Folge von Reduzierungen möglich:

${\ displaystyle {\ begin {align} & (\ mathbf {\ lambda} xz) ((\ lambda w.www) (\ lambda w.www)) \\\ rightarrow & (\ lambda xz) ((\ lambda w .www) (\ lambda w.www) (\ lambda w.www)) \\\ rightarrow & (\ lambda xz) ((\ lambda w.www) (\ lambda w.www) (\ lambda w.www) (\ lambda w.www)) \\\ rightarrow & (\ lambda xz) ((\ lambda w.www) (\ lambda w.www) (\ lambda w.www) (\ lambda w.www) (\ lambda) w.www)) \\ & \ ldots \ end {align}}}$

Bei Verwendung der Reduktion normaler Ordnung reduziert sich derselbe Ausgangspunkt jedoch schnell auf die normale Form:

${\ displaystyle (\ mathbf {\ lambda} xz) ((\ lambda w.www) (\ lambda w.www))}$

${\ displaystyle \ rightarrow z}$

Sinots Director-Strings sind eine Methode, mit der die rechnerische Komplexität der Beta-Reduktion optimiert werden kann.

Siehe auch

• Lambda-Kalkül
• Normalform (Begriffsklärung)

Verweise