Dlaczego najmniej ważny punkt (LFP) jest ważny w analizie programu?

Próbuję uzyskać ogólny obraz znaczenia najmniej ustalonego punktu (LFP) w analizie programu. Na przykład abstrakcyjna interpretacja wydaje się wykorzystywać istnienie LFP. Wiele prac badawczych na temat analizy programów również koncentruje się w dużej mierze na znalezieniu najmniej ustalonego punktu.

Mówiąc dokładniej, ten artykuł w wikipedii: Twierdzenie Knaster-Tarski wspomina, że ​​LFP są używane do definiowania semantyki programu.

Dlaczego to jest ważne? Każdy prosty przykład pomaga mi. (Próbuję uzyskać duży obraz).

EDYTOWAĆ

Myślę, że moje sformułowanie jest niepoprawne. Nie kwestionuję znaczenia LFP. Moje dokładne pytanie (początkujący) brzmi: w jaki sposób informatyka pomaga w analizie programu? Na przykład, dlaczego / jak abstrakcyjna interpretacja używa LFP? co się stanie, jeśli nie ma LFP w domenie abstrakcyjnej?

Mam nadzieję, że moje pytanie jest teraz bardziej konkretne.

Każda forma rekurencji lub iteracji w programowaniu jest w rzeczywistości stałym punktem. Na przykład whilepętla charakteryzuje się równaniem

while b do c done  ≡  if b then (c ; while b do c done)

co oznacza, że while b do c donejest to rozwiązanie Wrównania

W  ≡  Φ(W)

gdzie Φ(x) ≡ if b then (c ; x). Ale co, jeśli Φma wiele stałych punktów? Który odpowiada whilepętli? Jednym z podstawowych wniosków dotyczących semantyki programowania jest to, że jest to najmniej ustalony punkt.

Weźmy prosty przykład, tym razem rekurencyjny. Użyję Haskell. Funkcja rekurencyjna fzdefiniowana przez

f :: a -> a
f x = f x

jest wszędzie niezdefiniowaną funkcją, ponieważ działa po prostu na zawsze. Możemy przepisać tę definicję w bardziej nietypowy sposób (ale nadal działa w Haskell) as

f :: a -> a
f = f

Więc fjest stałym punktem funkcji tożsamości:

f ≡ id f

Ale każda funkcja jest stałym punktem id. Zgodnie ze zwykłym uporządkowaniem teoretycznym domenowym „niezdefiniowany” jest najmniejszym elementem. I rzeczywiście, nasza funkcja fjest wszędzie niezdefiniowaną funkcją.

Dodano na żądanie: w komentarzach OP zapytał o częściową kolejność dla whilepętli semantyki (zakładałeś, że to była sieć, ale nie musi). Bardziej ogólne pytanie brzmi: jaka jest teoretyczna interpretacja języka proceduralnego, który może manipulować zmiennymi i ma podstawowe struktury kontrolne (warunkowe i pętle). Można to zrobić na kilka sposobów, w zależności od tego, co dokładnie chcesz uchwycić, ale dla uproszczenia załóżmy, że mamy stałą liczbę zmiennych globalnych$n$$x_1, \ldots, x_n$że program może czytać i aktualizować oraz nic więcej (żadnych operacji we / wy lub wyjątków lub przydzielania nowych zmiennych). W takim przypadku program może być postrzegany jako transformacja stanu początkowego zmiennych do stanu końcowego lub wartość nieokreślona, ​​jeśli program się zmienia. Tak więc, jeśli każda zmienna zawiera element zestawu , program będzie odpowiadał odwzorowaniu : dla każdej początkowej konfiguracji zmiennych program albo się rozejdzie i wyda , albo zakończy i wytworzy stan końcowy, który jest elementem . Zestaw wszystkich map to domena:$V$$V^n \to V^n \cup \{\bot\}$$(v_1, \ldots, v_n) \in V^n$$\bot$$V^n$$V^n \to V^n \cup \{\bot\}$

• używamy płaskiego porządku na który ma na dole i wszystkie elementy „płaskiego” nad nim, a następnie jest uporządkowany punktowo,$V^n \cup \{\bot\}$$\bot$$V^n$$V^n \to V^n \cup \{\bot\}$
• najmniejszym elementem jest funkcja, która zawsze mapuje na , odpowiadający programowi (i wielu innym),$\bot$while true do skip done
• każda rosnąca sekwencja ma supremum

Aby dać ci wyobrażenie o tym, jak to działa, semantykę programu

x_1 := e

będzie funkcją, która przyjmuje jako dane wejściowe , oblicza wartość wyrażenia w stanie i zwraca .v e ( v 1 , … , v n ) ( v e , v 2 , … , v n$(v_1, \ldots, v_n) \in V^n$$v_e$e$(v_1, \ldots, v_n)$$(v_e, v_2, \ldots, v_n)$

Oto intuicja: najmniej ustalone punkty pomagają analizować pętle.

Analiza programu obejmuje wykonanie programu - ale wyodrębnienie niektórych szczegółów danych. To wszystko dobrze. Abstrakcja pomaga analizie przebiegać szybciej niż faktyczne uruchomienie programu, ponieważ pozwala zignorować aspekty, na których ci nie zależy. Na przykład tak działa interpretacja abstrakcyjna: w zasadzie symuluje wykonanie programu, ale śledzi tylko częściowe informacje o stanie programu.

Trudne jest, gdy dojdziesz do pętli. Pętla może być wykonywana wiele, wiele razy. Zazwyczaj nie chcesz, aby analiza programu musiała wykonywać wszystkie te iteracje pętli, ponieważ wtedy analiza programu zajmie dużo czasu ... a nawet może się nie skończyć. Więc tam używasz najmniej ustalonego punktu. Najmniej ustalony punkt zasadniczo charakteryzuje to, co można powiedzieć na pewno będzie prawdziwe po zakończeniu pętli, jeśli nie wiesz, ile razy pętla będzie się powtarzać.

Do tego służy najmniej ustalony punkt. Ponieważ w programach występują pętle, podczas analizy programu używane są najmniej ustalone punkty. Najmniej ustalonych punktów są ważne, ponieważ pętle są wszędzie i ważna jest możliwość analizowania pętli.

Nawiasem mówiąc, rekurencja i wzajemna rekurencja są po prostu kolejną formą pętli - więc one również mają tendencję do obsługi z najmniej ustalonym punktem.