Jaki jest ludowy model logiki liniowej?

Prawdopodobnie najczęstszym zastosowaniem typów liniowych w PL jest użycie ich do nadania języków, które kontrolują aliasing (tzn. Wartość liniowa ma mniej więcej jeden wskaźnik).

Ale istnieje niewielkie niedopasowanie między tym użytkowaniem a typowymi denotacyjnymi modelami logiki liniowej. IIRC, Benton wykazał, że jeśli kartezjańska zamknięta kategoria ma silną przemienną monadę, to jej kategoria algeb będzie symetryczna zamknięta monoidalnie (tj. Model logiki liniowej). Ale to twierdzenie nie dotyczy użycia kontroli aliasów, ponieważ monada stanu nie jest przemienna. I rzeczywiście, w ciągu ostatnich kilku lat Simpson i jego współpracownicy podali rachunki dla ogólnych silnych monad, które nie są terminami dla logiki liniowej.

Moje pytanie brzmi: jaka jest semantyka denotacyjna języków liniowych ze stanem? Czy istnieje nie-zdegenerowana (tj. Tensor nie jest produktem kartezjańskim) symetryczna monoidalna kategoria zamknięta, w której można modelować alokację, odczyt i aktualizację liniową?

Wydaje mi się, że kierunek, który należy rozważyć, obraca się wokół semantyki gry dla ogólnych odniesień i związanej z nią semantyki dla logiki liniowej, takiej jak te oparte na grach Conwaya . Algebraiczna relacja odniesień do semantyki gry autorstwa Paula-André Mellièsa i Nicolasa Tabareau jest prawdopodobnie najlepszym miejscem na początek. W tym artykule logika liniowa jest zrelaksowana w stosunku do tak zwanej logiki tensorowej, aby wszystko działało, więc nie jest to pożądane ustawienie. Ale polegają na grach Conway, więc z pewnością istnieje związek z modelami logiki liniowej. Nie wykorzystują też tak naprawdę liniowości, jak w typach liniowych, ale maszyneria jest dostępna, jeśli chcesz, jak sądzę.

Prace Jima Lairda (takie jak A Game Semantics of Names and Pointers ) i Guy McCusker mogą również przyczynić się do twojej misji. Niedawna ciekawa teza Semantyka gry dla zorientowanego obiektowo języka autorstwa Nicholasa Wolversona popycha te idee dalej w ustawieniach OO. Rozważa szczegółowo wątki liniowe , tylko jedna operacja aktywna na raz i opisuje, jak dodać klasy liniowe . Oba opierają się na pisaniu liniowym. Ponownie jednak podstawowy model nie jest ściśle modelem logiki liniowej, ale jest blisko.

(Boże, Neel, to było trudne pytanie).

„Ludowy model” logiki liniowej jest zdecydowanie spójnym modelem przestrzeni, omówionym w artykule Girarda w Linear Logic (a także w „Dowodach i typach”). To nie jest zdegenerowane w sensie, który opisujesz.

Czy ta semantyka rzuca jakiekolwiek światło na sposób implementacji liniowego języka funkcjonalnego, nie jestem pewien. Kiedy mówisz o alokacji, czytaniu i aktualizacji liniowej, naprawdę mówisz o implementacji. Być może więc twoje pytanie może zostać sformułowane jako „jak udowodnić poprawność implementacji liniowego języka funkcjonalnego wykorzystującego aktualizację stanu?” Nie znam odpowiedzi na to pytanie, ale myślę, że musi istnieć w dokumentach, które proponują liniowe aktualizacje.