Nr 01 · Słownik · Teoria informatyki · Języki i teoria typów

Semantyka i ewaluacja

16 pojęć w 7 podgrupach, z prostymi definicjami i źródłami.

Przekazywanie argumentow · 3

  • 01wołanie przez nazwęcall-by-nameSposób przekazywania argumentów, w którym argument przekazywany jest niewyliczony i obliczany dopiero przy każdym użyciu w ciele funkcji.
  • 02wołanie przez potrzebęcall-by-needSposób przekazywania argumentów łączący wołanie przez nazwę z zapamiętywaniem: argument liczony co najwyżej raz, przy pierwszym użyciu.
  • 03wołanie przez wartośćcall-by-valueSposób przekazywania argumentów, w którym najpierw oblicza się argument, a jego wartość przekazuje do funkcji.

Redukcja lambda · 2

  • 01postać normalnaWyrażenie, do którego nie można już zastosować żadnej reguły redukcji; reprezentuje w pełni obliczony wynik.
  • 02redukcja betaβ-redukcjaPodstawowa reguła obliczeniowa rachunku lambda: aplikacja abstrakcji do argumentu zastępuje go w ciele za związaną zmienną.

Rodzaje semantyki · 5

  • 01semantyka aksjomatycznaSposób opisu znaczenia programów przez asercje logiczne o stanach przed i po wykonaniu, zwykle za pomocą trójek Hoare'a.
  • 02semantyka denotacyjnaSposób nadawania znaczenia programom przez odwzorowanie konstrukcji składniowych na obiekty matematyczne (denotacje) w dziedzinach semantycznych.
  • 03semantyka dużych krokówsemantyka naturalnaWariant semantyki operacyjnej wiążący wyrażenie bezpośrednio z jego końcową wartością bez opisu pośrednich kroków.
  • 04semantyka małych krokówsemantyka strukturalna (SOS)Wariant semantyki operacyjnej opisujący wykonanie jako pojedyncze, atomowe przejścia redukcyjne między konfiguracjami.
  • 05semantyka operacyjnaSposób definiowania znaczenia programu przez opis kroków wykonania na abstrakcyjnej maszynie lub przez reguły przejść między stanami.

Rownowaznosc programow · 1

  • 01ekwiwalencja obserwacyjnarównoważność kontekstowaRelacja uznająca dwa wyrażenia za równoważne, gdy są nieodróżnialne w każdym kontekście programu pod względem obserwowalnego zachowania.

Semantyka aksjomatyczna · 2

  • 01najsłabszy warunek wstępnywpNajogólniejszy warunek na stan początkowy gwarantujący, że po wykonaniu programu spełniony będzie zadany warunek końcowy.
  • 02trójka Hoare'aAsercja postaci {P}C{Q} stwierdzająca, że jeśli warunek wstępny P zachodzi przed wykonaniem programu C, to po nim zachodzi warunek końcowy Q.

Strategie ewaluacji · 1

  • 01kontekst ewaluacjiWyrażenie z wyróżnioną dziurą wskazującą miejsce, w którym może zajść następny krok redukcji, ujmujące strategię obliczania.

Wlasnosci redukcji · 2

  • 01konfluencjawłasność Churcha-RosseraWłasność systemu redukcji, w którym różne ścieżki obliczeń z jednego wyrażenia zawsze prowadzą do wspólnego potomka.
  • 02silna normalizacjaWłasność systemu, w którym każda sekwencja redukcji dowolnego wyrażenia jest skończona i kończy się postacią normalną.

Pozostałe grupy — Języki i teoria typów

Grupa pojęć · Języki i teoria typów16 haseł