Semantyka i ewaluacja

Sposób przekazywania argumentów, w którym argument przekazywany jest niewyliczony i obliczany dopiero przy każdym użyciu w ciele funkcji.

Sposób przekazywania argumentów łączący wołanie przez nazwę z zapamiętywaniem: argument liczony co najwyżej raz, przy pierwszym użyciu.

Sposób przekazywania argumentów, w którym najpierw oblicza się argument, a jego wartość przekazuje do funkcji.

Wyrażenie, do którego nie można już zastosować żadnej reguły redukcji; reprezentuje w pełni obliczony wynik.

Podstawowa reguła obliczeniowa rachunku lambda: aplikacja abstrakcji do argumentu zastępuje go w ciele za związaną zmienną.

Sposób opisu znaczenia programów przez asercje logiczne o stanach przed i po wykonaniu, zwykle za pomocą trójek Hoare'a.

Sposób nadawania znaczenia programom przez odwzorowanie konstrukcji składniowych na obiekty matematyczne (denotacje) w dziedzinach semantycznych.

Wariant semantyki operacyjnej wiążący wyrażenie bezpośrednio z jego końcową wartością bez opisu pośrednich kroków.

Wariant semantyki operacyjnej opisujący wykonanie jako pojedyncze, atomowe przejścia redukcyjne między konfiguracjami.

Sposób definiowania znaczenia programu przez opis kroków wykonania na abstrakcyjnej maszynie lub przez reguły przejść między stanami.

Relacja uznająca dwa wyrażenia za równoważne, gdy są nieodróżnialne w każdym kontekście programu pod względem obserwowalnego zachowania.

Najogólniejszy warunek na stan początkowy gwarantujący, że po wykonaniu programu spełniony będzie zadany warunek końcowy.

Asercja 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.

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

Własność systemu redukcji, w którym różne ścieżki obliczeń z jednego wyrażenia zawsze prowadzą do wspólnego potomka.

Własność systemu, w którym każda sekwencja redukcji dowolnego wyrażenia jest skończona i kończy się postacią normalną.