Punkt stały, co to znaczy w świecie informatyki

Ciągle natrafiam na odniesienia do stałego punktu w pytaniach i odpowiedziach na stackexchange i szukam znaczenia w Internecie, oczywiście znajdując odnośniki na stronach takich jak Wikipedia. Jednak żadne z odniesień tak naprawdę nie odpowiada na moje pytanie, co jest stałym punktem i co to znaczy w świecie informatyki.

W informatyce najbardziej widocznym zastosowaniem punktów stałych jest teoria sieci ¹. Sieć to częściowo uporządkowany zbiór z dodatkową właściwością, która dała dowolne dwa elementy x , y ∈ S , zbiór { x , y } ma zarówno supremum, jak i infimum (w S ).$(S, \leq)$$x,y \in S$$\{x,y\}$$S$

Teraz często rozważasz funkcje monotoniczne na tej sieci, które „zbiegają się”, to znaczy dla niektórych x ∈ S masz f ( x ) = x . Ważnymi wynikami w tej dziedzinie są twierdzenie Kleene'a o stałym punkcie oraz twierdzenie Knastera-Tarskiego .$f$$x \in S$$f(x)=x$

Znakomity przykład jest krata dla A, część zestawu i f indukowane przez określenie indukcyjnego. Na przykład, pozwólmy A = { a , b } ∗, a my zdefiniujemy język L ∈ 2 { a , b } ∗ przez$(2^A,\subseteq)$$A$$f$$A = \{a,b\}^*$$L \in 2^{\{a,b\}^*}$

$\qquad \begin{align} \phantom{w \in L} &\phantom{\implies} \varepsilon, a \in L \\ aw \in L &\implies baw \in L \\ bw \in L &\implies abw, bbw \in L \end{align}$

Ta definicja indukcyjna odpowiada funkcji monotonicznej

$\qquad \displaystyle f(A) = \{\varepsilon, a\} \cup A \cup \{baw \mid aw \in L\} \cup \{abw, bbw \mid bw \in L\}$

Przez Knaster-Tarskiego twierdzenia wiemy, ma najmniejszą fixpoint który jest Supremum wszystkich mniejszych „wyniki pośrednie” (co odpowiada skończenie często stosowania konstruktory definicji indukcyjne), a najmniejszą fixpoint jest rzeczywiście l .$f$$L$

Nawiasem mówiąc, największy punkt stały ma również zastosowania; patrz tutaj na przykład.

W teorii rekurencji istnieje inne twierdzenie o punkcie stałym, również z powodu Kleene'a. To mówi ²,

Niech się numerację Godeł ³ i R : N → N TOTAL, funkcja obliczeniowy (intuicji kompilator). Potem jest i ∈ N takie, że φ r ( i ) = φ i .$\varphi$$r :\mathbb{N} \to \mathbb{N}$$i \in \mathbb{N}$$\varphi_{r(i)}=\varphi_i$

W rzeczywistości istnieje nawet nieskończenie wiele takich ; gdyby tam było tylko skończonych wielu, moglibyśmy załatać r (przez przeglądanie tabeli), aby nie mieć stałych punktów, co jest sprzeczne z twierdzeniem.$i$$r$

1. Każdy używa go codziennie, nawet jeśli nie zdajesz sobie z tego sprawy.
2. Nie podoba mi się ten artykuł z Wikipedii; prawdopodobnie lepiej jest sprawdzić książkę gatunku.
3. Specjalny rodzaj numeracji funkcji. Dla intuicji pomyśl o tym jako o języku programowania (kompletnym Turinga).

Pozwól mi rozwinąć nieco odpowiedź Meisterluka: Wyobraź sobie, że próbujemy zdefiniować funkcję silniową: pamiętaj definicję funkcji silniowej:

fact 0     = 1
fact (n+1) = n*(fact n)

Teraz w niektórych frameworkach PL (a mianowicie calculus$\lambda$ ) nie jest od razu oczywiste, jak zdefiniować taką funkcję. Jednak może być łatwo zdefiniować następującą funkcję wyższego rzędu , tak zwaną, ponieważ przyjmuje ona jako wejście inną funkcję i liczbę naturalną

Fact f 0     = 1
Fact f (n+1) = n * (f n)

W tej definicji funkcji nie ma zastosowania rekurencji. Jednakże, jeśli istnieje jakiś sposób znalezienia FIX-punkt z Fact, czyli funkcja takie, że Fakt φ n = φ n dla każdego n , to łatwo sprawdzić, że φ jest rzeczywiście realizacja funkcji silni.$\phi$

Teraz w ramach, takich jak calculus, można pokazać, że faktycznie istnieją wszystkie stałe punkty tego rodzaju, co wyjaśnia, że ​​można go używać jako ogólnego języka programowania.$\lambda$

Pojęcie punktów stałych w informatyce ma wiele innych zastosowań, ale większość sprowadza się do tego, który pokazałem powyżej, tj. Udowadnia, że ​​istnieją pewne punkty stałe, aby móc wykazać, że pewne funkcje lub konstrukcje są dobrze zdefiniowane w twój framework (tutaj pokazaliśmy, że funkcja silnia istnieje).

$f: A \to A$$x$$f(x)$$x$$x^2$$0$$1$$x^3$

Teraz, w zależności od struktury matematycznej, z którą mamy do czynienia, istnieje bardzo wiele różnych powodów, aby interesować się stałymi punktami. Na przykład, jeśli weźmiesz pod uwagę dynamiczny system, który patrzy na stan świata i zmienia go (jak termostat), wówczas punkt stały odpowiada stabilnej konfiguracji. Jeśli myślisz o grach w matematycznym sensie teorii gier, punkty stałe odpowiadają równowagom, jeśli myślisz o zachowaniu procedury optymalizacji, która iteracyjnie poprawia swoje rozwiązanie, punkt stały odpowiada rozwiązaniu optymalnemu. Tak więc matematyczne pojęcie punktu stałego ma wiele zastosowań w wielu różnych kontekstach.

Bardzo powszechnym i podstawowym zastosowaniem stałych punktów w informatyce jest matematyczne modelowanie pętli i programów rekurencyjnych. Jeśli spróbujemy modelować program jako funkcję matematyczną, zarówno pętle, jak i rekurencja nie są oczywiste do modelowania. Wynika to z faktu, że ciało pętli jest programem i może być reprezentowane jako funkcja matematyczna. Jak uzyskać funkcję reprezentującą zachowanie pętli? Odpowiada to wielokrotnemu nakładaniu korpusu pętli, w połączeniu z osłoną pętli, aż dalsza zmiana nie jest możliwa. Podobnie, jeśli modelujemy programy rekurencyjne matematycznie, potrzebujemy matematycznego pojęcia, co to znaczy, że funkcja może się zastosować. Odpowiedzi udzielają stałe punkty.

Funkcja w matematyce jest mapą między wartościami wejściowymi i wyjściowymi. Punkty stałe to wartości wejściowe (dla funkcji), które odwzorowują na wartości wyjściowe odpowiadające równości z danymi wejściowymi.

$f(x) = x$$f(x) = x^2$$\{0, 1\}$

Jeśli chodzi o informatykę, dużo mówimy o funkcjach cząstkowych , ale nie zmienia to dla nas definicji punktów stałych.

Być może mylisz się co do zupełnie innego tematu: arytmetyka stałoprzecinkowa to koncepcja reprezentowania liczb rzeczywistych w pamięci. Ale nazwa „punkty stałe” nie odnosi się ogólnie do tego tematu (ponieważ jest tylko 1 punkt).

teoria gier jest głównym podobszarem CS, a ważną koncepcją jest równowaga Nasha, która jest twierdzeniem o punkcie stałym. daje to możliwość zidentyfikowania optymalnych strategii gry, biorąc pod uwagę, że inni gracze znają się nawzajem. można to udowodnić za pomocą twierdzenia o punkcie stałym Kakutani lub twierdzenia o punkcie stałym Browera . Nash zdobył Nagrodę Nobla w dziedzinie ekonomii częściowo za rozwinięcie tej teorii.