Niestety dzieje się tu zbyt wiele rzeczy. Łatwo jest więc pomieszać. Użycie „pełnego” w „pełnej kompletności” i „pełnej abstrakcji” odnosi się do zupełnie różnych idei pełni. Ale istnieje również niejasny związek między nimi. To będzie skomplikowana odpowiedź.
Pełna kompletność : „Dźwięk i kompletność” to właściwość, którą tradycyjna logika ma mieć pod względem semantyki. Zdrowość oznacza, że wszystko, co można udowodnić w logice, jest prawdziwe w modelu semantycznym. Kompletność oznacza, że wszystko, co jest prawdziwe w modelu semantycznym, można udowodnić w logice. Mówimy, że logika jest solidna i kompletna dla konkretnego modelu semantycznego. Kiedy dochodzimy do logiki konstruktywnej, takich jak teoria typu Martina-Lofa lub logika liniowa, dbamy nie tylko o to, czy formuły są możliwe do udowodnienia, ale także o to, jakie są ich dowody. Sprawdzalna formuła może mieć wiele dowodów, a konstruktywna logika chce je rozdzielić. Tak więc semantyka logiki konstruktywnej polega nie tylko na określeniu, czy formuła jest prawdziwa, ale także na abstrakcyjnym semantycznym pojęciu „dowodu” („dowodu”) na jej prawdziwość. Abramsky i współpracownicy wymyślili termin „pełna kompletność”, co oznacza, że dowody w logice mogą wyrażać wszystkie dowody semantyczne w modelu. „Pełny” odnosi się tutaj do dowodów. „Kompletna” logika może udowodnić wszystko, czego potrzebuje. „W pełni kompletna” logika zawiera wszystkie dowody, które musi posiadać. Zatem „pełna kompletność” oznacza „konstruktywną kompletność” lub „kompletność dowodową”. Nie ma to nic wspólnego z pełną abstrakcją.
Pełna abstrakcja : „Adekwatna i w pełni abstrakcyjna” to właściwość, której potrzebujesz dla semantycznego modelu języka programowania. (Zauważ pierwszą różnicę: mamy teraz do czynienia z właściwościami modelu semantycznego, a nie właściwości języka!) Adekwatność oznacza, że ilekroć dwa terminy mają to samo znaczenie w modelu semantycznym, są obserwacyjnie równoważne w języku programowania (w odniesieniu do niektórych pojęć wykonania). Pełna abstrakcja oznacza, że jeśli dwa terminy są równoważne obserwacyjnie, mają takie samo znaczenie w modelu semantycznym. Te pomysły mogą być związane z solidnością i kompletnością, ale w nieco wymyślny sposób. Jeśli myślimy o semantycznym modelu języka programowania jako o „logice” lub „metodzie dowodowej”, aby mówić o równoważności obserwacyjnej, to adekwatność oznacza, że ta metoda dowodowa jest solidna; pełna abstrakcja oznacza, że ta metoda dowodowa jest kompletna. Nie ma pojęcia „pełnej kompletności”metoda dowodowa. (Ale coś takiego jest teoretycznie możliwe i pewnego dnia ktoś może to zrobić.)
W twoim przypadku interesują Cię tłumaczenia, a nie modele semantyczne. Właściwości adekwatności i pełnej abstrakcji można rozszerzyć w celu obsługi tłumaczeń w następujący sposób. Myślisz o języku docelowym jako o „modelu semantycznym”, tj. O formalizmie, który w pełni rozumiesz. Jeśli tak, masz jakieś pojęcie o równoważności. Następnie mówimy, że tłumaczenie jest odpowiednie, jeśli ilekroć tłumaczenia dwóch programów źródłowych są równoważne w języku docelowym, są one obserwacyjnie równoważne w języku źródłowym. Mówimy, że jest w pełni abstrakcyjny, jeśli ilekroć dwa programy źródłowe są obserwacyjnie równoważne w języku źródłowym, ich tłumaczenia są równoważne w języku docelowym.
W rzeczywistości nie znam żadnych języków docelowych, które naprawdę w pełni „rozumiemy”. Wszystko, co wiemy, to inne pojęcie równoważności obserwacyjnej dla języka docelowego. W takim przypadku tłumaczenie jest odpowiednie, jeżeli obserwacyjna równoważność tłumaczeń w języku docelowym implikuje równoważność obserwacyjną w języku źródłowym.
Tłumaczenie jest w pełni abstrakcyjne, jeżeli obserwacyjna równoważność terminów w języku źródłowym implikuje obserwacyjną równoważność tłumaczeń w języku docelowym.
M ≅ N ⟹ τ ( M )
τ( M) ≅τ( N) ⟹ M≅N.
Niektórzy autorzy uważają „tłumaczenie w pełni abstrakcyjne” za kombinację tych dwóch właściwości:
M ≅ NM.≅N.⟹ τ( M) ≅τ( N)
M.≅N.⟺τ( M) ≅τ( N)
ZAZA
∀ N.: τ( A ) .∃ M.: .τ( M) = N
Teraz niejasny związek między pełną kompletnością a pełną abstrakcją. Udowodnienie, że model semantyczny lub tłumaczenie jest w pełni abstrakcyjne, często wymaga pewnej definiowalności. Jest tak, ponieważ nasze języki są na ogół wyższego rzędu. Tak więc, jeśli model semantyczny lub język docelowy ma zbyt wiele „kontekstów”, będzie w stanie wbić nasze terminy lub znaczenia semantyczne w niepożądany sposób i zepsuć ich równoważność. „Niepożądane sposoby” oznaczają sposoby, w które sam język programowania nie może ich dotknąć. Tak więc, aby uzyskać pełną abstrakcję, musimy upewnić się, że „konteksty” dostępne w modelu semantycznym lub języku docelowym pochodzą od tych w języku źródłowym w jakiejś formie. Należy pamiętać, że dotyczy to właściwości pełnej kompletności.
Dlaczego chcemy takich właściwości? Nie ma niczrobić z kompilatorami! Chcemy tych właściwości, aby twierdzić, że język źródłowy jest osadzony w języku docelowym. Jeśli jesteśmy zadowoleni z określonego języka docelowego (jako czystego, zrozumiałego, w jakiś sposób podstawowego lub podanego przez Boga), to jeśli język źródłowy jest w niego osadzony, możemy twierdzić, że nie ma nic nowego w języku źródłowym. To tylko fragment języka docelowego, który znamy i kochamy. To tylko cukier syntaktyczny. Tak więc ludzie w pełni abstrakcyjni tłumaczą, aby ustalić, że poszczególne języki docelowe są świetne. Czasami są one również podawane przez ludzi, którzy mają do czynienia z dużym lub skomplikowanym językiem. Zamiast więc bezpośrednio definiować semantykę, tłumaczą go na jakiś język podstawowy, a następnie podają semantykę na język podstawowy. Na przykład robi to raport Haskell. Jednak pełna abstrakcja tych tłumaczeń rzadko jest udowodniona, ponieważ języki źródłowe są duże i skomplikowane. Ludzie wierzą, że tłumaczenie jest dobre.
Po raz kolejny nie ma to nic wspólnego z kompilatorami. Kompilatory rzadko są adekwatne lub w pełni abstrakcyjne. I nie muszą tak być! Kompilator musi jedynie zachować zachowanie wykonawcze kompletnych programów. Język docelowy kompilatora jest na ogół ogromny, co oznacza, że ma wiele kontekstów, które mogą zepsuć równoważność. Zatem równoważne programy w języku źródłowym prawie nigdy nie są równoważne kontekstowo po skompilowaniu.