Obvodový počet - Cirquent calculus

Na kruhy lze pohlížet jako na sbírky sekvencí s případně sdílenými prvky

Obvodový počet je důkazní kalkul který manipuluje konstrukty ve stylu grafu nazývané obvody, na rozdíl od tradičních stromových objektů, jako jsou vzorce nebo sekvence. Okruhy přicházejí v různých formách, ale všechny sdílejí jeden hlavní charakteristický rys, který je odlišuje od tradičnějších předmětů syntaktické manipulace. Touto funkcí je schopnost explicitně zohlednit možné sdílení dílčích komponent mezi různými komponentami. Například je možné napsat výraz, kde dva dílčí výrazy F a E, zatímco žádný z nich není subexpresí druhého, stále se běžně vyskytuje subexpresi G (na rozdíl od dvou různých výskytů G, jeden dovnitř F a jeden dovnitř E).

Přehled

Přístup představil G. Japaridze v[1] jako alternativní důkazní teorie schopná „zkrocení“ různých jeho netriviálních fragmentů logika vypočítatelnosti, které by jinak odolávaly všem axiomatizačním pokusům v tradičních rámcích důkazní teorie.[2][3] Původ termínu „cirquent“ je CIRcuit + seQUENT, jako nejjednodušší forma cirquentů, připomínající obvodů spíše než vzorce, lze považovat za kolekce jednostranných sekvence (například sekvence dané úrovně kontrolního stromu stylu Gentzen), kde některé sekvence mohou mít sdílené prvky.

Jde o kombinaci zdrojů „dva ze tří“, která je v lineární logice nevyjádřitelná

Základní verze kruhového počtu v systému Windows[4] byl doprovázen „abstraktní sémantika zdrojů„a tvrzení, že to byla adekvátní formalizace filozofie zdrojů tradičně spojená s lineární logika. Na základě tohoto tvrzení a skutečnosti, že sémantika vyvolala logiku řádně silnější než (afinní) lineární logiku, Japaridze tvrdil, že lineární logika byla neúplná jako logika zdrojů. Dále tvrdil, že nejen deduktivní síla, ale také expresivní síla lineární logiky byla slabá, protože na rozdíl od současného počtu nedokázala zachytit všudypřítomný fenomén sdílení zdrojů.[5]

Lineární logika chápe zobrazený vzorec jako levý kruh, zatímco klasická logika jako pravý kruh

Filozofie zdrojů cirkulárního počtu vidí přístupy lineární logika a klasická logika jako dva extrémy: první neumožňuje vůbec žádné sdílení, zatímco ve druhém „je sdíleno všechno, co lze sdílet“. Na rozdíl od aktuálního počtu tedy ani jeden přístup neumožňuje smíšené případy, kdy jsou sdíleny některé stejné podformule a jiné ne.

Mezi později nalezenými aplikacemi cirkulárního počtu bylo jeho použití k definování sémantiky pro čistě výrokovou logika vstřícná k nezávislosti.[6] Odpovídající logika byla axiomatizována W. Xu.[7]

Syntakticky jsou cirkulující kameny hluboký závěr systémy s jedinečnou vlastností sdílení dílčích modelů. Ukázalo se, že tato funkce poskytuje zrychlení pro určité nátisky. Byly například konstruovány analytické důkazy o polynomiální velikosti pro výrokovou pigeonhole.[8] V tomto hlubokém inferenčním systému byly pro tento princip nalezeny pouze kvazipolynomiální analytické důkazy.[9] V rozlišovacích nebo analytických systémech Gentzenova stylu je známo, že princip pigeonhole má pouze důkazy o exponenciální velikosti.[10]

Reference

  1. ^ G. Japaridze, “Úvod do cirkulárního počtu a sémantiky abstraktních zdrojů “. Journal of Logic and Computation 16 (2006), str. 489–532.
  2. ^ G. Japaridze, “Zkrocení opakování v logice vypočítatelnosti pomocí obíhajícího počtu, část I. “. Archiv pro Mathematical Logic 52 (2013), strany 173-212.
  3. ^ G.Japaridze, "Zkrocení opakování logiky vypočítatelnosti pomocí obracejícího se počtu, část II." „Archiv pro Mathematical Logic 52 (2013), strany 213–259.
  4. ^ G. Japaridze, “Úvod do cirkulárního počtu a sémantiky abstraktních zdrojů ". Journal of Logic and Computation 16 (2006), str. 489–532.
  5. ^ G. Japaridze, “Okruhový počet se prohloubil. “ Journal of Logic and Computation 18 (2008), str. 983–1028.
  6. ^ G. Japaridze, “Od vzorců po okruhy v logice vypočítatelnosti “. Logical Methods is Computer Science 7 (2011), Issue 2, Paper 1, pp. 1-55.
  7. ^ W.Xu, “Výrokový systém indukovaný přístupem Japaridze k logice IF “. Logic Journal of the IGPL 22 (2014), strany 982–991.
  8. ^ G. Japaridze, “Okruhový počet se prohloubil. “ Journal of Logic and Computation 18 (2008), str. 983–1028.
  9. ^ A. Das, “Na pigeonhole a souvisejících principech v systémech Deep Inference a Monotone ”.
  10. ^ A. Haken, “Neřešitelnost řešení “. Theoretical Computer Science 39 (1985), str. 297-308.

Literatura

externí odkazy