SW wykład 4 - Slajd7

<<powrót do strony wykładu

Semantyka denotacyjna Dziedziny składniowe i semantyczne Funkcje semantyczne Kompozycjonalność Tiny. Semantyka denotacyjna Tiny. Semantyka denotacyjna, c.d. Pojęcia pomocnicze Pojęcia pomocnicze, c.d. |Tiny. Semantyka denotacyjna, c.d. Tiny. Semantyka denotacyjna, c.d. Problem z while Konstrukcje stałopunktowe Konstrukcje stałopunktowe, c.d. Konstrukcje stałopunktowe, c.d. Przykład Przykład, c.d. Dowód Dowód Zgodność semantyki denotacyjnej

Zanim podamy klauzule semantyczne definiujące wprowadzone na poprzednim slajdzie funkcje semantyczne, kilka słów o wykorzystywanej w nich notacji.

Po pierwsze, intensywnie będziemy tu wykorzystywać notację lambda: nie formalny rachunek lambda, ale po prostu notację wykorzystywaną standardowo do definiowania funkcji o wartościach określonych wyrażeniem dla dowolnej wartości parametru formalnego, branych z określonej dziedziny semantycznej.

Dalej, wprowadzamy standardowe oznaczenie dla funkcji identycznościowej na danej dziedzinie.

Złożenie funkcji będzie w tych materiałach oznaczane średnikiem i zapisywane w "kolejności wyliczania": od lewej do prawej.

Wykorzystywać też będziemy funkcję warunkową, wybierającą jako wynik swój drugi lub trzeci argument w zależności od wartości (logicznej) pierwszego argumentu.

Wszystkie takie funkcje, definiowane formalnie dla poszczególnych dziedzin określających ich zbiory argumentów lub wyników i oznaczane odpowiednio "udekorowanymi" symbolami, często zapisywać będziemy pomijając te wskazujące na konkretną dziedzinę dekoracje, oczekując, że łatwo je będzie odtworzyć z kontekstu.