Stochastyczne obliczenia lambda Scotta

Ostatnio Dana Scott zaproponowała stochastyczny rachunek lambda, próbę wprowadzenia elementów probabilistycznych do (nietypowego) rachunku lambda w oparciu o semantykę zwaną modelem grafowym. Jego slajdy można znaleźć na przykład w Internecie , a jego artykuł w Journal of Applied Logic , t. 12 (2014).

Jednak po szybkim przeszukaniu Internetu znalazłem podobne wcześniejsze badania, na przykład dotyczące systemu typu Hindley-Milner . Sposób, w jaki wprowadzają semantykę probabilistyczną, jest podobny do Scott'a (w pierwszym używają monad, w drugim Scott stosuje styl kontynuacji).

W jaki sposób dostępna jest praca Scotta od poprzedniej, jeśli chodzi o same teorie lub ich możliwe zastosowania?

Jedną z widocznych zalet jego podejścia jest to, że umożliwia obserwowanie wyników funkcji wyższego rzędu (tj. Warunków lambda), co na ogół jest dość trudne. (Podstawowym problemem jest to, że przestrzenie funkcji mierzalnych na ogół nie mają borel -algebry, dla której funkcja aplikacji - czasami nazywana „eval” - jest mierzalna; patrz wprowadzenie do papierowych struktur Borela dla przestrzeni funkcji .) Scott robi to za pomocą Kodowanie Gödela od terminów lambda do liczb naturalnych i praca bezpośrednio z zakodowanymi terminami. Jedną słabością tego podejścia może być to, że kodowanie może być trudne do rozszerzenia przy użyciu liczb rzeczywistych jako wartości programu. (Edycja: To nie jest słabość - patrz komentarz Andreja poniżej.)$\sigma$

Wydaje się, że użycie CPS służy przede wszystkim do narzucenia całkowitego obliczenia, w celu nałożenia całkowitego zamówienia na dostęp do losowego źródła. Stanowa monada powinna równie dobrze.

„Zmienne losowe” Scotta wydają się być takie same jak „funkcje próbkowania” Parka w jego semantyce operacyjnej . Technika przekształcania standardowych wartości jednolitych w wartości o dowolnym rozkładzie jest szerzej znana jako próbkowanie z transformacją odwrotną .

Uważam, że istnieje tylko jedna zasadnicza różnica między semantyką Ramseya i Scotta. Ramsey interpretuje programy jako obliczenia, które budują miarę na wynikach programu. Scott zakłada istniejącą jednolitą miarę nakładów i interpretuje programy jako transformacje tych nakładów. (Miarę wyjściową można w zasadzie obliczyć na podstawie obrazów ). Scott's jest analogiczny do używania losowej monady w Haskell.

W ogólnym ujęciu semantyka Scotta wydaje się najbardziej podobna do drugiej połowy mojej rozprawy na temat języków probabilistycznych - z wyjątkiem tego, że utknąłem przy wartościach pierwszego rzędu zamiast sprytnego kodowania, użyłem nieskończonych drzew liczb losowych zamiast strumieni i interpretowałem programy jako obliczenia strzałek. (Jedna ze strzałek oblicza transformację ze stałej przestrzeni prawdopodobieństwa do wyników programu; inne obliczają preimages i przybliżone preimages). Rozdział 7 mojej rozprawy wyjaśnia, dlaczego myślę, że interpretowanie programów jako transformacji stałej przestrzeni prawdopodobieństwa jest lepsze niż interpretowanie ich jako obliczeń które budują miarę. Zasadniczo sprowadza się to do „punktów stałych miar są o wiele skomplikowane, ale rozumiemy punkty stałe programów całkiem dobrze”.