Jaki jest ludowy model logiki liniowej?

23

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ą?

Neel Krishnaswami
źródło
6
Tego rodzaju oczekiwałbym od ciebie odpowiedzi Neela, a nie zadawania pytań. ;-)
Marc Hamann
5
jeśli możesz przyciągnąć naukowców do cstheory.stackoverflow.com, którzy są w stanie odpowiedzieć na to pytanie, świat będzie na to lepszym miejscem.
Dave Clarke,

Odpowiedzi:

9

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.

Dave Clarke
źródło
1
Po prostu ciekawy Neel. Czy przydało ci się to, czy wiedziałeś już o tych wszystkich rzeczach?
Dave Clarke
T.(ZA)=S.ZA×S.
1
Może stan globalny Udaya Reddy'ego uznany za niepotrzebny: wprowadzenie do semantyki obiektowej, J. Lisp and Symbolic Computation, 9 (1996): 7-76.
Dave Clarke
Właściwie to teraz czytam!
Neel Krishnaswami,
7

(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.

Uday Reddy
źródło
W rzeczywistości zbyt łatwo jest udowodnić poprawność implementacji stanu liniowego - liniowość jest tak silnym ograniczeniem strukturalnym, że ledwo potrzebujesz semantyki, aby wykonać te dowody. W rezultacie nie znam prostej denotacyjnej semantyki stanu liniowego. Dwie najbliższe rzeczy, których chcę, to twoja praca nad semantyką obiektową i model „przestrzeni długości” Hofmanna w jego pracy na temat niejawnej złożoności.
Neel Krishnaswami
W rzeczywistości nie opisałbym semantyki obiektowej jako modelowania „stanu liniowego”. Jest to raczej „stan sekwencyjny” i „obiekty liniowe”, a latte narzuca SCI. Modele gier Idealized Algol, które są w tym samym sensie „oparte na obiektach”, nie mają niczego liniowego.
Uday Reddy
Czy możesz podać odniesienia do miejsc, w których można znaleźć takie dowody poprawności? (Przepraszamy, odwracam pytanie od ciebie!)
Uday Reddy
1
Najprostszym dowodem na poprawność dźwięku dla języka liniowego ze znanym stanem jest „L3: Język liniowy z lokalizacjami” Ahmeda, Flueta i Morisetta. ( ttic.uchicago.edu/~amal/papers/linloc-fi07.pdf ) W artykule podają prostą logiczną relację, ale wspominają, że przechodzi również syntaktyczny dowód postępu i zachowania.
Neel Krishnaswami
Oto kolejna praca, która właśnie zwróciła moją uwagę. Wypróbuj citeseer dla Stephena Coopera, link „On Linear Types and Imperative Update” . Powinienem był o tym wiedzieć, ale nie wiedział.
Uday Reddy