SW wykład 9 - Slajd15

<<powrót do strony wykładu

Dziedziny podstawowe Suma i produkt Suma spłaszczona i produkt spłaszczony Przestrzeń funkcji ciągłych Izomorfizm dziedzin Konstruowanie funkcji ciągłych Złożenie funkcji i indeksowanie Inne konstrukcje Operator punktu stałego Równania stałopunktowe Równania dziedzinowe Rekurencyjne równania dziedzinowe Rekurencyjne równania dziedzinowe Problemy Dziedziny refleksywne Rozwiązanie naiwne dziedziny Scotta

Z sytuacji naszkicowanej na poprzednim slajdzie wyabstrahować można problem zdefiniowania dziedziny (zbioru łańcuchowo zupełnego) izomorficznego ze zbiorem funkcji z tego zbioru w tenże zbiór. Łatwo się przekonać, że taki nietrywialny zbiór nie istnieje (łatwy argument o mocach zbiorów prowadzi do wniosku, że musiałby to być zbiór jednoelementowy). Co więcej, nawet ograniczając rozważania do funkcji ciągłych, przedstawionej wyżej techniki kolejnych iteracji nie da się tu zastosować w oczywisty sposób.

Nic dziwnego --- problem zdefiniowania dziedziny, spełniającej powyższe równanie (dziedziny takie zwane są dziedzinami refleksywnymi) to jeden z najciekawszych i najtrudniejszych problemów semantyki języków programowania. Dziedziny takie są potrzebne do opisu konstrukcji językowych dozwalających na jakąś formę "samoaplikacji" --- a więc wprowadzających funkcje, które mogą być aplikowane do argumentów zawierających je same. Mechanizmy takie, jak beztypowe parametry procedur, które mogą być procedurami, czy pełne wiązanie dynamiczne, wymagają dziedzin semantycznych takiej lub podobnej postaci.

Znów, abstrahując od konkretnych mechanizmów językowych, dziedziny refleksywne stanowią podstawę dla definiowania semantycznych modeli dla beztypowego rachunku lambda (gdzie każdy element jest funkcją, którą można aplikować do dowolnego elementu modelu, w tym do samej tej funkcji).

Problem zbudowania semantycznego modelu dla beztypowego rachunku lambda, czy definicji nietrywialnej dziedziny refleksywnej, pozostawał otwarty do przełomu lat 60. i 70., kiedy Dana Scott podał pierwszą konstrukcję takiej dziedziny. Konstrukcja ta zresztą była oparta o ideę budowania kolejnych aproksymacji dziedziny refleksywnej przez iterowanie konstrukcji dziedziny funkcji ciągłych --- nietrywialnym jej elementem było jednak pokazanie, jak i w jakim sensie kolejne iteracje są zawarte w następnych, i jak skonstruować ich odpowiednią, nieskończoną sumę.