Scott–Curry-satsen

I matematisk logik är Scott -Curry-satsen ett resultat i lambdakalkyl som säger att om två icke-tomma uppsättningar av lambdatermer A och B stängs under beta-konvertibilitet så är de rekursivt oskiljbara .

Förklaring

En uppsättning A med lambda-termer stängs under beta-konvertibilitet om för några lambda-termer X och Y, om $X\in A$ och X är β-ekvivalent med Y då $Y\ i A$ . Två uppsättningar A och B av naturliga tal är rekursivt separerbara om det finns en beräkningsbar funktion $f:\mathbb {N} \rightarrow \{0,1\}$ så att $f(a)=0$ om $a\in A$ och $f(b)=1$ om $b\ i B$ . Två uppsättningar lambda-termer är rekursivt separerbara om deras motsvarande mängder under en Gödel-numrering är rekursivt separerbara och rekursivt oskiljbara annars.

Scott–Curry-satsen gäller lika för termuppsättningar i kombinatorisk logik med svag likhet. Den har paralleller till Rices teorem i beräkningsbarhetssatsen, som säger att alla icke-triviala semantiska egenskaper hos program är oavgjorda.

Satsen får den omedelbara konsekvensen att det är ett oavgörligt problem att avgöra om två lambdatermer är β-ekvivalenta.

Bevis

Beviset är anpassat från Barendregt i The Lambda Calculus .

Låt A och B vara stängda under beta-konvertibilitet och låt a och b vara lambdatermrepresentationer av element från A respektive B. Antag för en motsägelse att f är en lambdaterm som representerar en beräkningsbar funktion så att $fx=0$ ​​om $x\in A$ och $fx=1$ om $x\in B$ (där likhet är β-likhet). Definiera sedan $G\equiv \lambda x.{\text{if}}\ ({\text{noll?}}\ (fx))ab$ . Här, ${\text{noll?}}$ är sant om dess argument är noll och annars falskt, och ${\text{if}}$ är identiteten så att ${\ text{om}}\ bxy$ är lika med x om b är sant och y om b är falskt.

Då $x\in C\implicerar Gx=a$ och på liknande sätt, $x\notin C\implicerar Gx=b$ . I den andra rekursionssatsen finns det en term X som är lika med f applicerad på kyrkans siffra för dess Gödel-numrering, X ' . Då $X\in C$ att $X=G(X')=b$ så faktiskt $X\notin C$ . Det omvända antagandet $X\notin C$ ger $X=G(X')=a$ så $X\in C$ . Oavsett vilket vi uppstår vid en motsägelse, och därför f inte vara en funktion som skiljer A och B . Därför A och B rekursivt oskiljbara.

Historia

Dana Scott bevisade satsen först 1963. Satsen, i en något mindre allmän form, bevisades oberoende av Haskell Curry . Den publicerades i Currys 1969-tidning "The undecidability of λK-conversion".