Fizyk contra złośliwy programista

Widzę w buzzie długą, fachową dyskysję o sprawdzaniu poprawności programów. Niestety, nie jestem w stanie jej rozumieć. Mam za duże dziury erudycyjne w zakresie wiedzy o różnych programach, narzędziach, ... - nie jestem informatykiem. Temat jednak mnie ciekawi. Programy, nawet krótkie, potrafią być naprawdę trudne, mogą się opierać na bardzo nieoczywistych algorytmach, opierających się na wysoce nietrywialnych twierdzeniach. Czyż program sprawdzający poprawność programów, ale tak na pewniaka, nie musiałby mieć ogromnej wiedzy? Przerastającej wiedzę schowaną w programach?

Dla łatwego wprowadzenia tematu chcę zacząć od czegoś bardzo prostego, od zmyślonej sytuacji:

Pewien fizyk potrzebuje pliku z parami (punkt prosta), gdzie chodzi o pary incydentne, brane z płaszczyzny afinicznej rzędu 9 (ma 81 punktów), standardowej, nad ciałem GF(9). Zatrudnił więc fizyk programistę, żeby mu ten plik sprokurował. Poza tym od programisty wziął program, który programista napisał, żeby wygenerować żądaną płaszczyznę.

A teraz fizyk ma wątpliwości co do poprawności pliku i programu. Jak program sprawdzający poprawność pomoże fizykowi? Powiedzmy, że złośliwy programista poprawnie zaprogramował, ale niestandardową płaszczyznę. Odróżnić ją od standardowej jest bardzo trudno, ma szereg własności takich samych. Program sprawdzający poprawność mógłby nawet machnąć ręką (:-) na kod, i sprawdzić poprawność outputu. Porównać go z płaszczyzną standardową. Takie rzeczy robią CAD programy. Ogólnie taki problem, sprawdzający izomorfizm dwóch grafów, jest NP-complete (?), jest niewielomianowy. Więc gdyby chodziło o płaszczyzny wyższego rzędu, to CAD programy wysiadłyby, mimo że można takie płaszczyzny łatwo generować (dostać outputowy plik, przedstawiający graf punktowo-liniowy). Jeżeli programy CAD wysiadłyby, to jak sobie poradzi program sprawdzający poprawność? Musi jednak zajrzeć do kodu - powodzenia! Kod jest poprawny w pewnym sensie, ale produkuje płaszczyznę nieizomorficzną z żądaną. Dowód niepoprawności kodu wydaje mi się znacznie trudniejszym problemem niż dowód niepoprawności outputowego pliku; najprościej byłoby program puścić i analizować jednak output. Ba!

Oczywiście w przypadkach ogólnych sprawdzanie outputu jest niemożliwe, bo w zależności od inputu, output może być ogromny (a zastosowanie może korzystać tylko z małej części outputu, ale a priori z dowolnej, w zależności od losowych parametrów).

Może jednak zacznijmy od malutkiej 81-punktowej płaszczyzny nad ciałem GF(9).

Dwa podejścia do geometrii - logiczne i grupowe. Cz 0.

Uwagi wstępne

Dla skupienia uwagi, będę pisał o płaszczyźnie zespolonej  [;\mathbf C;],  ale przedstawione idee będą znacznie ogólniejsze.

Słowo grupowe w tytule tego postu odnosi się do teorii grup, która to teoria jest częścią algebry. Dla zrozumienia niniejszego postu nie ma większej potrzeby znajomości podstaw teorii grup (ale co Wam szkodzi zajrzeć tu i tam :-).

Tytuł mówi o dwóch podejściach do geometrii. W przypadku płaszczyzny okaże się (w Cz 1), że są one równoważne. Będzie tak ze względu na wielką jednorodność płaszczyzny. Prawdziwe, zdrowe, klasyczne geometrie kochają jednorodność.

Podejście "logiczne"

Odległością  [;d(v\ w);]  pomiędzy dwoma liczbami (punktami) zespolonymi  [;v\ w\in\mathbf C;]  nazywamy moduł ich różnicy

                [;d(v\ w)\ :=\ |w-v|;]

(jest to zwykła odległość euklidesowa). Odtąd możemy rozwijać geometrię metryczną płaszczyzny  [;\mathbf C;].  Przez twierdzenia tej teorii rozumie się twierdzenia, które wyrażają się wyłącznie w terminach odległości. Takim twierdzeniem jest na przykład nierówność trójkąta:

        [;d(u\ v)+d(v\ w)\ \ge\ d(u\ w);]

dla dowolnych liczb zespolonych  [;u\ v\ w\in\mathbf C;].

Twierdzenia takie nazywa się niezmienniczymi. Nie występują w nich ani współrzędne punktów (popularnie nazywane  [;x\ y;] - chodzi o część rzeczywistą i urojoną), ani nie występują w nich konkretne liczby zespolone ani operacje algebraiczne ciała liczb zespolonych, jak  [;\mathbf 0\ \mathbf 1\ +\ -\ \cdot;].  

UWAGA  Znak dodawania, który wystąpił w nierówności trójkąta, to było dodawanie odległości, a nie punktów (liczb zespolonych). Może tu dojść do pewnych subtelnośći (komplikacji), ale znowu nie chcę się rozpraszać.

Powyższe określenie twierdzeń geometrycznych geometrzy używają intuicyjnie z łatwością, ale jednak budzi ono lekki niepokój. Tylko lekki. Nie jest to jeszcze definicja ścisła. Żeby ją uściślić, trzeba by się sporo i cierpliwie potrudzić, co chętnie uczyniliby logicy. Powiedziliby dokładnie co to znaczy, że twierdzenie wyraża się jedynie w terminach odległości, czyli że jest niezmiennicze. Geometrzy nie za bardzo potrzebują uściślenia. Gdy rozwijają geometrię, to wiedzą, że geometrię, wiedzą to i bez uściślenia. Na dodatek, oprócz twierdzeń ściśle geometrycznych (niezmienniczych) istnieją, i są ważne, twierdzenia analityczno-geometryczne. Na przykład, algebraicznym środkiem liczb zespolonych (punktów)  [;v\ w\in\mathbf C;] nazywamy punkt

        [;s(v\ w)\ :=\ \frac{v+w}{2};]

Natomiast ich geometrycznym środkiem nazywamy punkt  [;S(v\ w);], który spełnia warunek:

        [;d(v\ S(v\ w)) = d(S(v\ w)\ w) = \frac{S(v\ w)}{2};]

Nawet a priori nie wiemy, czy taka geometryczna definicja jest poprawna - a co jeżeli więcej niż jeden punkt spełnia podany warunek geometryczny? A może czasem żaden? Otóż twierdzenie mówi, że środek algebraiczny i geometryczny pokrywają się:

        [;S(v\ w)\ =\ s(v\ w);]

dla dowolnych punktów  [;v\ w\in\mathbf C;]. W szczególnośći środek geometryczny dwóch punktów zawsze istnieje, i tylko jeden. Ponieważ środek algebraiczny nie jest pojęciem a priori geometrycznym (zawiera dodawanie liczb zespolonych oraz dzielenie przez 2), to twierdzenie o równości środków nie jest (czysto) geometryczne, lecz jest analityczno-geometryczne. Takie twierdzenia są ważne na przykład jako narzędzia, gdyż pozwalają geometrze korzystać z algebry, a ta ma tendencję do bycia prostą i klarowną. Na przykład, zgodnie z twierdzeniem o środku geometrycznym i algebraicznym, odtąd możemy w twierdzeniach geometrycznych (niezmienniczych) korzystać "legalnie" ze środka algebraicznego, czyli z czegoś istotnego geometrycznie, a przy tym łatwego analitycznie. Ułatwia to znacznie rozwijanie geometrii.

Dla kontrastu, pojęcie dodawania liczb zespolonych  [;v+w;]  nie jest geometryczne, nie da się wyrazić czysto za pomocą wyłącznie odległości punktów. Matematyka potrafi zadziwiać. Po podzieleniu sumy przez 2 otrzymujemy pojęcie geometryczne. A algebraicznie prostsze wyrażenie samej sumy geometrycznym jednak nie jest. W tej chwili trudno byłoby nam tego dowieść, kupa żmudnej roboty, a nawet chyba nie widać dobrze jak się do tego zabrać, że suma nie jest geometryczna.

W następnej części przedstawię podejście grupowe. Wtedy na takie pytania będzie można odpowiadać rutynowo, na ogół z łatwością. Ponieważ podejście grupowe będzie równoważne z logicznym, to trudne dla podejścia logicznego pytania staną się łatwe. Byle zainwestować jednorazowo w podstawowe twierdzenie o równoważności dwóch podejść.