Cirkelräkning

Cirquents kan ses som samlingar av sekvenser med möjligen delade element

Cirquent calculus är en beviskalkyl som manipulerar grafliknande konstruktioner som kallas cirquents , i motsats till de traditionella trädliknande objekten som formler eller sekvenser . Cirquents finns i en mängd olika former, men de delar alla ett huvudsakligt kännetecken, vilket gör dem annorlunda än de mer traditionella föremålen för syntaktisk manipulation. Denna funktion är möjligheten att explicit redogöra för eventuell delning av underkomponenter mellan olika komponenter. Det är till exempel möjligt att skriva ett uttryck där två deluttryck F och E , medan inget av dem är ett deluttryck av det andra, fortfarande har en gemensam förekomst av ett deluttryck G (i motsats till att ha två olika förekomster av G , en i F och en i E ).

Översikt

Tillvägagångssättet introducerades av G. Japaridze som en alternativ bevisteori som kan "tämja" olika icke-triviala fragment av hans beräkningsbarhetslogik , som annars hade motstått alla försök till axiomatisering inom de traditionella bevisteoretiska ramarna. Ursprunget till termen "cirquent" är CIRcuit+seQUENT, eftersom den enklaste formen av kretslopp, även om den liknar kretsar snarare än formler, kan ses som samlingar av ensidiga sekvenser (till exempel sekvenser av en given nivå av en Gentzen -style proof tree) där vissa sekvenser kan ha delade element.

Cirquent för "två av tre" kombinationen av resurser, outsäglig i linjär logik

Den grundläggande versionen av cirquent kalkyl i åtföljdes av en " abstrakt resurssemantik " och påståendet att den senare var en adekvat formalisering av resursfilosofin som traditionellt förknippas med linjär logik . Baserat på det påståendet och det faktum att semantiken inducerade en logik som var riktigt starkare än (affin) linjär logik, hävdade Japaridze att linjär logik var ofullständig som en resurslogik. Vidare hävdade han att inte bara den deduktiva kraften utan också den uttryckskraften hos linjär logik var svag, för den, till skillnad från cirkvent kalkyl, misslyckades med att fånga det allestädes närvarande fenomenet resursdelning.

Linjär logik förstår den visade formeln som den vänstra kretsen, medan klassisk logik som den högra kretsen

Resursfilosofin kring cirkulär kalkyl ser tillvägagångssätten för linjär logik och klassisk logik som två ytterligheter: den förra tillåter inte någon delning alls, medan i den senare "delas allt som kan delas". Till skillnad från cirkulär kalkyl tillåter ingen av metoderna således blandade fall där vissa identiska underformler delas och andra inte.

Bland de senare hittade tillämpningarna av cirkvent kalkyl var användningen av den för att definiera en semantik för rent propositionell oberoende-vänlig logik . Motsvarande logik axiomatiserades av W. Xu.

Syntaktiskt sett är cirkventa kalkyler djupa slutledningssystem med den unika egenskapen att dela delformler. Denna funktion har visat sig ge snabba upp för vissa bevis. analytiska bevis för polynomstorleken för det propositionella hålet konstruerats. Endast kvasipolynomiska analytiska bevis har hittats för denna princip i andra djupa slutledningssystem. I upplösnings- eller analytiska Gentzen-liknande system duvhålsprincipen känd för att endast ha exponentiell storleksbevis.

Litteratur

externa länkar


Hämtad från " https://en.wikipedia.org/w/index.php?title=Cirquent_calculus&oldid=1135811811 "