Jämför rst-order funktionella program med högre-order program som tillåter funktioner som funktionsparametrar. Kan den första programklassen lösa färre problem än den andra? Svaret är nej: båda klasserna är Turing kompletta, vilket innebär att de kan beräkna alla partiella rekursiva funktioner. I synnerhet kan högre ordervärden simuleras med hjälp av listkonstruktören \cons" för att bygga funktionsstängningar. Denna uppsats använder komplexitetsteori för att bevisa vissa expressivitet resultat om små programmeringsspråk som är mindre än Turing komplett. Komplexitet klasser av beslutsproblem används för att karakterisera den expressiva kraften i funktionella programmeringsspråk funktioner. Ett exempel: andra ordningen program är mer kraftfulla än rst-order, eftersom en funktion f av typen Bool]->Bool kan beräknas av en cons-free rst-order funktionella program om och endast om f är i ptime, medan f kan beräknas av en cons-free andra ordningen program om och endast om f är i exptime. Exakta karakteriseringar ges för de problem av typen Bool]->Bool som kan lösas av program med flera kombinationer av operationer på data: närvaro eller frånvaro av konstruktörer; ordningen av datavärden: 0, 1 eller högre; och programkontrollstrukturer: allmän rekursion, svansrekursion, primitiv rekursion. Har programmeringsstilen vi använder en ekt de problem vi kan lösa, eller eektiviteten hos de program vi kan skriva för att lösa ett givet problem? Några frågor som är särskilt relevanta för denna tidskrift: 1. Ger användningen av funktioner som datavärden en större problemlösningsförmåga? 2. Utgångspunkten är följande: Är rekursion mer kraftfull än iteration? 3. Vad är det som händer? Skulle användningen av ett starkt normaliserande programmeringsspråk, som föreslagits av flera forskare, inklusive (Crockett, Spencer, 1991), (Voda, 1994), (Turner, 1996) och (Lloyd, 1999) införa några begränsningar på de problem som kan lösas? Detta dokument ger några svar på dessa frågor, när det är begränsat till helt enkelt maskinskrivna funktionella program utan \cons". I synnerhet svaret på fråga 1 är Denna forskning stöddes delvis av det danska Naturvetenskapliga forskningsrådet (DART-projektet). \yes," högre ordning program kan lösa problem som rst-order program inte kan. Svaret på fråga 2 för rst-order program är \yes" om och endast om ptime 6 = logspace (och därför sannolikt inte kommer att beslutas inom överskådlig framtid). Ett partiellt (positivt) svar på fråga 3 kommer att ges senare. Programmeringsstilar. Faktorer som är eektiva och enkla att programmera inkluderar de former av kontroll som används: allmän rekursion, primitiv rekursion, svansrekursion, undantag, backtracking, etc.; de datatransaktioner som används: är data grundläggande eller högre ordning, är det otypad eller typad av olika system, är \logic variabler" tillåtet, etc.; och andra semantiska frågor: ivrig eller lat utvärdering, memoarering av funktionsresultat, närvaro eller frånvaro av ett globalt tillstånd, statisk eller dynamisk namnbindning, etc. Vårt främsta mål är att förstå (och avgränsa) den uttrycksfulla kraften hos olika programmeringsspråkfunktioner. I allmänhet kan man skilja mellan absoluta expressivitetsfrågor och relativa expressivitetsfrågor. En \absolut expressivitet" fråga om programmering språkfunktion X: \ Finns det problem som kan lösas av program med funktion X, och kan inte lösas utan funktion X?" En \relativ expressivitet" fråga: \ Finns det ett problem som kan lösas både med och utan funktion X, men så att någon lösning utan funktion X nödvändigtvis är mindre effektiv än någon lösning med X?" (Effektivitet kommer att mätas med tidsanvändning i hela detta papper.) Hur kan expressivitetsfrågor formuleras på ett exakt och meningsfullt sätt, och hur kan man finna svar på dem? Vår strategi är att använda komplexitetsteori, vilket ger ett kraftfullt sätt att klassificera problem efter deras lösningssvårighet. I synnerhet finns det teorem som visar att, under lämpliga antaganden, ökar den tillgängliga beräkningstiden bevisligen förstorar den klass av problem som kan lösas, med analoga resultat för andra resurser som minne. Ett hinder för att studera absolut uttrycksfullhet. Absoluta expressivitetsfrågor är irrelevanta för tillräckligt starka språk. Anledningen är att alla Turing kompletta språk kan beräkna alla partiella rekursiva funktioner (modulo datakodning) { och därmed i absolut mening alla är lika uttrycksfulla. Vi kommer runt detta genom att studera Turing-ofullständiga underspråk. Hinder för att studera relativ expressivitet. En av kulten är att det finns många tämligen effektiva simuleringar av ett programmeringsspråk som andra har. En följd av detta är att det på ett starkt språk är svårt att besvara relativa expressivitetsfrågor eftersom alla förväntade komplexitetsskillnader skulle vara mycket små. Detta beror på förmågan att \programmera din väg runt ett problem" på ett tillräckligt starkt språk. Två besläktade fakta av detta slag följer. (Körtid mäts som antalet atomiska beräkningssteg som en funktion av ingångslängd n.) En slumpmässig-access maskin kan simulera en rst-order eller högre-order funktionella program (eller Turing maskin) med som mest en konstant avmattning. Ett rst-order funktionella program kan simulera en slumpmässig-access maskin med som mest en logaritmisk avmattning, från tid T(n) till T(n) log T(n). Sådana resultat tenderar att minimera betydelsen av skillnader i programmeringsparadigm, förutsatt att de berörda språken är tillräckligt rika på sätt att \program runt." Vårt sätt att studera uttrycksfullhet. Ett språk som har obunden lagring/minne för datavärden, plus kontroll som tillåter ett obundet antal operationer på datavärden, kommer nästan säkert att vara Turing komplett. Ett sätt runt detta hinder är att gradvis begränsa språkfunktioner, ta bort en i taget tills det resulterande programmeringsspråket inte längre Turing komplett, och sedan använda beräkningsbarhet och komplexitet teori för att jämföra den absoluta uttryckskraft av resulterande \minispråk." Eekten är att studera expressivitet av språkkonstruktioner med hjälp av komplexitetsteori för att jämföra olika val av språkfunktioner. Vi karakteriserar exakt, när det gäller komplexitetsklasser, eekterna på uttryckskraft av olika kombinationer av tre programbegränsningar. Den första rör skapandet av ny lagring: är konstruktörer av strukturerade data tillåtna eller inte? Den andra gäller ordningen för datavärden: 0, 1 eller högre. Den tredje gäller programkontrollstrukturer: allmän rekursion, eller endast svansrekursion, eller endast primitiv rekursion. Länkarna sammanfattas i tabellen i figur 2.1 och kon rm programmerares intuitioner att högre ordningstyper verkligen ger en större problemlösningsförmåga. I detta dokument bevisar vi endast resultaten av raderna 3 och 4, de andra som ingår för sammanhangets skull. Många kombinationer är Turing-komplett, så sådana program beräkna alla partiella rekursiva funktioner. Ett klassiskt Turing-ofullständigt språk får man genom att begränsa data till ordning 0 och kontroll till \fold." Sådana program beräknar de primitiva rekursiva funktionerna. Figur 2.1 visar eekten av högre ordningstyper på datorkraften hos program av typen Bool]->Bool. Varje post är en komplexitetsklass, dvs. insamling av beslutsproblem som kan lösas av program som begränsas av rad- och kolumnindex. ro står för \read-only, d.v.s. program utan konstruktörer, och rw står för \read-write." säger meningsfulla saker om programmeringsspråk. Komplexitetsteorin används traditionellt för att klassificera beslutsproblemens hårdhet, så vi måste koppla beslutsproblem till program och deras beräkningar. Länka beslutsproblem och funktionella program. I komplexitet teori ett beslut problem A är en uppsättning strängar över en nite alfabetet, så A. En lösning på problemet är en algoritm som, med tanke på x = a 1 a 2 : : a n 2, bestämmer om x 2 A. Vi kan utan förlust av generalitet välja = f0; 1g, eftersom större alfabet kan kodas som bitsträngar. Den karakteristiska funktionen f A för uppsättning A f0; 1g, av typ f A : f0; 1g! f0; 1g, satis es för alla a 1 ; a 2 ; : : ; a n 2 f0; 1g f(a 1 a 2 : : : a n) = om a 1 a 2 : : : a n 2 A sedan 1 annan 0 Hädanefter ska vi identifiera 0,1 med falsk, sann och kodsträng a 1 a 2 : : : a n som booleanlista a 1 ; a 2 ; : : ; a n ], vilket gör analogin mellan beslutsproblem och program med input-output typ Bool] - > Bool exakt. Mer allmänt, Figur 2.1 gäller beräkningskraft av fullt maskinskrivna funktionella program vars interna typer är begränsade till de som bildas från Bool och Bool] av funktionsutrymmen! 0 och Cartesian produkter 0. Ingen typ av siffror ingår, eftersom om siffrorna begränsas de kan simuleras av tuples av Boooleska variabler; och om siffrorna är obundna, konstiga och orealistiska beräkningar kan utföras (som kommer att ses nedan). Vidare Kolumnindexen begränsar beställningarna av programdatatyper. Ett \order k + 1" program kan ha funktioner av typ! 0 där datatypen är av ordning k. Således, till exempel, den första kolumnen beskriver rst-order program, vars parametrar är booleaner eller listor över booleaner. Varje post är insamling av beslutsproblem som kan lösas av program som begränsas av rad- och kolumnindex. Rad 1: Dessa programkurser är alla Turing färdiga. Följaktligen kan de acceptera exakt rekursivt omfångsrika undergrupper av f0; 1g. Rad 2: Dessa program har obegränsade dataoperationer och typer, men kontrollen är begränsad till primitiv rekursion, bekant för funktionella programmerare under namnet\fold right". 1 Sådana rst-order program accepterar exakt de uppsättningar vars karakteristiska funktioner är primitiva rekursiva (sant oavsett om data är strängar eller naturliga tal). Högre ordning primitiva rekursiva funktioner dök upp i G odel system T många år sedan (Girard, Lafont, Taylor, 1989), (Voda, 1997). De är för närvarande av stort intresse för den konstruktiva typteorins eld på grund av Curry-Howards isomorfism, vilket gör det möjligt att extrahera program från bevis. Primitiv rekursion kommer på grund av bevis genom induktion; extraktion av program som använder allmän rekursion är mycket mindre naturligt. Rad 3: Dessa program har obegränsad kontroll, men tillåter endast skrivskyddad åtkomst till deras data. Lista destructor operationer hd och tl är tillåtna, men inte konstruktören nackdelar. Även om detta kan tyckas vara en drakonisk begränsning ur programmerarens synvinkel, är den klass av problem som kan lösas respektabelt stor. Order 1 program kan lösa alla problem som ligger i ptime; ordning 2 program, med rst-order funktioner som datavärden, kan lösa alla problem i den ganska stora klassen exptime, etc. I allmänhet leder varje ökning av datatypernas ordning till en korrekt ökning av de lösbara problemen, eftersom det är känt att ptime är ordentligt inneslutet i exptime, och så vidare upp hierarkin. Rad 4 karakteriserar read-only program begränsade till svans rekursion, där ingen funktion kan kalla sig på ett näste sätt. Order 1 svans rekursiva program accepterar alla och endast problem i logspace, en välstuderad delmängd av ptime. Högre ordning svans rekursiva program accepterar problem i (korrekt) större rumsbundna klasser pspace, expspace, etc. (Tail recursion är av operativt intresse eftersom vid körning (förutsatt ivrig utvärdering, dvs. call-by- value semantics) call stack djup har en konstant djup bunden, oavsett indata. Ett sådant program kan konverteras till icke-rekursiv imperativ form genom att ersätta varje funktion anrop med en GOTO, och realisera funktion parameter passerar uppdrag till globala variabler.) 1 Kleenes definition av primitiv rekursion är lite mer allmän än \fold right, "men är lätt programmerad med hjälp av vik höger och komposition. Se (Hutton, 1999) för närmare information. Rad 5 karakteriserar lässkyddade program begränsade så all rekursion måste uttryckas med \fold right, dvs. endast primitiv rekursion är tillåten. Order 1 skrivskyddade primitiva rekursiva program accepterar endast problem i logrymden och är således likvärdiga med svansrekursiva program. Vid högre klasser försvinner denna ekvivalens; de primitiva rekursiva läsbara programmens förmåga att lösa beslutsproblem växer endast med halva hastigheten": en ökning av dataordern med 2 behövs för att uppnå samma ökning av beslutsförmågan som en ökning med 1 som uppnås för allmänna eller svansrekursiva program. Gräns på raderna 3, 4 och 5 Det står klart att sammanslutningen av klasserna i rad 3 är lika med föreningen för rad 4 och för rad 5. Detta är den klass av problem som kan lösas i tiden avgränsas av 2 2 2 n, där höjden på exponenten stacken är något naturligt tal. Detta är välkänt som klass av elementära uppsättningar, och studerades av logiker innan komplexitetsteorin började. Detta dokuments tillämpningsområde och bidrag. Resultaten i raderna 1 och 2 är klassiska och upprepas inte här. Vi bevisar resultaten i raderna 3 och 4 i figur 2.1. Resultaten i rad 4 verkar vara nya; och resultaten i rad 3, medan i en mening förväntas av (Goerdt, 1992), här bevisas för första gången i ett programmeringsspråk sammanhang. Resultaten i rad 5 erhålls från (Goerdt, 1992) och (Goerdt, Seidl, 1996) genom att omtolka resultat från nite modellteori som skisseras i bilagan. Det har länge varit känt att ordningen k + 1 primitiva rekursiva program är riktigt kraftfullare än ordningen k primitiva rekursiva program, d.v.s. prim k rec. prim k+1 rec. Detta är dock av föga praktiskt intresse, eftersom även ordningen 0 klass prim.rec. är enorm, ordentligt innehållande sådana klasser som nptime och elementär. Ger användningen av funktioner som datavärden en större problemlösningsförmåga? I figur 2.1 är svaret \ nej" för obegränsade program, och \ ja" för alla de begränsade språk vi anser. Den enda osäkerheten är med de skrivbara primitiva rekursiva programmen; för dessa behövs en ökning i dataordning på minst 2 för att garantera en korrekt ökning av problemlösningskraften. Är allmän rekursion mer kraftfull än svans rekursion? För lässkyddade program med rst-order har denna fråga klassisk import eftersom detta vid tabellens första kolumn (rad 3, 4) motsvarar frågan: Är ptime en riktig superuppsättning logspace? Detta är tyvärr en olöst fråga, öppen sedan den först formulerades i början av 1970-talet. En motsvarande fråga (rad 3, 5): Är allmän rekursion mer kraftfull än primitiv rekursion? Situationen är dock olika för andra och högre order. För läsbara program med högre ordning, är frågan om allmän rekursion är starkare än svansrekursion också öppen, vilket motsvarar exptime pspace? Men svaret är \ ja" när man jämför allmän rekursion med primitiv rekursion, eftersom det är känt att exptime korrekt inkluderar ptime. På starkt normalisera språk. Om vi antar som vanligt att program i ett starkt normaliserande språk endast har primitiv rekursiv kontroll, det finns problem som kan lösas genom läs-bara allmänna rekursiva program med dataordning 1; 2; 3; : : :, men inte lösbar genom läs-bara starkt normalisera program av samma data order. Detta tyder på en inneboende svaghet i utvinningen av program från bevis av Curry-Howard isomorphism. Rad 3, kolumn 1 i figur 2.1 hävdar att rst-order cons-free read-only program kan lösa alla och bara problemen i ptime. Vid re ection detta påstående verkar ganska osannolikt, eftersom det är lätt (utan att använda högre-order funktioner) att skriva cons-fria läs-endast program som kör exponentiellt långt innan stopp. Till exempel: f x = om x = ] sedan sant annars om f(tl x) sedan f(tl x) annars falska körs i tid (2 n ) på en inmatningslista över längd n (oavsett om anrop-för-värde eller lata semantik används), på grund av dator f(tl x) om och om igen. Vad är det? Den skenbara paradoxen försvinner när man väl förstår vad det är som bevisen åstadkommer 2. Den har två delar: Construction 1 visar att alla rst-order cons-free read-only program bestämmer ett problem i ptime. Metod: visa hur man simulerar en godtycklig rst-order cons-fri read-only program med en polynom-tid algoritm. Konstruktion 2 visar att eventuella problem i ptime kan beräknas av vissa rstorder cons-free read-only program. Metod: visa hur man simulerar en godtycklig polynom-tid Turing maskin med en rst-order cons-fri lässkyddat program. Metoden av Construction 1 i e ect visar hur man simulerar ett cons-free read only-program snabbare än det körs. Det är inte en steg-för-steg simulering, men använder en icke-standard \memoizing" semantisk tolkning. (För exemplet ovan skulle värdet av f(tl x) sparas när rst beräknas, och hämtas från minnet varje gång samtalet senare utförs.) Metoden för Construction 2 ger program som nästan alltid tar exponentiell tid att köra; men detta är inte en motsägelse eftersom genom Construction 1 de problem de löser kan avgöras i polynom tid. 3 Relaterat arbete och erkännanden Mycket arbete som relaterar komplexitet och logiska eller programmeringsspråk har olika utgångspunkter och motiv. Många tidningar har som mål att karakterisera 2 För rst-order cons-free read-only program se (Jones, 1997; Jones, 1999), som använder en teknik från (Cook, 1971). För lässkyddade program i högre ordning, se Theorem 7.17 senare i denna artikel. resursbundna komplexitetsklasser i form av logiska, rekursionsteoretiska eller andra formalismer. Exempel (beordrade genom att öka avståndet från programmeringsspråk) inkluderar rekursiva funktioner, lambda kalkyl, program schemata, nite modellteori, och kategoriteori. Arbete som direkt relaterar programmeringsspråk och komplexitetsteori. Syftet med detta dokument är just att karakterisera beräkningskraften hos flera begränsningar av ett realistiskt programmeringsspråk. (Jones, 1999) är ett av de få dokument som fokuserar på det gränssnittet; det kännetecknar kraften i rst-order read-only program i komplexa termer. Loggar och ptime poster i kolumn 1 visas där, och i (Jones, 1997) som Theorems 24.1.7, Corollary 24.2.4 och Theorem 24.2.5. Här dessa resultat utvidgas till godtyckliga nite data order, och till svans rekursiva program. Resultaten har ännu djupare rötter. Logspace resultatet stärker en \folklore" resultat på multihead read-only Turing maskiner; och ptime resultatet motsvarar ett resultat på \ två-vägs hjälp pushdown automata" bevisat av Cook, innan hans P-NP papper (Cook, 1971). Bidraget från (Jones, 1997; Jones, 1999) var att återuttrycka Cooks resultat med hjälp av ett rekursivt programmeringsspråk. Relativ expressivitet. En signi kan inte kliva fram i relativ expressivitet (en eld med många gissningar men få beprövade resultat) var (Pippenger, 1997), som visade att ren LISP måste vara långsammare med en logaritmisk faktor än \impure" LISP. Mer exakt, ett visst problem (att tillämpa en permutation on-line) visade sig kräva tid (n log n) i ren Lisp, men att vara löslig i tid O (n) i oren Lisp med setcar och setcdr. Intressant, (Bird, Jones, De Moor, 1998) visar att samma problem kan lösas med tiden O(n) på ett språk med lat utvärdering, så sådana språk är i sig snabbare än rst-order ivriga språk. Ett bevis på att deras konstruktion faktiskt går i linjär tid finns i (Neergaard, 1999). Rekursiv funktion och kategoriteori. Recursive function denition systems kan betraktas som att definiera programmeringsspråk, till exempel den primitiva rekursiva funktionen de nitions, och underhierarkin studeras av (Grzegorczyk, 1953) med flera. (Cobham, 1964) gav en tidig karakterisering av ptime innefattande yttre storlek gränser jämförbara med de av Grzegorczyk, men med rekursion på notation. (Voda, 1994) relaterar primitiv rekursion och subrecursion till programmeringsspråk, med hjälp av en datastruktur som den för (Jones, 1997 ). En \intrinsic" metod som karakteriserar ptime efter stegvis rekursion på notation 3 ses i (Bellantoni och Cook, 1992), och har inspirerat mycket arbete sedan dess, några med kategoriska begrepp (Bellantoni, Niggl, Schwichtenberg, 1998; Hofmann, 1999). Skriven lambda calculi. En serie av papper av Leivant (vissa med Marion) karakteriserar komplexitet clases i termer av helt enkelt maskinskrivna lambda calculi med återkommande konstanter, 3 Tanken är att rekursion över ingångar är tillåtet ( rst nivå), men inte recusrsion över beräknade värden (andra nivån). Ett typsystem håller reda på nivåerna. inklusive (Leivant, 1989; Leivant och Marion, 1993; Leivant och Marion, 1999). I synnerhet studerar de kalkyl vidgade av funktioner och operationer på en algebra av ord över f0; 1g, och karakteriserar ptime, pspace och flera andra klasser. De tidigare verken hade ganska komplexa formuleringar främst relaterade till rami ed recidiv, men (Leivant, 1999) Program schemata. (Paterson, Hewitt, 1970 ) var en banbrytande tidig tidning, och rekursion avlägsnande har varit ett återkommande tema i denna Eld. Komplexitet karakteriseringar relaterade till datatyper visas i (Kfoury, Tiuryn, Urzyczyn, 1987) och (Kfoury, Tiuryn, Urzyczyn, 1992). Skillnaden mellan rekursion och iteration när högre orderdata är inblandade studeras i (Kfoury, 1997; Kfoury, 1999). Ur ett schematiskt perspektiv, svar på de frågor som ställs om programbeteende måste vara giltiga för alla möjliga interpetitioner av domäner och basfunktioner som visas i ett givet program. Sådana resultat är mindre direkt relevanta för programmeringsspråk än våra; programmerare använder naturligtvis en enda xed data tolkning. Finita modellteorier. Många komplexitet karakteriseringar har gjorts av problem med nite modellteori, med (Jones, Selman 74) uppenbarligen den första i en Eld utvecklats ganska avsevärt sedan dess (Gurevich, 1983; Gurevich, 1984; Immerman, 1987; Goerdt, 1992). Det finns ett naturligt samband mellan beräkning genom read-only programs och i nite modell teori som de ned av Gurevich och andra, tillräckligt nära att vissa komplexitet karakteriseringar från nite modell teori innebär motsvarande resultat om read-only program. Anslutningen kräver dock tillräckligt de nitional maskineri, att för att undvika att bryta kontinuiteten i presentationen vi skjuter upp det till ett tillägg. De enda resultat vi inte bevisar här med hjälp av funktionell programmering är de på rad 5. Finita modellversioner av loggrymden och ptime-posterna i kolumn 1 visades av Gurevich. Goerdt bevisade nite modellversioner av alla rad 3. Vissa ganska komplexa konstruktioner etablerar de första 4 kolumnerna i rad 5 i (Goerdt, 1992; Goerdt, 1992); och (Goerdt, Seidl, 1996) visar att tid-rymdväxlingen sträcker sig till godtyckliga dataordningar. Tackar. Tack är Bruce Kapron, för att påpeka likheten mellan Gurevich och Goerdts nite modellteori resultat med mina på rst-order read-only program; till anonyma domare; till Amir Ben-Amram för många användbara dis-
I REF Jones karakteriseras PTIME med hjälp av enkla konstruktörsfria program.
The Expressive Power of Higher-order Types or, Life without CONS
{'venue': 'J. Funct. Program.', 'journal': 'J. Funct. Program.', 'mag_field_of_study': ['Computer Science']}