Dla jakich języków istnieje już teoria równoważności obserwacyjnej?

Dla potwierdzenia poprawności szukam użytecznego pojęcia równoważności programu dla systemów czystego typu (PTS) Barendregta; brakuje tego, dla wystarczającej liczby systemów określonego typu. Moim celem jest po prostu użycie tego pojęcia, a nie badanie go dla samego siebie. $\cong$

Pojęcie to powinno być „ ekstensywne ” - w szczególności, aby udowodnić, że , powinno wystarczyć, aby udowodnić, że $t_1 \cong t_2$ dla wszystkich wartości odpowiedniego typu. $t_1\; v \cong t_2\; v$ $v$

Równoważność denotacyjna

Równoważność denotacyjna z łatwością spełnia wszystkie właściwe lematy, ale semantyka denotacyjna dla arbitralnego PTS wydaje się dość trudna - już dla systemu F. wydawałoby się trudne.

Równoważność kontekstowa / obserwacyjna

Oczywistą alternatywą są wówczas różne formy równoważności kontekstowej (dwa terminy są równoważne, jeśli żaden kontekst gruntowy ich nie rozróżnia), ale jego definicja nie jest natychmiast użyteczna; różne lematy nie są łatwe do udowodnienia. Czy zostały udowodnione dla PTS? Alternatywnie, czy teoria byłaby „oczywistym rozszerzeniem”, czy też istnieje powód, by sądzić, że teoria byłaby znacząco inna?

EDYCJA: Nie powiedziałem tego, co jest trudne powyżej.

Prosta część: definicja

Określenie równoważności nie jest zbyt trudne, a definicja pojawia się w wielu artykułach (zaczynając przynajmniej od badań PCF Plotkina z 1975 r., Jeśli nie wcześniej - źródłem może być praca doktorska Morrisa z 1968 r.). We jeśli dla wszystkich kontekstów naziemnych , - to znaczy, że i dają ten sam wynik $t_1 \cong t_2$ $C$ $C[t_1] \simeq C[t_2]$ $C[t_1]$ $C[t_2]$ . Masz kilka wyborów tutaj z wielu alternatyw: Na przykład, w języku, silnie normalizacji, jeśli masz rodzaj uziemienia Naturals, można powiedzieć, że konteksty ziemne są te, które Naturals powrotu, a następnie oznacza, że i oceniają na tę samą liczbę. W przypadku nieterminacji, dla rozsądnych języków wystarczy użyć „X terminates” jako obserwacji, ponieważ jeśli dwa programy są równoważne podczas obserwowania zakończenia, są one również równoważne podczas obserwowania wyniku. $a \simeq b$ $a$ $b$

Trudna część: dowody

Jednak dokumenty te często nie wyjaśniają, jak trudno jest faktycznie używać tej definicji. Wszystkie poniższe odnośniki pokazują, jak sobie z tym poradzić, ale potrzebna teoria jest trudniejsza niż się wydaje. Jak udowodnimy, że ? Czy faktycznie przeprowadzamy analizę przypadków i wprowadzamy konteksty? Nie chcesz tego robić. $t_1 \cong t_2$

Jak zauważa Martin Berger, zamiast tego chcesz użyć bisimulacji (jak to uczynił Pitts) lub logicznej relacji równoważności (którą Harper po prostu nazywa „logiczną równoważnością”).

Wreszcie, w jaki sposób udowodnisz ekstensywność, jak zdefiniowano powyżej?

Harper rozwiązuje te pytania na 10 stronach dla Systemu T, poprzez znaczną spryt i logiczne relacje. Pitts bierze więcej. Niektóre języki są jeszcze bardziej złożone.

Jak sobie z tym poradzić

Kusi mnie, by warunkowo przedstawić moje dowody oparte na domniemanej teorii równoważności PTS, ale rzeczywiste teorie wymagają nietrywialnych argumentów, więc nie jestem pewien, jak prawdopodobne byłoby takie przypuszczenie.

Jestem świadomy (choć nie szczegółowo) następujących prac:

Andrew Pitts (na przykład w ATTAPL dla rozszerzonego Systemu F oraz w kilku artykułach, takich jak 58-stronicowa „Operacyjna teoria równoważności programu”).
Praktyczne podstawy języków programowania (rozdziały 47–48), które są inspirowane Pittsem (ale twierdzi, że mają prostsze dowody).
Logiczne badanie równoważności programu . Nie mogę znaleźć angielskiego streszczenia, ale wydaje się, że poświęca dużo wysiłku na efekty uboczne (referencje), co wydaje się ortogonalną komplikacją.

pl.programming-languages type-theory operational-semantics Blaisorblade
źródło

⇓

$\Downarrow$

P ≅ Q

$P \cong Q$

C [\cdot]

$C[\cdot]$

C [P] ⇓

$C[P] \Downarrow$

C [Q] ⇓

$C[Q] \Downarrow$

@MartinBerger: to jest idea, o której wspominam, ale udowodnienie jej bezpośrednio jest zaskakująco trudne, ponieważ musisz zrobić dowody dla całego C (wyjaśnię to lepiej w pytaniu). Ponadto, jeśli wszystkie programy zakończą się, podana definicja określa wszystkie programy.

Blaisorblade,

β η

$\beta\eta$

C [P] ⇓ t r u e

$C[P] \Downarrow true$

C [Q] ⇓ t r u e

$C[Q] \Downarrow true$

≅

$\cong$ oraz (2) łatwe w obsłudze, np. pewne pojęcie podobieństwa lub relacji logicznej. Zależy od aplikacji.

Martin Berger,

@Blaisorblade Prawdopodobnie. Teoretycy współbieżności robili to intensywnie od dłuższego czasu, ponieważ przy równoległych procesach o wiele mniej jasne jest, jakiego pojęcia równoważności użyć. Doprowadziło to do podziału pracy: użyj semantyki opartej na redukcji z kwantyfikacją ponad kontekstami, aby zdefiniować pojęcie równoważności, a następnie użyj bisimulacji lub śladów nad oznakowanymi przejściami, aby udowodnić równoważność (lub jej brak). Wielkim otwartym pytaniem badawczym w teorii współbieżności jest sposób przejścia od pierwszego do drugiego algorytmicznie.

Martin Berger,

Odpowiedzi:

$[\![ {-} ]\!]$

[[t_{1}]] = [[t_{2}]] ⟹ t_{1} ≅ t_{2} .

$[\![ t_1 ]\!] = [\![ t_2 ]\!] \implies t_1 \cong t_2.$

Andrej Bauer
źródło

≅

$\cong$

Dzięki za odpowiedź, ale -1: choć się zgadzam, pytanie wymienia systemy czystego typu - AFAICS, semantyka denotacyjna dla systemów czystego typu jest otwartym problemem, więc myślę, że odpowiedź powinna wskazywać na pewną semantykę denotacyjną. (W rzeczywistości, gdybym miał semantykę denotacyjną, zrezygnowałbym całkowicie z operacyjnej, jak wspomniano w pytaniu). (Ale przepraszam za zbyt długie pytanie.)

Blaisorblade

@MartinBerger, nie rozumiem twojej krytyki. OP prosi o metody wykazania równoważności obserwacyjnej, wspominam o wspólnej, a następnie kwestionujesz, że istnieją inne sposoby, które unikają tej metody?

Andrej Bauer,

@ Blaisorblade, więc musisz wymyślić denotacyjną semantykę dla systemów czystego typu, prawda? :-) Ale poważniej, zapytam Alexa Simpsona, on wiedziałby lepiej o semantyce denotacyjnej dla takich rzeczy.

Andrej Bauer,

@AndrejBauer To nie była krytyka, a raczej dodatek.

Martin Berger,

$\eta$

cody
źródło

Nie sądzę, że doktor Streichera dotyczy PTS. Chodzi o semantykę Rachunku Konstrukcji i wyniki niezależności poprzez semantykę niezawodności. Zobacz tutaj .

Martin Berger,

Dziękuję za wyjaśnienie! Obawiam się, że link jest zepsuty (i trudny do naprawienia za pomocą zminimalizowanego linku).

cody

Link był do spisu treści książki tutaj . Mam nadzieję, że ten działa lepiej.

Martin Berger,

λ^{*}

$\lambda^*$

@MartinBerger: masz na myśli semantykę wykonalności?

Dominique Devriese,

Ta odpowiedź sugeruje podejście do problemu. (Informacje zwrotne są mile widziane).

Rozdział 49 PFPL omawia jednocześnie równoważne pojęcia równoważności obserwacyjnej i równoważności logicznej. Logiczna równoważność to ta sama relacja, którą zastosowano do określenia parametryczności, więc rdzeń tego rozdziału jest dowodem parametryczności dla Systemu F.

Praca nad parametrami dla PTS, AFAICT, nie omawia związku z równoważnością obserwacyjną. W rzeczywistości, aby nawet zdefiniować równoważność obserwacyjną, chyba że masz nieterminację, potrzebujesz jakiegoś pozytywnego rodzaju gruntu (naturals, booleans) do wykorzystania do obserwacji.

Jednak kluczowe twierdzenie (PFPL 47.6, 48.3, 49.2) odnoszące się do tych dwóch relacji zostało udowodnione niezależnie od konkretnego języka:

Równoważność obserwacyjna to najgrubsza spójna zgodność wyrażeń.

Następnie, aby pokazać, że równoważność logiczna implikuje równoważność obserwacyjną, wystarczy wykazać, że równoważność logiczna jest spójną spójnością. Jednak drugi kierunek wymaga nieco więcej pracy: w szczególności, aby wykazać, że logiczna równoważność jest zbieżnością, postępuje się przez indukcję kontekstów.

n + 1 = 1 + nVecN nnVecNVecN $n + 1 = 1 + n$ Vec (n + 1)Vec (1 + n)n + 11 + n

Blaisorblade
źródło