Vi studerar komplexiteten i tillgänglighetsproblem på grenning förlängningar av vektor tilläggssystem, vilket gör att vi kan härleda nya icke-elementära komplexitet gränser för fragment och varianter av promotionell linjär logik. Vi visar att bevisbarheten i det multiplikativa exponentiella fragmentet är TOWER-hård redan i det affina fallet-och därmed icke-elementära. Vi matchar denna lägre gräns för hela den propositionella lineära logiken, som bevisar dess TOWER-fullständighet. Vi visar också att bevisbarheten i propositionell kontraktiv linjär logik är Ackermann-komplett. • den oavvisliga bevisbarheten i projicativ linjär logik (LL), tack vare en minskning från det stoppande problemet i Minsky maskiner bevisade av Lincoln, Mitchell, Scedrov, och Shankar [14], som initierade mycket av denna linje av arbete, • den decisionabilityen av!-Horn fragment av multiplicativ exponentiell linjär logik, bevisas av Kanovitj [9] genom minskning till nåbarhet i vektor tilläggssystem, • decisionabilityen av bevisbarhet i affin linjär logik, först visas av Kopylov med hjälp av ett begrepp av vektor tillägg spel [10], • AckermanN-fullhet bevisbarhet i konjunktiv implicative fragment av relevans logik, bevisas av * Urquhart [23], med hjälp av minskningar till och från expansiva växelvektor tilläggssystem, och • interreproducerbarheten mellan bevisbarheten i multiplicativ exponentiell linjär logik och nåbarhet i en modell av grenning vektor tilläggssystem, visat av de Groote, Guillaume, och Salvati [5]. I det här dokumentet ser vi över överensstämmelserna mellan promotionell linjär logik och motsystem med fokus på beräkningskomplexitet. I Avsnitt 3 definierar vi en modell av växelförgrenade vektortilläggssystem (ABVASS) med fullständiga nolltester. Även om denna modell kan ses som en förlängning och ompackning av Kopylovs vektorspel, har dess räckvidd problem mycket enkla minskningar till och från bevisbarhet i LL, som är lämpliga för komplexa uttalanden (se avsnitt 4). Vi bevisar att: • täckbarhet i den övre-ner, rot-till-blad riktning är TOWERfullständig, dvs.. komplett för den klass av problem som kan lösas med tid eller utrymme resurser avgränsas av ett torn av exponentiella vars höjd beror delvis i ingångsstorlek (se avsnitt 5 för den övre gränsen och avsnitt 6 för den nedre gränsen), och • täckning i nedersta-up, leave-to-root riktning är komplett för ACKERMANN, dvs. komplett för resurser som begränsas av Ackermann-funktionen av någon primitiv-rekursiv funktion av inmatningen. På grund av utrymmesbegränsningar utelämnas de tekniska detaljerna för denna andra punkt i detta dokument men finns tillsammans med annat material i det fullständiga dokumentet på adressen http://arxiv.org/abs/1401.6785. Vår komplexitet gränser för ABVASS översätta till exakt samma gränser för bevisbarhet i fragment och varianter av LL: Affine Linear Logic (LLW) visades decidable av Kopylov [10] 1995 med hjälp av vektor tillägg spel; en modell-teoretiska bevis presenterades senare av Lafont [11]. 1 De mest kända komplexitetsgränserna för LLW beror på Urquhart [24]: genom en minskning från täckning i vektor tilläggssystem [15], han härleder en EXPSPACE lägre gräns, mycket långt från 1 Varianter av LLW är populära i litteraturen om implicit komplexitet; till exempel, ljus affin linjär logik [1] är känd för att skriva exakt klass FP av polynomiska tidskalkylerbara funktioner. I detta dokument är vi dock intresserade av komplexiteten i propositionsfragmentet, snarare än komplexiteten i normaliseringen. När det gäller lambda kalkyl, våra resultat hänför sig till komplexiteten i typen av boende problem.
Komplexiteten i nåbarhet löstes för förgrening VASS av Lazic och Schmitz REF.
Non-elementary complexities for branching VASS, MELL, and extensions
{'venue': "CSL-LICS '14", 'journal': None, 'mag_field_of_study': ['Computer Science', 'Mathematics']}