Reduktionsstrategi

Vid omskrivning är en reduktionsstrategi eller omskrivningsstrategi en relation som anger en omskrivning för varje objekt eller term, kompatibel med en given reduktionsrelation. Vissa författare använder termen för att referera till en utvärderingsstrategi .

Definitioner

Formellt, för ett abstrakt omskrivningssystem $(A,\to )$ , är en reduktionsstrategi $\to _{S}$ en binär relation på $A$ med ${\displaystyle \to _{S}\subseteq {\overset {+}{\to }}} ,$ där ${\overset {+}{\to }}$ är transitiven stängning av $\to$ (men inte den reflexiva stängningen). Dessutom måste de normala formerna för strategin vara desamma som de normala formerna för det ursprungliga omskrivningssystemet, dvs för alla ${\displaystyle a} ,$ finns det en $b$ med $a\ till b$ om $\exists b'.a\to _{S}b'$ .

En ettstegsreduktionsstrategi är en där $\to _{S}\subseteq \to$ . Annars är det en strategi i många steg .

En deterministisk strategi är en där $\to _{S}$ är en partiell funktion , dvs för varje $a\in A$ finns det högst en $b$ så att $a\to _{S}b$ . Annars är det en icke-deterministisk strategi.

Termomskrivning

I ett termomskrivningssystem specificerar en omskrivningsstrategi, av alla reducerbara undertermer ( redexes ), vilken som ska reduceras ( kontrakteras ) inom en term.

Enstegsstrategier för omskrivning av termer inkluderar:

längst in till vänster: i varje steg dras den längst till vänster av de innersta redoxerna samman, där en innersta redex är en redex som inte innehåller några redexer
ytterst till vänster: i varje steg dras den längst till vänster av de yttersta redoxerna samman, där en yttersta redex är en redex som inte ingår i några redoxer
längst till höger, längst till höger: på liknande sätt

Flerstegsstrategier inkluderar:

parallell-innersta: reducerar alla innersta redoxer samtidigt. Detta är väldefinierat eftersom redoxerna är parvis osammanhängande.
parallellt-ytterst: på liknande sätt
Gross-Knuth-reduktion, även kallad full substitution eller Kleene-reduktion: alla redoxer i termen reduceras samtidigt

Parallell yttersta och Gross-Knuth-reduktion är hypernormaliserande för alla nästan ortogonala termomskrivningssystem, vilket innebär att dessa strategier så småningom kommer att nå en normal form om den existerar, även när man utför (ändligt många) godtyckliga reduktioner mellan successiva tillämpningar av strategin.

Stratego är ett domänspecifikt språk som är designat specifikt för programmeringsstrategier för omskrivning av termer.

Lambdakalkyl

I samband med lambdakalkylen hänvisar normalordningsreduktion till minskningen längst till vänster i den mening som ges ovan . Normalordningsreduktion är normaliserande, i den meningen att om en term har en normal form, så kommer normalordningsreduktion så småningom att nå den, därav namnet normal. Detta är känt som standardiseringsteoremet.

Reduktion längst till vänster används ibland för att hänvisa till normal ordningsreduktion, eftersom begreppen överensstämmer med en förbeställningsövergång, och på samma sätt är den yttersta redexen redoxen med det första tecknet längst till vänster när lambda-termen betraktas som en teckensträng. När "längst till vänster" definieras med hjälp av en genomgång i ordning är begreppen distinkta. Till exempel, i termen $(\lambda xx\Omega )(\lambda yI)$ med $\Omega ,I$ definierad här , redexen längst till vänster för genomgången i ordning är $\Omega$ medan redexen längst till vänster är hela uttrycket.

Tillämplig ordningsreduktion avser reduktion längst till vänster. Till skillnad från normal ordning får tillämplig ordningsnedsättning inte upphöra, även när termen har normal form. Om du till exempel använder applicerande orderreduktion är följande sekvens av reduktioner möjlig:

{\ displaystyle {\begin{aligned}&(\mathbf {\lambda } xz)((\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda xz)((\lambda w.www) )(\lambda w.www)(\lambda w.www))\\\högerpil &(\lambda xz)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\ lambda w.www))\\\högerpil &(\lambda xz)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www. www))\\&\ldots \end{aligned}}}

Men med normal ordningsreduktion reduceras samma utgångspunkt snabbt till normal form:

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

\rightarrow z

Full β-reduktion hänvisar till den icke-deterministiska enstegsstrategin som gör det möjligt att reducera eventuell redex vid varje steg. Takahashis parallella β-reduktion är strategin som minskar alla redoxer i termen samtidigt.

Svag reduktion

Normal och applikativ ordningsreduktion är starka genom att de tillåter reduktion under lambdaabstraktioner. Däremot svag reduktion under en lambdaabstraktion. Call-by-name-reduktion är den svaga reduktionsstrategin som reducerar den yttersta redexen längst till vänster inte inuti en lambdaabstraktion, medan call-by-value-reduktion är den svaga reduktionsstrategin som reducerar den innersta redexen längst till vänster inte inuti en lambdaabstraktion. Dessa strategier utarbetades för att återspegla strategierna för call-by-name och call-by-value . Faktum är att applikativ orderreduktion också ursprungligen introducerades för att modellera tekniken för överföring av call-by-value parameter som finns i Algol 60 och moderna programmeringsspråk. När den kombineras med idén om svag reduktion, är den resulterande call-by-value-minskningen verkligen en trogen approximation.

Tyvärr är svag reduktion inte sammanflytande, och de traditionella reduktionsekvationerna i lambdakalkylen är värdelösa, eftersom de föreslår samband som bryter mot den svaga utvärderingsregimen. Det är dock möjligt att utöka systemet till att vara sammanflytande genom att tillåta en begränsad form av reduktion under en abstraktion, i synnerhet när redexen inte involverar variabeln som är bunden av abstraktionen. Till exempel λ x .(λ y . x ) z i normal form för en svag reduktionsstrategi eftersom redex (λ y . x ) z ingår i en lambdaabstraktion. Men termen λ x .(λ y . y ) z kan fortfarande reduceras under den utökade svaga reduktionsstrategin, eftersom redexen (λ y . y ) z inte refererar till x .

Optimal reduktion

Optimal reduktion motiveras av förekomsten av lambda-termer där det inte finns en sekvens av reduktioner som reducerar dem utan att duplicera arbete. Tänk till exempel

((λg.(g(g(λx.x)))) (λh.((λf.(f(f(λz.z)))) (λw.(h(w(λy.y))))) )))

Den är sammansatt av tre kapslade termer, x=((λg. ... ) (λh.y)) , y=((λf. ...) (λw.z) ) , och z=λw.(h( w(λy.y))) . Det finns bara två möjliga β-reduktioner att göra här, på x och på y. Att reducera den yttre x-termen resulterar först i att den inre y-termen dupliceras, och varje kopia måste reduceras, men om du först reducerar den inre y-termen dupliceras dess argument z, vilket gör att arbete dupliceras när värdena för h och w görs kända.

Optimal reduktion är inte en reduktionsstrategi för lambda-kalkylen i snäv bemärkelse eftersom att utföra β-reduktion förlorar informationen om de ersatta redoxer som delas. Istället definieras den för den märkta lambdakalkylen , en kommenterad lambdakalkyl som fångar en exakt uppfattning om det arbete som bör delas.

Etiketter består av en oräkneligt oändlig uppsättning atometiketter och sammanlänkningar $ab$ , överstrykningar ${\overline {a}}$ och understrykningar ${\underline {a}}$ av etiketter. En märkt term är en lambdakalkylterm där varje delterm har en etikett. Standardinledande märkning av en lambdaterm ger varje underterm en unik atommärkning. Märkt β-reduktion ges av:

((\lambda .xM)^{\alpha }N)^{\beta }\to \ beta {\overline {\alpha }}\cdot M[x\mapsto {\underline {\alpha }}\cdot N]

där $\cdot$ sammanfogar etiketter, $\beta \cdot T^{\alpha }=T^{\beta \alpha }$ , och substitution $M[x\mapsto N]$ definieras enligt följande (med Barendregt-konventionen) :

{\begin{aligned}x^{\alpha [x\mapsto N]&=\alpha \cdot N& \quad (\lambda yM)^{\alpha [x\mapsto N]&=(\lambda yM[x\mapsto N])^{\alpha }\\y^{\alpha [x\mapsto N] &=y^{\alpha }&\quad (MN)^{\alpha [x\mapsto P]&=(M[x\mapsto P]N[x\mapsto P])^{\alpha }\end {Justerat}}

Systemet kan bevisas vara sammanflytande. Optimal reduktion definieras då som normal ordning eller längst till vänster med reduktion av familjer, dvs parallell reduktion av alla redoxer med samma funktionsdeletikett. Strategin är optimal i den meningen att den utför det optimala (minsta) antalet familjeminskningssteg.

En praktisk algoritm för optimal reduktion beskrevs första gången 1989, mer än ett decennium efter att optimal reduktion först definierades 1974. Bologna Optimal Higher-order Machine (BOHM) är en prototypimplementering av en utvidgning av tekniken till interaktionsnät . Lambdascope är en nyare implementering av optimal reduktion, även med hjälp av interaktionsnät.

Ring efter behovsminskning

Call by need reduction kan definieras på samma sätt som optimal reduktion som svag minskning längst till vänster med parallell reduktion av redoxer med samma etikett, för en något annorlunda märkt lambda-kalkyl. En alternativ definition ändrar betaregeln till en operation som hittar nästa "behövliga" beräkning, utvärderar den och ersätter resultatet på alla platser. Detta kräver att betaregeln utökas för att tillåta reducering av termer som inte är syntaktiskt intill varandra. Som med call-by-name och call-by-value, utformades call-by-need-reduktion för att efterlikna beteendet hos utvärderingsstrategin som kallas " call -by-need" eller lat utvärdering .

Se även

Anteckningar

externa länkar

Arbetsbänk för reduktion av lambdakalkyl