Church–Rosser sats

I lambdakalkylen säger Church –Rosser-satsen att, när man tillämpar reduktionsregler på termer , gör ordningen i vilken reduktionerna väljs ingen skillnad för det slutliga resultatet.

Mer exakt, om det finns två distinkta reduktioner eller sekvenser av reduktioner som kan appliceras på samma term, så finns det en term som kan nås från båda resultaten, genom att tillämpa (eventuellt tomma) sekvenser av ytterligare reduktioner. Teoremet bevisades 1936 av Alonzo Church och J. Barkley Rosser , efter vilken den är uppkallad.

Satsen symboliseras av det intilliggande diagrammet: Om term a kan reduceras till både b och c , så måste det finnas ytterligare en term d (eventuellt lika med antingen b eller c ) som både b och c kan reduceras till. Ser man på lambdakalkylen som ett abstrakt omskrivningssystem , säger Church-Rosser-satsen att reduktionsreglerna för lambdakalkylen är sammanflytande . Som en konsekvens av satsen har en term i lambdakalkylen högst en normalform , vilket motiverar hänvisning till " normalformen " av en given normaliserbar term.

Historia

År 1936 bevisade Alonzo Church och J. Barkley Rosser att satsen gäller för β-reduktion i λI-kalkylen (där varje abstraherad variabel måste förekomma i termens kropp). Bevismetoden är känd som "finiteness of developments", och den har ytterligare konsekvenser som till exempel Standardization Theorem, som relaterar till en metod där reduktioner kan utföras från vänster till höger för att nå en normal form (om en sådan finns). Resultatet för den rena otypade lambdakalkylen bevisades av DE Shroer 1965.

Ren otypad lambdakalkyl

En typ av reduktion i den rena otypade lambdakalkylen som Church–Rosser-satsen gäller är β-reduktion, där en delterm av formen ( λ x . t ) s {\ $}$ kontraheras av substitutionen $t[x:=s]$ . Om β-reduktion betecknas med $\rightarrow _{\beta }$ och dess reflexiva, transitiva stängning med $\twoheadrightarrow _{\beta }$ så är Church–Rosser-satsen att:

$\forall M,N_{1 },N_{2}\in \Lambda :{\text{if}}\ M\twoheadrightarrow _{\beta }N_{1}\ {\text{and}}\ M\twoheadrightarrow _{\beta }N_{ 2}\ {\text{då}}\ \exists X\i \Lambda :N_{1}\twoheadrightarrow _{\beta }X\ {\text{and}}\ N_{2}\twoheadrightarrow _{\beta }X$

En konsekvens av denna egenskap är att två termer lika med $\lambda \beta$ måste reduceras till en vanlig term:

$\forall M,N\in \Lambda :{\text{if}}\ \lambda \beta \vdash M=N\ {\text{då}}\ \exists X:M\twoheadrightarrow _{\beta }X\ {\text{and}}\ N\twoheadrightarrow _{\beta }X$

Satsen gäller även för η-reduktion, där en delterm $\lambda x.Sx$ ersätts med $S$ . Det gäller även βη-reduktion, föreningen av de två reduktionsreglerna.

Bevis

För β-reduktion kommer en bevismetod från William W. Tait och Per Martin-Löf . Säg att en binär relation $\rightarrow$ uppfyller diamantegenskapen om:

$\forall M,N_{1},N_{ 2}\i \Lambda :{\text{if}}\ M\högerpil N_{1}\ {\text{och}}\ M\högerpil N_{2}\ {\text{då}}\ \exists X \in \Lambda :N_{1}\högerpil X\ {\text{och}}\ N_{2}\högerpil X$

Då är egenskapen Church–Rosser påståendet att $\twoheadrightarrow _{\beta }$ uppfyller diamantegenskapen. Vi introducerar en ny reduktion $\rightarrow _{\|}$ vars reflexiva transitiva stängning är $\twoheadrightarrow _{\beta }$ och som uppfyller diamantegenskapen. Genom induktion på antalet steg i reduktionen följer alltså att $\twoheadrightarrow _{\beta }$ uppfyller diamantegenskapen.

Relationen $\rightarrow _{\|}$ har formationsreglerna:

• $M\rightarrow _{\|}M$
• Om $M\rightarrow _{\|}M'$ och $N\rightarrow _{\|}N'$ så är $\lambda xM\rightarrow _{\|}\lambda xM'$ och $MN\rightarrow _{\|}M'N'$ och $(\lambda xM)N\rightarrow _{\|}M'[x:=N']$

η-reduktionsregeln kan bevisas vara Church–Rosser direkt. Sedan kan det bevisas att β-reduktion och η-reduktion pendlar i den meningen att:

Om $M\rightarrow _{\beta }N_{1}$ och $M\rightarrow _{\eta }N_{2}$ så finns det en term $X$ så att $N_{1}\rightarrow _{\eta }X$ och $N_{2}\rightarrow _{\beta }X$ .

Därför kan vi dra slutsatsen att βη-reduktion är Church–Rosser.

Normalisering

En reduktionsregel som uppfyller Church–Rosser-egenskapen har egenskapen att varje term M kan ha högst en distinkt normalform, enligt följande: om X och Y är normala former av M , så reducerar de båda med Church–Rosser-egenskapen till en lika term Z . Båda termerna är redan normala former så $X=Z=Y$ .

Om en reduktion är starkt normaliserande (det finns inga oändliga reduktionsvägar) så innebär en svag form av Church-Rosser-egenskapen hela egenskapen (se Newmans lemma ). Den svaga egenskapen, för en relation $\rightarrow$ , är:

$\forall M,N_{1},N_{2}\in \Lambda :$ om $M\rightarrow N_{1}$ och $M\rightarrow N_{2}$ så finns det en term $X$ så att $N_{1}\twoheadrightarrow X$ och ${\ displaystyle N_{2}\twoheadrightarrow X}$ .

Varianter

Church–Rosser-satsen gäller också för många varianter av lambdakalkylen, som den enkelt skrivna lambdakalkylen , många kalkyler med avancerade typsystem och Gordon Plotkins betavärdekalkyl. Plotkin använde också en Church-Rosser-sats för att bevisa att utvärderingen av funktionella program (för både lat utvärdering och ivriga utvärdering ) är en funktion från program till värden (en delmängd av lambda-termerna).

I äldre forskningsartiklar sägs ett omskrivningssystem vara Church–Rosser, eller att ha egenskapen Church–Rosser, när det är sammanflytande .

Anteckningar

• Alama, Jesse (2017). Zalta, Edward N. (red.). The Stanford Encyclopedia of Philosophy (Hösten 2017 ed.). Metafysikforskningslab, Stanford University.
•   Kyrka, Alonzo ; Rosser, J. Barkley (maj 1936), "Some properties of conversion" (PDF) , Transactions of the American Mathematical Society , 39 (3): 472–482, doi : 10.2307/1989762 , JSTOR 1989762 .
•   Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics , Studies in Logic and the Foundations of Mathematics, vol. 103 (Reviderad utg.), North Holland, Amsterdam, ISBN 0-444-87508-5 , arkiverad från originalet 2004-08-23 . Errata .