Jaki jest obecny stan równoległych lub współbieżnych programów w izomorfizmie Curry-Howarda?

W Dowodach i typach Girarda możemy przeczytać:

Z algorytmicznego punktu widzenia rachunek sekwencyjny nie ma izomorfizmu Curry'ego-Howarda ze względu na wiele sposobów pisania tego samego dowodu. To uniemożliwia nam użycie go jako maszynopisu -calculus, chociaż dostrzegamy jakąś głęboką strukturę tego rodzaju, prawdopodobnie związaną z równoległością.$\lambda$

Dowody i typy , JY Girard (strona 28)

Ale możemy to również przeczytać (o logice liniowej)

Z punktu widzenia informatyki daje nowe podejście do kwestii lenistwa, skutków ubocznych i przydziału pamięci [GirLaf, Laf87, Laf88] z obiecującymi zastosowaniami równoległości.

Dowody i typy , JY Girard (strona 149, napisane przez Yvesa Lafonta)

W jaki sposób równoległe programy są powiązane z izomorfizmem Curry-Howarda? Jakie są obecne przemyślenia na ten temat?

Jednoczesne Logical Framework jest jeden interesujący obszar łącznie z jego potomków, jak Linear meldunku i LolliMon . Opiera się to na intuicyjnej logice liniowej.

Klasyczna logika liniowa ma połączenia z liniową chemiczną maszyną abstrakcyjną (CHAM), jak opisano np . Rachunkiem dla sieci interakcji opartym na liniowej chemicznej maszynie abstrakcyjnej, który wyraźnie opisuje wynik jako wynik typu Curry-Howarda.

Teza Aleksandra Summersa Curry-Howard Termin Calculi dla klasycznych logiki w stylu Gentzen, której nie czytałem, wydaje się być skierowana bezpośrednio na problem zapewnienia korespondencji Curry-Howarda dla rachunku w stylu Gentzen. The$\lambda\mu$-calculus Curiena i Herbelina wprowadzony w The Duality of Computation jest przełomowym dziełem w tym stylu (nieliniowych) obliczeń lambda odpowiadających logice klasycznej.

W każdym razie jest to wciąż żywy obszar badań. Istnieje wiele ostatnich artykułów na ten temat. Powyższe nawet nie wspomina o jeszcze bardziej strukturalnej stronie logiki separacji i odpowiedniej Teorii Typu Hoare'a, która koncentruje się na imperatywnych językach programowania. Na przykład istnieje „ W kierunku semantyki teoretycznej dla współbieżności transakcyjnej”, której odniesienia można prześledzić dla wcześniejszej pracy.

(Jako trochę pedantyczna uwaga, większość z nich koncentruje się na współbieżności , a nie na równoległości jako takiej ).

Jeśli chodzi o współbieżność, istnieje bardzo aktywna linia badań, którą starałem się streścić w tej odpowiedzi: https://cs.stackexchange.com/a/102711/98901

Poniżej zamieszczam komentarz dotyczący równoległości.

Avron [1996] wprowadził pojęcie hipseksekwencji , tj. Zbiory sekwencji w osądach.

W [Kokke i in., 2019] pokazaliśmy, że konserwatywne rozszerzenie logiki liniowej hipersekwencjami może być użyte do wpisania równoległości w obliczeniach procesowych. Zasadniczo, jeśli masz dwa niezależne dowody w logice liniowej hipersekwencji$\mathcal{G}$ i $\mathcal{H}$odpowiednio, możesz wyprowadzić $\mathcal{G} | \mathcal{H}$, gdzie $|$jest operatorem tworzenia hipersekwencji. Zgodnie z interpretacją Abramsky'ego „Proofs as Processes” [Abramsky, 1996] otrzymujemy regułę typowania dla paralelizmu: powiedz, że masz dwa niezależne procesy$P$ i $Q$ wpisane przez $\mathcal G$ i $\mathcal H$odpowiednio; następnie skład równoległy$P|Q$ (z $P$ i $Q$ niezależny) jest wpisany przez $\mathcal G | \mathcal H$.

Właśnie zaczęliśmy zarysowywać powierzchnię semantycznej interpretacji tego, ale to, że jest to paralelizm, jest dość oczywiste: semantyka kompozycji równoległej pozwala widzieć równoczesne działania z obu procesów, aw artykule znajduje się twierdzenie, że żadne z nich oba procesy muszą poczekać, aż drugi wykona co najmniej pewne działanie (Twierdzenie o gotowości). Wydłużenie do więcej niż dwóch działań jednocześnie wydaje się proste. (Pisanie już na to pozwala, ale semantyka w tym dokumencie nie wykorzystuje go w pełni).