Jaka intuicja kryje się za logiką liniową?

Próbuję zrozumieć logikę liniową, aby lepiej zrozumieć systemy typu liniowego. Jednak kiedy czytam zasady, nie rozumiem za tym intuicji, jak to zrobiłem w logice modalnej - oznacza, że jest wymagane, ponieważ w ramkach Kripke jest wymagane dla każdego osiągalnego świata [ to jest możliwe mutatis mutandis]. Ale nie mogę znaleźć żadnego intuicyjnego wyjaśnienia dualizmu i tego, które pary koniunkcji / rozłączności (jeśli występują) odpowiadają i . $\Box A$ $A$ $A$ $\Diamond A$ $A$ $\land$ $\lor$

lo.logic type-theory linear-logic

— Maciej Piechotka
źródło

Oryginalny papier Girarda jest miejscem, w którym powinieneś spojrzeć, jeśli chcesz zrozumieć intuicję. Pytanie, jakie jest, jest zbyt ogólne, a odpowiedzią byłoby poszukać logiki liniowej na stronie Wikipedii.

— Kaveh

Zgadzam się, że to trochę za mało i zdecydowanie nie jest to poziom badań, może powinieneś zadać pytanie na CS Stack Exchange. Odradzałbym jednak korzystanie z oryginalnego papieru Girarda jako punktu wejścia do logiki liniowej. Może Wikipedia jest lepszym miejscem do rozpoczęcia.

— Damiano Mazza

To jest dość szerokie. Być może sugestia może zacząć traktować formuły jako „walutę”, którą można wydać, zamiast stwierdzeń prawdy. Następnie spójnik może być

czemu można spędzić zarówno

monetę i

monetę. Innym rodzajem koniunkcji może być

, co oznacza, że możemy wybierać między wydatkami

i wydatkami

(ale nie oba!). Możesz znaleźć kilka przykładów na Wikipedii, jak sugerował Damiano.

a \otimes b

$a \otimes b$

a

$a$

b

$b$

a & b

$a \& b$

a

$a$

b

$b$

— chi

@chi Nie jestem pewien, czy „interpretacja zasobów” jest najlepszym sposobem na zrozumienie dualności w LL. Interpretacja procesu jest znacznie bardziej zrozumiała.

— Martin Berger,

Nie jestem pewien, czy to pytanie jest idealne dla CSTheory, ale biorąc pod uwagę, że już zbiera opinie, oto odpowiedź, którą ktoś mógłby udzielić, gdyby pytanie zostało opublikowane na cs.stackexchange .

Aby zrozumieć pojęcie dualności logiki liniowej , która rozdziela koniunkcję i dysjunkcję znacznie dalej niż jesteśmy przyzwyczajeni w konwencjonalnej logice, zalecam nie myśleć o logice liniowej pod względem zasobów (chociaż jest to ważna lektura ). Zamiast tego pomyśl o liniowych formułach logicznych jako procesach komunikujących się w porcie / nazwie / kanale. Zgodnie z moją najlepszą wiedzą interpretacja ta została rozwinięta w pierwszej części (1), ale nawiązuje do niej już oryginalna praca Girarda. Jako obraz: $(\cdot)^{\bot}$ $A$

$A \otimes B$ $A$ $B$ $A \otimes B$ $(a, b)$ $a$ $A$ $b$ $B$

$(.)^{\bot}$ $A \otimes B$

(A \otimes B)^{⊥} = A^{⊥} ⅋ B^{⊥}

$(A \otimes B)^{\bot} \quad = \quad A^{\bot} ⅋ B^{\bot}$

W tym odczytu jest proces, który komunikuje się z . $A^{\bot} ⅋ B^{\bot}$ $A \otimes B$

Odpowiednik dysocjacji w logice liniowej może otrzymać podobny odczyt teoretyczny. Formuła

A & B

$A\ \&\ B$

powinny być również postrzegane jako dwa równoległe procesy i , ale zamiast aktywnie wysyłać wiadomości, czekają, aż środowisko zdecyduje, które uruchomić. Więc siedzi tam, czekając na jego kanale na trochę informacji, które decyduje czy powinny działać jako lub . Jest to „równoległa” wersja w sekwencyjnych językach programowania. Podwójny z jest $A$ $B$ $A \& B$ $A \& B$ $A$ $B$ $if/then/else$ $(A \& B)^{\bot}$ $A \& B$

(A & B)^{⊥} = A^{⊥} \oplus B^{⊥}

$(A \& B)^{\bot} \quad = \quad A^{\bot} \oplus B^{\bot}$

może być postrzegany jako proces wysyłający 1 bit informacji do , a mianowicie: „kontynuuj jako ” lub „kontynuuj jako ”. Jest to podobne do tego w oceniany na podczas oceniany na , z tym że wybór między i jest teraz dokonywany przez środowisko. $A \& B$ $A$ $B$ $if\ true\ then\ P\ else\ Q$ $P$ $if\ false\ then\ P\ else\ Q$ $Q$ $A$ $B$

Operator! Ma również interpretację teoretyczną: jeśli jest odczytywany jako proces, to można odczytać jako uruchamiający nieskończenie wiele procesów równolegle.

A

$A$

! A

$!A$

A

$A$

W tym odczytu axioms liniowych logicznych się proste „przewody”, które przekazywania komunikatów z procesów do procesów . Ta interpretacja aksjomatów znajduje się już w siatkach dowodowych Girarda (3). $A \vdash A$ $A^{\bot}$ $A$

Ta interpretacja teoretyczna procesu miała wpływ i spowodowała wiele dalszych prac, takich jak np. (2) dla typów sesji. Niemniej jednak istnieją pewne przypadki krawędzi, które sprawiają, że jest to trochę niezręczne, i zgodnie z moją wiedzą nie zostało stworzone, aby działało idealnie dla pełnej logiki liniowej nawet w 2017 roku.

_{1. S. Abramsky, Interpretacje obliczeniowe logiki liniowej .

2. P. Wadler, Propozycje jako sesje .

3. Wikipedia, siatka próbna .}

— Martin Berger
źródło