Beta normální forma - Beta normal form

V lambda kalkulu je termín v beta normální formě, pokud není možné snížení beta . Termín je v normální formě beta-eta, pokud není možné snížení beta ani snížení eta . Termín je v normální formě hlavy, pokud v poloze hlavy není beta-redex .

Snížení beta

V lambda kalkulu je beta redex výrazem ve formě:

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

Redex je v pozici hlavy v termínu , pokud má následující tvar (všimněte si, že aplikace má vyšší prioritu než abstrakce a že níže uvedený vzorec má být lambda-abstrakce, nikoli aplikace): ${\ 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}}$ , kde a . ${\ displaystyle n \ geq 0}$${\ displaystyle m \ geq 1}$

Snížení beta je aplikace z následujícího pravidla pro přepis na beta REDEX obsažené v termínu:

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

kde je výsledek nahrazení termínu proměnnou v termínu . ${\ displaystyle A [x: = M]}$${\ displaystyle M}$${\ displaystyle x}$${\ displaystyle A}$

Hlava snížení beta je snížení beta aplikovat v poloze hlavy, to znamená, že v následující 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}}$ , kde a . ${\ displaystyle n \ geq 0}$${\ displaystyle m \ geq 1}$

Jakákoli jiná redukce je interní beta redukce.

Normální forma je termín, který neobsahuje žádný beta REDEX, tzn , že nemůže být dále snížena. Hlava normální forma je termín, který neobsahuje beta REDEX v poloze hlavy, tj , které nemohou být dále snížena snížením hlavy. Když vezmeme v úvahu jednoduchý lambda kalkul (viz. Bez přidání konstantních nebo funkčních symbolů, které mají být redukovány dalším pravidlem delta), jsou normální tvary hlavy pojmy následujícího tvaru:

${\ displaystyle \ lambda x_ {1} \ ldots \ lambda x_ {n} .xM_ {1} M_ {2} \ ldots M_ {m}}$ , kde je proměnná, a . ${\ displaystyle x}$${\ displaystyle n \ geq 0}$${\ displaystyle m \ geq 0}$

Normální forma hlavy není vždy normální forma, protože použité argumenty nemusí být normální. Opak je však pravdou: jakákoli normální forma je také normální hlavou. Ve skutečnosti jsou normální formy přesně hlavními normálními formami, ve kterých jsou podmnožiny samy o sobě normálními formami. To poskytuje induktivní syntaktický popis normálních forem. ${\ displaystyle M_ {j}}$${\ displaystyle M_ {j}}$

Existuje také představa normální formy slabé hlavy : výraz v normální formě slabé hlavy je buď výraz v normální formě hlavy, nebo lambda abstrakce. To znamená, že uvnitř těla lambda se může objevit redex.

Redukční strategie

Obecně může daný výraz obsahovat několik redexů, a proto by mohlo být použito několik různých beta redukcí. Můžeme určit strategii pro výběr redexu, který se má snížit.

• Redukce v normálním pořadí je strategie, při které se nepřetržitě aplikuje pravidlo pro beta redukci v poloze hlavy, dokud již takové redukce nejsou možné. V tomto bodě je výsledný člen v normální formě hlavy. Jeden pak pokračuje v redukci hlavy v dílčích podmínkách zleva doprava. Jinak řečeno, redukce normálního řádu je strategie, která vždy nejprve redukuje nejnebezpečnější redex nejvíce vlevo. ${\ displaystyle M_ {j}}$
• Naproti tomu při aplikovatelné redukci pořadí se nejprve použije vnitřní redukce a poté se použije redukce hlavy pouze tehdy, když již nejsou možné žádné vnitřní redukce.

Redukce normálního řádu je úplná v tom smyslu, že pokud má termín normální formu hlavy, redukce normálního řádu ji nakonec dosáhne. Podle výše uvedeného syntaktického popisu normálních forem to znamená stejné tvrzení pro „plně“ normální formu (to je věta o standardizaci ). Naproti tomu se nemusí aplikativní redukce objednávky ukončit, i když má termín normální formu. Například pomocí aplikovatelné redukce objednávky je možná následující sekvence redukcí:

${\ displaystyle {\ begin {zarovnané} & (\ 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 {zarovnáno}}}$

Ale pomocí redukce normálního řádu se stejný výchozí bod rychle sníží na normální formu:

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

${\ displaystyle \ rightarrow z}$

Ředitelské řetězce Sinot jsou jednou z metod, pomocí kterých lze optimalizovat výpočetní složitost redukce beta.

Viz také

• Lambda kalkul
• Normální forma (disambiguation)

Reference