SW wykład 2 - Slajd18: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 7: | Linia 7: | ||
wartości podwyrażeń. | wartości podwyrażeń. | ||
Sformułowana formalnie w ramce powyżej własność mówi z jednej strony, | Sformułowana formalnie (w ramce powyżej) własność mówi z jednej strony, | ||
że w każdym wyrażeniu możemy zastąpić dowolne jego podwyrażenie | że w każdym wyrażeniu możemy zastąpić dowolne jego podwyrażenie | ||
(dokładniej: pewną liczbę wystąpień tego podwyrażenia) nową zmienną, | (dokładniej: pewną liczbę wystąpień tego podwyrażenia) nową zmienną, | ||
| Linia 29: | Linia 29: | ||
strukturze wyrażeń arytmetycznych pozostawiamy Państwu. Przypadek | strukturze wyrażeń arytmetycznych pozostawiamy Państwu. Przypadek | ||
wyrażeń będących stałymi numerycznymi, jak zwykle, jest | wyrażeń będących stałymi numerycznymi, jak zwykle, jest | ||
trywialny. Przypadki wyrażeń będących sumą, iloczynem lub różnicą | trywialny. Przypadki wyrażeń będących sumą, iloczynem lub różnicą | ||
to też łatwe wykorzystanie założenia indukcyjnego i definicji | to też łatwe wykorzystanie założenia indukcyjnego i definicji | ||
podstawienia dla tych przypadków. Pewnej staranności --- ale niczego | podstawienia dla tych przypadków. Pewnej staranności --- ale niczego | ||
więcej --- wymaga przypadek wyrażeń będących zmiennymi. | więcej --- wymaga przypadek wyrażeń będących zmiennymi. | ||
Aktualna wersja na dzień 11:05, 27 wrz 2006
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
Kolejną własność wyrażeń określa się jako przejrzystość (przezroczystość) odwołań (do zmiennych w wyrażeniach). Nieformalnie, chodzi tu o możliwość dowolnego manipulowania stopniem wyliczenia wartości podwyrażeń.
Sformułowana formalnie (w ramce powyżej) własność mówi z jednej strony, że w każdym wyrażeniu możemy zastąpić dowolne jego podwyrażenie (dokładniej: pewną liczbę wystąpień tego podwyrażenia) nową zmienną, której przypiszemy w stanie wartość zastępowanego podwyrażenia. Z drugiej zaś strony: każdą zmienna w wyrażeniu możemy zastąpić podwyrażeniem, którego wartością jest wartość liczbowa przypisana danej zmiennej w stanie. (To pierwsze sformułowanie odpowiada czytaniu podanej równości z lewej strony ku prawej, a to drugie: z prawej ku lewej.)
Dla ścisłego sformułowania tego faktu wykorzystujemy pojęcie podstawienia wyrażenia arytmetycznego za zmienną w wyrażeniu arytmetycznym. Powyżej podajemy formalną definicję indukcyjną --- zupełnie chyba oczywistą i oczekiwaną. Zwróćmy tylko jeszcze uwagę, że zmienna, na którą podstawiamy, nie musi w danym wyrażeniu występować, a jeśli występuje, to może występować więcej niż raz. Warto też zauważyć, że podstawiane wyrażenie znów może zawierać tę zmienną (może to wręcz być to samo wyrażenie, w którym podstawiamy).
Prosty dowód własności w ramce przez indukcję strukturalną po strukturze wyrażeń arytmetycznych pozostawiamy Państwu. Przypadek wyrażeń będących stałymi numerycznymi, jak zwykle, jest trywialny. Przypadki wyrażeń będących sumą, iloczynem lub różnicą to też łatwe wykorzystanie założenia indukcyjnego i definicji podstawienia dla tych przypadków. Pewnej staranności --- ale niczego więcej --- wymaga przypadek wyrażeń będących zmiennymi.
