SW wykład 2 - Slajd10

Z Studia Informatyczne
Wersja z dnia 10:35, 27 wrz 2006 autorstwa Dorota (dyskusja | edycje)
(różn.) ← poprzednia wersja | przejdź do aktualnej wersji (różn.) | następna wersja → (różn.)
Przejdź do nawigacjiPrzejdź do wyszukiwania

<<powrót do strony wykładu

Składnia Składnia konkretna Składnia abstrakcyjna Przyjmowane założenia Przykład wiodący Kategorie składniowe Kategorie składniowe, c.d. Uwagi Indukcja strukturalna Definicje indukcyjne Kategorie semantyczne Wartościowanie zmiennych Semantyka wyrażeń Semantyka wyrażeń logicznych Semantyka instrukcji Prosty fakt Dowód Przezroczystość odwołań Semantyka operacyjna Obliczenia Semantyka operacyjna Tiny Własności Własności, c.d. Warianty definicji

Powyższy przykład definicji indukcyjnej określa zbiór zmiennych wolnych każdego wyrażenia arytmetycznego (wobec braku wiązania zmiennych czy deklarowania zmiennych lokalnych w wyrażeniach, na przykład przez kwantyfikatory, jest to po prostu zbiór zmiennych, które w tym wyrażeniu występują).

Na przykład, łatwo teraz pokazać, że zbiór zmiennych wolnych każdego wyrażenia arytmetycznego jest skończony. Własność ta zachodzi bowiem wprost z definicji dla wyrażeń, będących stałymi numerycznymi lub zmiennymi, oraz jeśli zachodzi ona dla dwóch wyrażeń arytmetycznych, to zachodzi też dla wyrażeń będących ich sumą, iloczynem lub różnicą. Zatem, na mocy zasady indukcji strukturalnej, własność ta zachodzi dla wszystkich wyrażeń arytmetycznych.