Линейна логика

Съдържание:

Линейна логика
Линейна логика
Anonim

Навигация за влизане

  • Съдържание за участие
  • библиография
  • Академични инструменти
  • Friends PDF Preview
  • Информация за автора и цитирането
  • Върнете се в началото

Линейна логика

Първо публикувано сря 6 септември 2006 г.; съществена ревизия пт 24 май 2019 г.

Линейната логика е усъвършенстване на класическата и интуиционистичната логика. Вместо да подчертава истината, както в класическата логика, или доказателството, както в интуиционистичната логика, линейната логика подчертава ролята на формулите като ресурси. За да се постигне този фокус, линейната логика не позволява обичайните структурни правила за свиване и отслабване да се прилагат за всички формули, а само за тези формули, маркирани с определени модали. Линейната логика съдържа напълно инволютивно отрицание, като същевременно поддържа силна конструктивна интерпретация. Линейната логика също предоставя нови поглед върху същността на доказателствата както в класическата, така и в интуиционистичната логика. Като се съсредоточи върху ресурсите, линейната логика намери много приложения в компютърните науки.

  • 1. Въведение

    • 1.1 Малко история
    • 1.2 Линейна логика и компютърни науки
  • 2. Системи за доказване

    • 2.1 Последователно смятане
    • 2.2 Фокусирано търсене на доказателство
    • 2.3 Доказателски мрежи
  • 3. Семантика

    • 3.1 Семантика на измеримостта
    • 3.2 Семантика на доказателствата
  • 4. Сложност
  • 5. Въздействие на компютърните науки

    • 5.1 Нормализиране на доказателствата
    • 5.2 Търсене на доказателство
  • 6. Вариации

    • 6.1 Различни третирания на модалността
    • 6.2 Некомутативна линейна логика
    • 6.3 Лечение на неограничено поведение
  • библиография
  • Академични инструменти
  • Други интернет ресурси
  • Свързани записи

1. Въведение

1.1 Малко история

Линейната логика е въведена от Жан-Ив Жирар в неговото първоначално произведение (Girard 1987). Докато произходът на откриването на тази нова логика идва от семантичен анализ на моделите на Система F (или полиморфен (lambda) - смятане), може да се види цялата система на линейна логика като смел опит за съгласуване на красота и симетрия на системите за класическа логика с търсенето на конструктивни доказателства, довели до интуиционистичната логика.

Всъщност може да се представи фрагмент от линейна логика, известен като мултипликативна аддитивна линейна логика (MALL), като резултат от две прости наблюдения.

  • В последователното представяне на класификацията на класическата логика, правилата за съединителите "и" и "или", както и правилото за рязане и правилото за импликация могат да бъдат представени еквивалентно в добавна форма (контекстът на помещенията е същият) или мултипликативна форма (контекстът на помещенията е различен). Тези две презентации са еквивалентни в класическата логика поради наличието на няколко т. Нар. „Структурни“правила, а именно свиване и отслабване.
  • Неконструктивните доказателства, които човек може да изпълни в класическата логика, действително използват при представянето на последователни смятания едно или друго от тези структурни правила.

Така че, ако искаме да премахнем неконструктивните доказателства, без да разрушим симетрията на последователното смятане, както е направено в интуиционистичната логика, можем вместо това да опитаме да премахнем правилата за свиване и отслабване. Правейки това, ни остават две различни версии на всеки съединител: адитивна версия и мултипликативна версия за свързване и разделяне. Тези различни версии на един и същи connecitve вече не са еквивалентни. Тези нови съединители са & ("с", добавка и), (oplus) ("плюс", добавка или, (otimes) ("тензор", мултипликативно и) и (lpar) („Номинална“, мултипликативна или).

Това дублиране на съединителите всъщност води до много по-ясно разбиране на конфликта между класическата и интуиционистичната логика. Например законът на изключената средна ((A) или не - (A)) се счита за валиден в класическия свят и за абсурден в интуиционистичния. Но в линейна логика този закон има две показания: версията на добавката ((A / oplus / neg A)) не е доказаема и съответства на интуиционистичния прочит на дизъюнцията; мултипликативната версия ((A / lpar / neg A)) е тривиално доказуема и просто съответства на тавтологията ((A) предполага (A)), която е напълно приемлива и в интуиционистичната логика.

Също така, свойството на дизюнкция, съществено за конструктивизма, лесно се установява за адитивното дизъюнция.

Тогава ние намираме вътре в тази по-богата логика начин да представим както нуждите на интуиционизма, така и елегантността на класическата логика: отрицанието е инволютивно, последователностите са симетрични, а съединителите са взаимоопределими. Сравнете тези свойства с тези на интуиционистичната логика, където отрицанието не е инволютивно, последователностите не са симетрични и всички съединители не могат да се определят.

Забележете обаче, че след като някой елиминира правилото за свиване и отслабване, формулите вече не се държат като неизменни стойности на истината: наистина, когато имаме доказателство за (A / Rightarrow B) и доказателство за (A) в линейна логика, като ги съставяме, ние всъщност ги консумираме, за да получим доказателство за (B), така че (A / Rightarrow B) и (A) вече не са достъпни след състава. Линейните логически формули се държат по-скоро като ресурси, които могат да бъдат използвани само веднъж.

За да се възстанови пълната експресивна сила на интуиционистичната и класическата логика, тогава е необходимо да се добави към MALL фрагмента две двойни модалности, които обикновено се наричат експоненци в литературната литературна литература. По-специално, експоненциалният „разбира се“(bang) позволява свиването и отслабването да се прилага към формулата (bang B) в контекста на лявата последователност, докато експоненциалът „защо-не“(quest) позволява свиването и отслабването да се прилага към формулата (quest B) в контекста на дясната последователност. Това води до пълната линейна логика на предложенията и до много хубава връзка с компютърните науки.

Забележете, че освен MALL, има още два широко използвани фрагмента на Linear Logic: Мултипликативна линейна логика (MLL), която е MALL без добавките на съединителите; и мултипликативна експоненциална линейна логика (MELL), която е линейна логика без добавъчните съединители.

Преди въвеждането на линейна логика през 1987 г. различни изследователи са работили върху различни видове субструктурни логики, в които не са приети всички структурни правила на Гентцен (свиване, отслабване и обмен). Ламбек проучва последователни системи за смятане, в които не е разрешено нито едно от тези структурни правила (Lambek 1958). Други примери за такава логика са уместна логика (в която отслабването не е прието) (Avron 1988, Read 1988). и аффинна логика (в която свиването не се приема) (Grishin 1981).

1.2 Линейна логика и компютърни науки

Теорията на доказателствата е фокусирана върху официалните системи за доказателство и такива формални системи са разработени за интуиционистично изчисление на предикатите, класическо изчисление на предикатите, аритметика, изчисления от по-висок ред, и много други. Интуиционистичната и конструктивна логика започна, когато хората видяха възможността да четат "(A / Rightarrow B)" като "ако ми дадеш (A), ще ти дам (B)", което е значително отклонение от класическото четене „(A) е невярно или (B) е вярно“.

Компютърните науки, от друга страна, се фокусират върху изчислителните механизми: приложение на функции, обработка на изключения, извикване на методи в обектно-ориентирани езици, присвояване на променливи и подобни набори от правила за изграждане на процеси. С изключение на това, че механизмите на тези процеси трябва да бъдат изрично изброени: функция от тип (A / rightarrow B) дава официална информация за начина на преобразуване на (A) в (B).

В даден момент тези две сетива се срещнаха. HB Curry и W. Howard разбраха, че наборът от интуиционистични изводи само за импликация е основен функционален език, наречен просто набран (lambda) - смятане: езикът за програмиране е логика, а логиката - език за програмиране. Тази запомняща се среща беше наречена „изоморфизмът на Къри-Хоуърд“(Хауърд 1980).

Линейната логика осигурява допълнителен обрат в интерпретацията на импликацията '(A / Rightarrow B)': сега може да се чете като 'дай ми толкова много (A), колкото може да ми трябва, и ще ти дам един (B) '. Идеята за копие, която е толкова важна за идеята за изчисляване, сега е включена в логиката.

Тази нова гледна точка отваря нови възможности, включително:

  • нови формули, изразяващи усъвършенствани оперативни свойства като „дай ми (A) веднъж и аз ще ти дам (B)“. Приложенията тук варират от усъвършенствано логическо програмиране, при което способността на линейната логика да представя състояния се използва (Hodas & Miller, 1994), до анализа на класическата логика и изчислителните интерпретации на нея (Abramsky 1993), до спецификацията на механизмите за изключения в програмни езици (Miller, 1996), до линейния анализ (Wadler, 1991).
  • нови правила, изразяващи ограничения за използването на копия, което води до фрагмент от линейна логика за изчисления в политай, за да се спомене само най-ефектното приложение (Baillot & Terui, 2004, Baillot 2015).
  • нови начини за представяне на доказателства (Abramsky & Jagadeesan, 1994, Girard 1987).

2. Системи за доказване

Основните предложни съединители на линейна логика са разделени на адитивни и мултипликативни съединители. Класическата конюнкция и нейната идентичност (клин) и (топ) се разделят на добавката (усилвател) (с) и (топ) (отгоре) и мултипликативната (otimes) (тензор) и 1 (един). По същия начин класическата дизъюнкция и нейната идентичност (vee) и (bot) се разделят на добавката (oplus) (oplus) и 0 (нула) и мултипликативната (lpar) (par) и (bot) (отдолу). Отрицанието обикновено се третира по един от двата начина в презентации линейна логика. Отрицанието може да се разглежда като примитивен предложителен съединител, без ограничения за възникването му във формули. Тъй като съществуват дуалности De Morgan между отрицанието и всички предложения за съединения, експоненци и количествени характеристики,възможно е също така да се третира отрицанието като специален символ, който се появява само при атомните формули. Импликациите също често се въвеждат в линейна логика чрез дефиниции: линейното импликация (B / limp C) може да бъде определена като (B ^ { bot} lpar C), докато интуитивното импликация (B / Rightarrow C) може да се определи като (взрив B / лимп C). Операторите (bang) и (quest) по различен начин се наричат модали или експоненциали. Терминът „експоненциален“е особено подходящ, тъй като, следвайки обичайната връзка между експоненция, добавяне и умножение, линейната логика поддържа еквивалентностите (bang (B / amp C) equiv (bang B / otimes / bang C)) и (quest (B / oplus C) equiv (quest B / lpar / quest C)), както и 0-арните версии на тези еквиваленти, а именно ((bang / top / equiv 1)) и ((quest 0 / equiv / bot)). Тук,използваме двоичната еквивалентност (B / equiv C), за да означаваме, че формулата ((B / limp C) amp (C / limp B)) е производна в линейна логика.

2.1 Последователно смятане

Двустранно последователно смятане за линейна логика е представено на фигурата по-долу. Забележете тук, че отрицанието се третира така, сякаш е някаква друга логическа съединителна връзка: тоест появата му във формули не е ограничена и има правила за въвеждане отляво и отдясно за отрицание. Лявата и дясната страна на последователностите са множество от формули: по този начин редът на формулите в тези контексти няма значение, но тяхното многообразие има значение.

Правила за самоличност) frac {} {B / vdash B} / textit {init} qquad / frac { Delta_1 / vdash B, / Gamma_1 / qquad / Delta_2, B / vdash / Gamma_2} { Delta_1, / Delta_2 / vdash / Gamma_1, / Gamma_2} / textit {cut}) Правила за отрицание) frac { Delta / vdash B, / Gamma} { Delta, B ^ { perp} vdash / Gamma} (cdot) ^ { perp} L / qquad / frac { Delta, B / vdash / Gamma} { Delta / vdash B ^ { perp}, / Gamma} (cdot) ^ { perp} R) Мултипликативни правила) frac { Delta / vdash / Gamma} { Delta, / one / vdash / Gamma} / един L / qquad / frac {} { vdash / one} / един R)) frac { } { bot / vdash} / bot L / qquad / frac { Delta / vdash / Gamma} { Delta / vdash / bot, / Gamma} / bot R)) frac { Delta, B_1, B_2 / vdash / Gamma} { Delta, B_1 / ot B_2 / vdash / Gamma} / от L / qquad / frac { Delta_1 / vdash B, / Gamma_1 / qquad / Delta_2 / vdash C, / Gamma_2} { Delta_1, / Delta_2 / vdash B / ot C, / Gamma_ {1}, / Gamma_ {2}} / ot R)) frac { Delta_1, B / vdash / Gamma_1 / qquad / Delta_2, C / vdash / Gamma_2} { Delta_1, / Delta_2, B / lpar C / vdash / Gamma_1, / Gamma_2} / lpar L / qquad / frac { Delta / vdash B, C, / Gamma} { Delta / vdash B / lpar C, / Gamma} / lpar R) Правила за добавки) frac {} { Delta, / zero / vdash / Gamma} / zero L / qquad / frac {} { Delta / vdash / top, / Gamma} / top R)) frac { Delta, B_i / vdash / Gamma} { Delta, B_1 / amp B_2 / vdash / Gamma} { amp} L (i = 1,2) qquad / frac { Delta / vdash B, / Gamma / qquad / Delta / vdash C, / Gamma} { Delta / vdash B / amp C, / Gamma} { amp} R)) frac { Delta, B / vdash / Gamma / qquad / Delta, C / vdash / Gamma} { Delta, B / oplus C / vdash / Gamma} { oplus} L / qquad / frac { Delta / vdash B_i, / Gamma} { Delta / vdash B_1 / oplus B_2, / Gamma} { oplus} R (i = 1,2)) Правила за количествено определяне) frac { Delta, B [t / x] vdash / Gamma} { Delta, / forall xB / vdash / Gamma} / forall L / qquad / frac { Delta / vdash B [y / x], / Gamma} { Delta / vdash / forall xB, / Gamma} / forall R)) frac { Delta / vdash B [t / x], / Gamma} { Delta / vdash / съществува xB / Gamma} / съществува R / qquad / frac { Delta, B [y / x] vdash / Gamma} { Delta, / съществува xB / vdash / Gamma} / съществува L,) Експоненциални правила) frac { Delta / vdash / Gamma} { Delta, / bang B / vdash / Gamma} / bang W / quad / frac { Delta, / bang B, / bang B / vdash / Gamma} { Delta, / bang B / vdash / Gamma} / bang C / quad / frac { Delta, B / vdash / Gamma} { Delta, / bang B / vdash / Gamma} / bang D)) frac { Delta / vdash / Gamma} { Delta / vdash / quest B, / Gamma} / quest W / quad / frac { Delta / vdash / quest B, / quest B, / Gamma} { Delta / vdash / търсене B, / Gamma} / quest C / quad / frac { Delta / vdash B, / Gamma} { Delta / vdash / quest B, / Gamma} / quest D)) frac { bang / Delta / vdash B, / quest / Gamma} { bang / Delta / vdash / bang B, / quest / Gamma} / bang R / quad / frac { bang / Delta, B / vdash / quest / Gamma} { взрив / Delta, / quest B / vdash / quest / Gamma} / quest L)

Забележете, че правилата за отслабване и свиване са достъпни само за формули, отбелязани с експоненциал (взрив) отляво или (quest) отдясно на последователността. Правилата (quest) R и (bang) L често се наричат правила за „отпадане“. Правилата (quest) L и (bang) R често се наричат правила за „промоция“и са същите като правилата за възможността и необходимостта, намерени в модалната логика на S4 на Kripke. Обичайното условие за (forall) - дясно и (съществува) - правилата за въвеждане в ляво се приемат: по-специално променливата (y) не трябва да бъде свободна във формулите на долната последователност на тези правила за извод. Количественото определяне тук се приема, че е от първи ред: версиите с по-висок ред на линейна логика могат да се записват по стандартни редове.

Правилото за рязане може да бъде премахнато и пълнотата да се запази. Двойно, правилото на init също може да бъде премахнато, с изключение на появата на init, включващ атомни формули.

2.2 Фокусирани доказателства

Важна теорема за нормална форма за структурата на нережещите доказателства е предоставена от Andreoli (1992). Той класифицира неатомна формула като асинхронна, ако нейното логично съединител от най-високо ниво е (top), &, (bot, / lpar), (quest) или (forall) или синхронен, ако неговото логично съединител от най-високо ниво е (0, / oplus, 1, / otimes), (bang) или (съществува).

Когато разглеждаме търсенето на доказателства като изчислителен модел, можем да видим формули в последователност като „агенти“, които могат да действат независимо или в съгласие с други хора в тяхната среда. Тук действията на такива агенти се определят като се чете правилото за въвеждане за тях отдолу нагоре. Ако асинхронна формула се появи отдясно на последователност, тя може да се развие, без да повлияе на доказуемостта и без да взаимодейства с нейния контекст, т.е. съответното правило за въвеждане е необратимо. Например, агентът ((B / lpar C)) става (чрез прилагане на (lpar) - правилно правило за въвеждане) двата агента (B) и (C) (сега работят паралелно). По същия начин агентът ((B / amp C)) дава (чрез прилагане на правилото за въвеждане & -право) два различни идентични свята (последователности), с изключение на това, че (B) е в един от тези светове и (C) е в другата.

От друга страна, ако гледаме на синхронна формула като агент, чиято еволюция се определя от съответното правило за въвеждане вдясно, тогава е възможно доказуемата последователност да се развие до непроявима последователност (например чрез прилагане на (oplus) правило за въвеждане надясно). Също така, случаите на такива правила за извод зависят от подробности за контекста на формулата. Например, успехът на правилото за 1 правилно въвеждане изисква околният контекст да е празен, а успехът на правилото (otimes) - правилното въвеждане зависи от това как заобикалящият контекст на агента е разделен на два контекста. Така еволюцията на такива агенти зависи от „синхронизирането“с други части на контекста.

Сега помислете за едностранно представяне на последователно смятане на линейна логика, където единствените правила за въвеждане са правилни правила за въвеждане. Като се има предвид горната класификация на съединителите, е възможно да се покаже, че търсенето на доказателства може да бъде структурирано в следните фази без загуба на пълнота. Асинхронната фаза възниква, ако има асинхронна формула в секвенцията. В тази фаза правилата за въвеждане вдясно се прилагат в произволен ред, докато няма други асинхронни формули. В синхронната фаза се избира някаква синхронна формула и се превръща във „фокус“на тази фаза: тоест към нея се прилагат правила за правилно въвеждане и към всяка синхронна подформула, която може да генерира.

Следващата фигура илюстрира линейната логика на системата за фокусиране. Забележете, че двете фази са представени от различни стрелки: стрелката нагоре означава асинхронната фаза, а стрелката надолу означава синхронната фаза. Също така, секвенциите са разделени на три зони (където зоните са разделени или с точка и запетая или стрелка нагоре или надолу). По-специално, отляво на стрелката нагоре и надолу са двете зони. Зоната, написана като (Psi), обозначава набор от формули, които могат да бъдат използвани произволно в доказателството за тази последователност. Зоната, написана като (Delta), обозначава множество от формули, които са ограничени, както в MALL. Зоната вдясно от стрелка нагоре също е множество от формули, докато зоната вдясно от стрелка надолу е единна формула. Възможно е да се наложи произволен ред на формулите вдясно от стрелката нагоре, тъй като въвеждането на асинхронни формули може да се извърши в произволен ред. Атомите имат полярност и на фигурата по-долу (A) означава положителни атоми, а отрицанието на (A) означава отрицателни атоми. Доказателствата, изградени от тези правила за извод, се наричат фокусирани доказателства. Резултатът от Andreoli 1992 е, че фокусираните доказателства са пълни за линейна логика.

Асинхронна фаза) frac { Up { Psi} { Delta} {L}} { Up { Psi} { Delta} { bot, L}}) bot] qquad / frac { Нагоре { Psi, F} { Delta} {L}} { нагоре { Psi} { Delta} { quest F, L}}) quest])) frac {} { нагоре { Psi} { Delta} { отгоре, L}}) горе] qquad / frac { нагоре { Psi} { Delta} {F [y / x], L}} { нагоре { Psi} { Delta} { forall xF, L}}) forall])) frac { Up { Psi} { Delta} {F_1, F_2, L}} { нагоре { Psi} { Delta} {F_1 / lpar F_2, L}}) lpar] qquad / frac { Up { Psi} { Delta} {F_1, L} quad / Up { Psi} { Delta} {F_2, L}} { нагоре { Psi} { Delta} {F_1 / amp F_2, L}}) amp])) frac { Up { Psi} { Delta, F} {L}} { Up { Psi} { Delta} {F, L}} [R / Uparrow] / текст {при условие, че $ F $ не е асинхронен}) Синхронна фаза) frac {} { надолу { Psi} { cdot} { one}}) one] qquad / frac { надолу { Psi} { Delta_1} {F_1} quad / надолу { Psi} { Delta_2} {F_2}} { надолу { Psi} { Delta_1, / Delta_2} {F_1 / ot F_2}}) ot] qquad / frac { нагоре { Psi} { cdot} {F}} { Down { Psi} { cdot} { bang F}}) bang])) frac { Down { Psi} { Delta} {F_i}} { Надолу { Psi} { Delta} {F_1 / oplus F_2}}) oplus_i] qquad / frac { надолу { Psi} { Delta} {F [t / x]}} { надолу { Psi} { Delta} { съществува xF}}) съществува])) frac { нагоре { Psi} { Delta} {F}} { надолу { Psi} { Delta} {F}} [R / Downarrow] / текст {при условие, че $ F $ е или асинхронен, или атом}) Правила за идентичност и решение) frac {} { надолу { Psi} {A} {A ^ { perp}}} [I_1] qquad / frac {} { надолу { Psi, A} { cdot} {A ^ { perp}}} [I_2] / текст {където} / текст {е атом})) frac { надолу { Psi} { Delta} {F}} { нагоре { Psi} { Delta, F} { cdot}} [D_1] qquad / frac { надолу { Psi} { Delta} {F}} { нагоре { Psi, F} { Delta} { cdot}} [D_2] / текст {където} F / текст {е положителна формула})

Системите с фокусирано доказателство също са проектирани за класическа и интуиционистка логика (Danos et al. 1997; Laurent et al. 2005; Liang & Miller 2009).

2.3 Доказателски мрежи

Доказателствата, представени с помощта на последователно смятане, съдържат много подробности, които понякога са неинтересни: помислете за пример колко много безинтересно различни начини има за формиране на доказателство за (vdash / Gamma, (A_1 / lpar A_2), / ldots, (A_ { n-1} lpar A_n)) от производно на (vdash / Gamma, A_1, A_2, / ldots, A_n). Този неприятен факт произтича от последователния характер на доказателствата при последователно смятане: ако искаме да приложим набор (S) от (n) правила към различни части на последователност, не можем да ги приложим в една стъпка, дори ако те не си пречат един на друг! Трябва да ги последователно, т.е. да изберем линеен ред на (S) и да приложим правилата в (n) стъпки, в съответствие с този ред.

Възниква естествен въпрос: „Има ли представяне на доказателства, които се абстрахират от такива безинтересни детайли?“. Подобен въпрос се дава положително в случай на интуиционистично последователно смятане с помощта на това, което е известно като естествена дедукция, която чрез кореспонденцията на Къри-Хауърд има силна връзка с изчислителното устройство, известно като (lambda) - смятане,

За линейна логика това кратко представяне на доказателствата се дава от доказателствени мрежи, подобни на графични структури, които се ползват с особено добри свойства за MLL фрагмента на логиката. Първата стъпка към това представяне е да се преобразува цялата последователна изчислителна система, използвайки инволютивността на отрицанието, в едностранна система, където последователностите са с формата (vdash / Gamma). В резултат на това броят на правилата се намалява, тъй като нямаме правила за въвеждане вляво, но запазваме същата изразителна сила, тъй като доказателствеността остава същата.

Към всяко следващо доказателство за изчисление в MLL, може да се индуцира свързващо доказателство мрежа със същите заключения, както следва:

  • Към доказателство, сведено до правилото за аксиома, свързваме връзка на аксиома.

    Аксиома мрежа
    Аксиома мрежа
  • За доказателство, получено чрез прилагане на правилото на разрязване към две доказателства, първо индуктивно изграждаме доказателствените мрежи, свързани с тези две доказателства, и след това ги комбинираме с помощта на рязана връзка.

    Изрязана нетна конструкция
    Изрязана нетна конструкция
  • За доказателство, получено чрез прилагане на правилото на тензор към две доказателства, първо индуктивно изграждаме доказателствените мрежи, свързани с тези две доказателства, и след това ги комбинираме с помощта на тензорна връзка.

    Конструкция на тензорна мрежа
    Конструкция на тензорна мрежа
  • За доказателство, получено чрез прилагане на правилото par на доказателство, първо индуктивно изградете доказателствената мрежа, свързана с това доказателство, и след това добавяме „връзката par“.

    Пар нетна конструкция
    Пар нетна конструкция

Всичко това може да бъде правилно формализирано с помощта на хиперграфи (формулите са възли и „връзките“са ориентирани хипереги с хипотези и заключения) и можем официално да определим като доказателствена мрежа хиперграф, индуктивно изграден от производното изчисление на MLL. Забележете, че има доста хиперграфи, които не са доказателствени мрежи.

Сега ако погледнете доказателствената мрежа, изградена от производите на (vdash / Gamma, (A_1 / lpar A_2), / ldots, (A_ {n-1} lpar A_n)), получени от (vdash / Gamma, A_1, A_2, / ldots, A_n), ще видите, че цялата следа от реда на прилагане на правилата е изчезнала. В известен смисъл, доказателствените мрежи са клас на еквивалентност на последователни производни смятане по отношение на реда за извличане на правила, чието приложение пътува.

Да предположим, че някой сега идва при теб с огромен хиперграф, изграден с връзки на аксиома, изрязване, номинална и тензорна форма, преструвайки се, че всъщност представлява представяне на доказателството за някакъв отдавна отворен математически проблем. Как можете да потвърдите, че това всъщност е представяне на доказателство, а не само случайна структура?

Извършването на тази проверка за коректност е предизвикателство, което се състои в възстановяване на последователна история на изграждането на вашата структура, съответстваща на извода в последователно смятане, и изглежда отначало много сложен проблем: първият критерий за коректност на мрежите за доказателство за MLL, наречен „дълго пътуване критерий “и присъства в оригиналната книга на Girard, е експоненциален, както и критерият ACC (Acyclic linked) на Danos и Regnier (1989), открит по-късно. Независимо от това, съществува много по-ефективен критерий, известен като Contractibility, заради Danos и Regnier, който наскоро беше преформулиран като следния елегантен критерий за анализ на графика от Guerrini, Martini и Masini: хиперграфът е доказателство, ако и само ако тя се свежда до единичния възел „мрежа“чрез следните правила за намаляване на графиката

Графична разборка за неточно разпознаване на MLL
Графична разборка за неточно разпознаване на MLL

Наивно извършването на тази проверка може да отнеме квадратично време (всяко приложение на правило може да изисква цялостно търсене на графиката, за да намерим редекса, и ние трябва да извършим толкова стъпки, колкото има хипервръзки в графиката). Линейните алгоритми за времето са дадени от Guerrini (2011) и от Murawski and Ong (2006).

Друг критерий за коректност на мрежите за доказателство за MLL е даден от Retoré (2003), в който е даден квадратичен алгоритъм за MLL.

На доказателствени мрежи може да се извърши елиминиране на отрязване по особено чист начин: поради техния паралелен характер, разрезите могат да бъдат елиминирани локално чрез две правила за опростяване:

  • Аксиомен ход:

    Аксиомен ход
    Аксиомен ход
  • Мултипликационен ход:

    Мултипликативен ход
    Мултипликативен ход

Това всъщност са правила за изчисляване на доказателствените мрежи и критериите за коректност позволяват лесно да се провери дали всяко такова правило запазва коректността и в резултат на това намаляването на доказателствената мрежа все още идва от доказателство за последователно изчисление на същия последователност.

Следователно, елиминирането на срезовете в мрежите, устойчиви на MLL, може да се извърши в линейно време и дава прост, елегантен резултат за елиминиране на среза за всички MLL.

Подходът на доказателствените мрежи може да бъде разширен до по-големи подмножества от линейна логика, но тогава е по-малко ясно как да се получат същите елегантни резултати, както при MLL: оригиналната система, предложена в Girard 1987, работи за MELL, например чрез асоцииране към четирите експоненциални правила следните конструкции на хиперграф:

  • свиване

    Конструкция за свиване
    Конструкция за свиване
  • Отслабване

    Слабо строителство
    Слабо строителство
  • изоставяне

    Изграждане на деликт
    Изграждане на деликт
  • Промоция, която въвежда понятието „кутия“, маркировка за секвенционализация около парче доказателствена мрежа, материализирана в снимките на графиките, на правоъгълника, изчертан около доказателствената мрежа на изводите (A) и (quest / Gamma).

    Промоция строителство
    Промоция строителство

Докато тези конструкции и свързаните с тях редукции на графики имат поразително сходство с (lambda) - смятане с изрични замествания, както първо беше отбелязано от Di Cosmo & Kesner (1997), те са твърде сходни със съответните правила за последователно смятане: ефектът на паралелизация толкова елегантен за MLL не се поддържа правилно тук, а правилата за намаляване на графиката включват полета и не са местни.

За да се възстанови задоволителната система, бяха направени много предложения, като се започне от тази на Danos & Regnier (1995), но тук искаме да споменем много елегантния подход на Guerrini, Martini и Masini (Guerrini et al. 2003), което ясно показва връзката между две системи за защита на нива за модална логика, правилни мрежи за доказателство за MELL и оптимално намаляване на изчислението (lambda).

Неотдавнашен документ на Heijltjes and Houston (2016) показа, че не може да има задоволителна представа за доказателствени мрежи за MLL, ако са разрешени и единици.

Възможно е да се осигури канонично третиране на адитивни съединители, дори с количествено определяне от първи ред (Heijltjes et al. 2018). Доказателствените мрежи за формули, съдържащи както мултипликативни, така и добавъчни съединители, имат различни технически презентации, нито една от които не изглежда канонична и задоволителна. Тяхното третиране в доказателствени системи, подобни на изпитвания, понастоящем е тема на активното изследване. По-специално, вижте (Hughes and van Glabbeek 2005) и (Hughes and Heijltjes 2016).

3. Семантика

Наближаването на семантиката на линейната логика обикновено се извършва по два различни пътя. Първо, съществуват различни семантични структури, които могат да се използват за картографиране на формули и обозначения в такива структури. Този подход може да се използва за установяване на здравина и пълнота за различни фрагменти от линейна логика. По-новият семантичен подход към линейната логика включва даване на семантика директно на доказателства. Ние описваме накратко тези два подхода и предоставяме някои връзки към литературата.

3.1 Семантика на измеримостта

Един подход за опит за надеждна и пълна семантика за фрагменти от линейна логика се свързва с формула, множеството от всички контексти, които могат да бъдат използвани за доказване на тази формула. Разбира се, такава колекция може да се наложи да бъде по-абстрактна и да получи различни свойства за затваряне. Фазовата семантика на Girard (1987) предоставя една такава семантика: някои приложения на такава семантика са направени в компютърните науки за предоставяне на контрапримери и като инструмент, който може да помогне да се установи, че дадена едновременна система не може да се превърне в друга с определени свойства (Fages et съч., 2001). По подобен начин семантиката в стил Крипке е предоставена в Allwein & Dunn 1993 и Hodas & Miller 1994. Quantales, определен вид частично подредени алгебрични структури, също са използвани за предоставяне на ранни семантични модели за части от линейна логика (Yetter 1990).

3.2 Семантика на доказателствата

В аналогията на формулите като видове, която е толкова популярна и ползотворна в теоретичната компютърна наука, логическа система се поставя в съответствие с въведено изчислително устройство (като typed (lambda) - смятане), като се свързва към всяко доказателство за тази формула програма, имаща тази формула като тип. Например, доказателство за тавтологията (A / Rightarrow A) съответства на програмата fun ((x: A).x: A / rightarrow A), функцията за идентичност на обекти от тип (A), Ето защо в конструктивните логически системи (като интуиционистичната логика и аритметика) и в линейната логика толкова голямо значение се придава на доказателствата, дотолкова, че изграждането и изучаването на модели на доказателства получава толкова много повече внимание, отколкото изграждането и изучаването на модели на доказуемост: не сме доволни да знаем, че формула е доказаема,ние наистина искаме да знаем изчислителното съдържание на неговото доказателство.

Предложени са много модели на линейни логически доказателства; считаме, че към днешна дата най-простата и интуитивна конструкция са тези, базирани на т. нар. „релационна семантика“или „семантика в стил Крипке“, където формулите се интерпретират като мултисети, а едностранните последователности се интерпретират като сборници на мултисети, а доказателствата се интерпретират като отношения спрямо интерпретацията на последователности. Ако човек иска да даде чисто теоретично зададена семантика, без да се прибягва до мултисети, е възможно да се направи с помощта на кохерентни пространства, множества, оборудвани със специално кохерентно отношение, както първоначално е показано в Girard 1987. Има интересна категория теоретична модели на линейна логика, като * -автономните категории (Barr 1991) и хиперкохерентности (Ehrhard 1993).

Друг подход към семантиката на доказателствата е даден от Геометрията на взаимодействието на Жирар, който ни позволява да получим напълно алгебрична характеристика на доказателствата. Към всяка доказателствена мрежа може да се свърже частична матрица за пермутация (sigma), съответстваща на изрязаните връзки, и подходяща матрица (M) съответстващи изрази, изградени от определена динамична алгебра, които описват възможните пътища вътре в доказателствена мрежа. След това е възможно напълно да се опише доказателствената мрежа чрез формулата за изпълнение

) mathrm {EX} (sigma, M) = (1- / sigma ^ 2) наляво (sum_i M (sigma M) дясно) (1- / sigma ^ 2))

което в случая с MLL е инвариант на процеса на нормализиране. Някаква приятна връзка с резултатите, идващи от alt="sep man icon" /> Как да цитирам този запис.

сеп човек икона
сеп човек икона

Вижте PDF версията на този запис в Дружеството на приятелите на SEP.

inpho икона
inpho икона

Разгледайте тази тема за вписване в интернет философския онтологичен проект (InPhO).

Фил хартия икона
Фил хартия икона

Подобрена библиография за този запис в PhilPapers, с връзки към неговата база данни.

Други интернет ресурси

  • Линейната логическа библиография (до 1998 г.).
  • Винсент Данос и Роберто Ди Космо. Линейният логически грунд. Бележки за курса (1992).

Препоръчано: