Polskie Towarzystwo Informatyczne
NUMER ARCHIWALNY:     9-10 / 27-28 rok III | wrzesień–październik 1984
Archiwum
Menu chronologiczne Menu tematyczne


Polskie Towarzystwo Informatyczne

O języku informatycznej formalizacji matematyki
 
                Będzie tutaj mowa o pracach jednej z sekcji PTI, noszącej miano sekcji języków informacyjno–logicznych; warto jednak tę lokalną działalność ukazać w kontekście bardziej uniwersalnym (i teoretycznym, i historycznym), w którym owa działalność przebiega.
                W paru miejscach na świecie ludzie próbują realizować pomysł systemu, który umożliwiłby formułowanie tekstów matematycznych w sposób tak precyzyjny; tak znormalizowany i tak dostosowany do współdziałania z komputerem, żeby korzystając z czysto formalnych operacji na tekście, wykonalnych bez reszty dla komputera, można było sprawdzić ów tekst pod względem poprawności syntaktycznej i logicznej. Sprawdzić — to znaczy bądź zaakceptować tekst jako poprawny, bądź zlokalizować i opisać popełnione w nim błędy. Sprawdzić w sposób formalny — to znaczy uczynić to nie odwołując się do rozumienia tekstu, a więc do znaczenia wyrażeń, lecz biorąc pod uwagę tylko fizyczny kształt napisów.
                Nadawanie dowodowi takiej postaci, by nadawał się on do formalnego, czyli mechanicznego sprawdzenia poprawności logicznej, jest od lat kilkudziesięciu praktykowane przez logików pod mianem formalizacji. Słynny program Hilberta postulował sformalizowanie całej arytmetyki w celu dowiedzenia jej niesprzeczności. Losy tego programu, a więc zaskakujące wyniki Gödla wskazujące na niewykonalność wersji maksymalistycznej, a także różne częściowe, lecz ważne jego realizacje — to wszystko sprawy zbyt dobrze znane logikom, aby się nad nimi dłużej zatrzymywać, i równocześnie zbyt złożone, aby na użytek innych zainteresowanych przedstawiać je w krótkiej notatce. Trzeba jednak wspomnieć ów logiczny program formalizacji, bo torował on drogę osiągnięciom informatycznym, o których w tej notatce ma być mowa.
                Formalizacja — jako mechaniczne przekształcanie tekstu przesłanek w tekst wniosku — jest dokładnie tym, czego potrzebuje komputer, aby można było wdać się z nim w dyskusję na temat poprawności dowodu. Sprawa nie jest jednak tak prosta, jak mogłoby się wydawać z samego zestawienia definicji formalizacji i definicji komputera. Owa uprawiana przez logików formalizacja w stylu Hilberta prowadzi bowiem do takiego wydłużenia dowodów i tak nużącej pedanterii, że mimo swych niezaprzeczalnych walorów teoretycznych nie mogła odegrać większej roli w praktyce matematycznej. Koliduje ona ze zdrową tendencją do intuicyjności (zakłócanej zbytnim rozdrobnieniem na kroki dowodowe) i do ekonomii wysłowienia.
                Dopiero wraz z komputerami pojawiła się możliwość takich procedur, które, zachowując walory hilbertowskiej formalizacji, dawałyby zarazem teksty dowodów zbliżone objętością i stopniem intuicyjności do dowodów znanych ze zwykłej praktyki matematycznej. Trudno jest podać ogólną ideę charakteryzującą takie procedury. Osiągnięcie to wymaga wielkiej liczby szczegółowych rozwiązań technicznych w toku programowania. Mechanizm pisania na kartce papieru (właściwy przedkomputerowej formalizacji) zostaje zastąpiony procesami elektronicznymi, te zaś, pozostając w kategorii mechanizmu, mogą zarazem symulować pewne kroki intuicyjne, a więc będące skrótami w stosunku do owej formalizacji za pomocą kartki i ołówka. Tak, na przykład, w pewnym systemie formalizacji komputerowej (o którym niżej) opuszczanie i dołączanie kwantyfikatora ogólnego jest potraktowane jako “oczywiste” i nie wymaga nowych wierszy dowodowych (których wymaga “ręczna” formalizacja), a zarazem jest to operacja mechaniczna, ponieważ jej wykonanie zawdzięcza się “włożonemu” do maszyny algorytmowi.
 
* * *
 
                Rozwijanie i upowszechnianie systemów w rodzaju wyżej opisanych należy do działalności PTI prowadzonej w Sekcji języków informacyjno–logicznych. Nazwa tej sekcji nie jest bardzo fortunna (może lepszy byłby w tej roli zwrot użyty w tytule obecnego komunikatu), ale i z niej można wyczytać nawiązanie do owych wspomnianych dwóch etapów w dziejach formalizowania. Języki sformalizowane z fazy przedkomputerowej były językami logicznymi, które nie nadawały się do komunikowania, czyli do wymiany informacji w obrębie społeczności informatyków; w tym sensie nie były te języki logiczne językami informacyjnymi. Nie mogły być językami informacyjnymi nie tylko z racji wspomnianej już małej operatywności, lecz także dlatego, że pozwalały one na zapisanie formalne tylko części dyskursu matematycznego, tej mianowicie części, która jest zawarta w formułach symbolicznych (w tzw. wzorach). Ale równie istotne dla konstrukcji dowodu są jego partie formułowane w języku naturalnym: Matematyk pisze np. w dowodzie: “Załóżmy najpierw, że... (tutaj następuje jakaś formuła). Wynika z niej, że... (tutaj znowu formuła). W przypadku ogólnym oznaczmy przez... (tutaj jakiś symbol)“; itd. Takie sformułowania pozasymboliczne również wpływają na poprawność lub niepoprawność dowodu, ale jako nie poddające się formalizacji (przedkomputerowej) nie mogą być testowane przez żaden algorytm.
                Istota przeto projektu logiczno–informacyjnego zawiera się w dwóch punktach: 1° opracować sposób formalizacji całego tekstu matematycznego (a nie tylko jego partii symbolicznych), co wymaga uprzedniej refleksji teoretycznej nad konstrukcją tekstów dowodów, a więc i sensem wyrażeń wprowadzających tę konstrukcję; 2° formalizację w jej zakresie tradycyjnym (tj. w odniesieniu do formuł) zmodyfikować w taki sposób, aby uzyskała intuicyjność i zwięzłość w rodzaju tej, jaka cechuje typową praktykę matematyczną.
                Przejdźmy do paru kronikarskich danych na temat tego, co z owych dalekosiężnych zamysłów zostało już zmaterializowane, to znaczy co udało się wcielić w algorytm dla komputera, w procedurę obsługi, w wydruki zawierające oceny poprawności dowodów.
 
* * *
 
                Idea takiej formalizacji i w ślad za nią idące prace pojawiły się niezależnie od siebie w kilku miejscach naraz w okolicy początku lat siedemdziesiątych. Działo się to, w szczególności, w uniwersytecie Stanforda, USA, w politechnice w Eindhoven, Holandia, i w Uniwersytecie Warszawskim (w jego części białostockiej), a z chwilą utworzenia PTI powstała dla polskiego projektu wielce dogodna baza organizacyjna w postaci odpowiedniej sekcji Towarzystwa.
                Projekt polski nosi nazwę Mizar (od pewnej gwiazdy, która, choć nie ma związku z treścią projektu, okazała się dla niego gwiazdą szczęśliwą). Jego autorem jest dr Andrzej Trybulec, kierownik Zakładu Podstaw Informatyki w Instytucie Matematyki Uniwersytetu Warszawskiego w Białymstoku (w roku, akademickim 1984/85 wykładowca matematyki i Mizara w uniwersytecie stanu Connecticut, USA).
                W języku Mizar daje się potencjalnie wyrazić cała matematyka, a także teksty nie–matematyczne, np. argumenty filozoficzne, jeśli ich formalizacja nie wykracza poza środki dowodowe właściwe matematyce (tak np. sprawdzono w Mizarze antynomię kłamcy i inne paradoksy filozoficzne). Użyłem słowa “potencjalnie”, ponieważ projekt jest realizowany etapami. Nie mogąc w tej notatce‚ zdać sprawy z wszystkich zrealizowanych etapów, ograniczę się do fragmentu nazwanego Mizarem MSE, który jest stosunkowo najlepiej wytestowany w praktyce dydaktycznej w Uniwersytecie Warszawskim oraz, co warto wspomnieć, w kursie korespondencyjnym miesięcznika Delta (większość tych kursów prowadzi Zakład Logiki, Metodologii i Filozofii Nauki Uniwersytetu Warszawskiego w Białymstoku, reprezentowany przez niżej podpisanego).
                Mizar MSE jest to symbolem wielozakresowego (ang. multisorted) rachunku predykatów z równością (ang. equality), do czego nawiązuje skrót MSE. W wersji dotychczas stosowanej nie ma symboli funkcyjnych, ale została też już opracowana wersja z funkcjami. Program Mizara MSE, podobnie jak innych wersji Mizara, jest napisany w Pascalu. “Kwatera główna” znajduje się w białostockiej części Uniwersytetu Warszawskiego, gdzie są do dyspozycji maszyny SM 4 (wzorowana na PDP 11) i Apple 2 (tę drugą zawdzięczamy współpracy na polu Mizara z belgijskim uniwersytetem w Louvain).
                Praca z komputerem wygląda jak następuje. Badacz lub student pisze dowód w języku Mizar MSE, który składa się z notacji logicznej oraz wziętych z angielskiego zwrotów służących do nadania dowodowi określonej struktury, np. ASSUME, CONSIDER, LET X BE REAL, NOW, HENCE, THUS itp., oraz ze znaków interpunkcyjnych i znaków służących do nadawania nazw formułom. Po wprowadzeniu tekstu dowodu wywołuje się system sprawdzający, tzw. checker. System ten wykrywa i zgłasza ewentualne błędy syntaktyczne lub logiczne, wskazując miejsce ich pojawienia się w tekście oraz opisując ich rodzaj (np. brak znaku interpunkcyjnego, wadliwa struktura gramatyczna, nie zadeklarowana zmienna, niezgodność deklaracji zmiennych z tezą, brak wynikania logicznego). Otrzymana diagnoza pozwala sporządzić poprawioną wersję dowodu, tę znowu poddać sprawdzeniu, i tak dalej, aż dowód okaże się bezbłędny, co obwieści na ekranie i na wydruku napis: OK. NO ERRORS DETECTED. THANKS.
                Problem walorów dydaktycznych takiego postępowania to temat osobny, do którego warto jeszcze będzie wrócić. Trzeba też wspomnieć, że aczkolwiek zastosowania dydaktyczne są tymi, od których zaczyna się praktyczne wprowadzanie Mizara w życie, to nie są one jedyne, a może nawet nie one okażą się najważniejsze. Dla bardziej zaawansowanych wersji oczekiwana jest przydatność w samej działalności badawczej matematyków, polegająca na możliwości sprawdzania długich i żmudnych dowodów. Podobnej natury przedsięwzięciem będzie badanie poprawności programów. Mizar zdaje się też być idealnym językiem dla banków danych matematycznych, ponieważ można w nim wyrażać treści matematyczne w formie zwięzłej, powszechnie dostępnej dla ludzi i komputerów, a przy tym podatnej na algorytmy przetwarzania danych (przekładu, streszczania, indeksowania itp.).
 
* * *
 
                Kilka słów o najbliższych pracach sekcji. Przyjęto taką strategię, by poniechać zrazu myśli o aspektach komercyjnych (aczkolwiek nie jest to myśl zdrożna i zasługuje, by do niej wrócić), skoncentrować się natomiast na wytworzeniu jak największego kręgu zainteresowanych tym systemem w kraju i zagranicą. Kontakt z zagranicą jest istotny nie tylko dlatego, że każdy wynik naukowy i techniczny ma zasięg międzynarodowy, lecz także dlatego, że uboga baza sprzętowa w naszym kraju nie stwarza możliwości rozwojowych (słowo “uboga” jest tutaj zbyt łagodne; w obliczu rozlicznych utrudnień, m. in. polskich przepisów celnych dotyczących przywozu mikrokomputerów do kraju, grozi nam w informatyce regres nie do odrobienia). Pierwsze osiągnięcia na polu kontaktów zagranicznych — to zaproszenie twórcy Mizara na roczny kontrakt do USA oraz współpraca z uniwersytetem w Louvain, gdzie przez kilka miesięcy latem 1984 przebywała ekipa prowadząca kursy Mizara dla pracowników uczelni i dla nauczycieli informatyki z belgijskich szkół średnich.
                To jest dopiero początek przedsięwzięcia, które będzie wymagać nieprzeciętnej mobilizacji. To, co jest do zrobienia w najbliższym czasie, to przygotowanie materiałów informacyjnych, zwłaszcza zaś pomocy dydaktycznych do nauczania logiki w systemie Mizar MSE. Istnieje wydany w serii Instytutu Podstaw Informatyki PAN tzw. Primer, zawierający kurs Mizara po angielsku, aplikowany do pewnego fragmentu elementarnej geometrii (autorstwa K. Prażmowskiego i P. Rudnickiego). Istnieje zbliżony do treści Primera kurs w Delcie, zainicjowany w specjalnym jej numerze wydanym po angielsku z okazji Światowego Kongresu Matematyków 1983 w Warszawie (ciąg dalszy tego kursu jest, oczywiście, po polsku). Istnieją dość liczne raporty i opisy, m. in. seria opisów w kilku kolejnych rocznikach, od 1980, wydawanych przez Zakład Logiki, Metodologii i Filozofii Nauki Uniwersytetu Warszawskiego w Białymstoku pt. Studies in Logic, Grammar and Rhetoric, gdzie są też publikowane raporty o porównywalnych projektach z uniwersytetu Stanforda i politechniki w Eindhoven (nadesłane przez współautorów tych projektów).
                Żadne jednak z tych opracowań nie zaspokaja najpilniejszej obecnie potrzeby zwięzłego podręcznika logiki i zestawu zadań w Mizarze, na tym więc będą się koncentrować najbliższe prace sekcji. Dzięki dotacji przyznanej sekcji przez Zarząd Główny PTI można było powierzyć tę pracę osobom równie kompetentnym w logice co w posługiwaniu się Mizarem, które mają za sobą pierwsze doświadczenia dydaktyczne, a przed sobą duże możliwości dalszego eksperymentowania (zawdzięczamy je zrozumieniu na różnych szczeblach administracji akademickiej uniwersytetu w Białymstoku). Ukończenie pierwszej wersji tych pomocy dydaktycznych jest oczekiwane w ciągu najbliższych 4 do 5 miesięcy. Po ich przetestowaniu w praktyce dydaktycznej będzie pora na ulepszoną wersję i na dokonanie jej przekładu na angielski. W tej postaci wejdą one w skład oferty składanej naszym potencjalnym partnerom w posługiwaniu się Mizarem, w kraju i zagranicą. Byłoby bardzo pożądane, gdyby owi partnerzy ukonstytuowali się w coś w rodzaju Klubu Użytkowników Mizara (Mizar Users Club), którego centrum stanowiłaby nasza sekcja, cyrkulacja zaś materiałów przyjęłaby systematyczną formę jakiegoś Mizar Newsletter. Można też rozważać inne formy upowszechniania, np. stałą współpracę z jednym z periodyków informatycznych o światowym zasięgu (podatne na taką kooperację są np. łamy American Journal of Computational Linguistics). O wyborze którejś z takich ewentualności będziemy myśleć w następnej fazie, tymczasem zaś trzeba przygotować jak najtreściwszą ofertę.
 
* * *
 
                Na koniec akcent trochę subiektywny, ale z intencją ukazania pewnej obiektywnej historycznej perspektywy. Niżej podpisany zainteresował się Mizarem z pozycji historyka logiki, zwłaszcza logiki XVII wieku. W tym to wieku powstał wielki projekt uniwersalnej matematyki (mathesis universalis), w którym postulowało się stworzenie wspólnej podstawy pojęciowej dla całej matematyki i wszelkich nauk matematyzowalnych oraz stworzenie uniwersalnego i maksymalnie sprawnego języka z wbudowanym weń rachunkiem logicznym (calculus ratiocinator). Pierwsza część tego wielkiego zamysłu zaczęła się na dobre realizować pod koniec wieku XIX w dziele Fregego, Cantora, Peano, Russella i in., poprzedzonym prekursorskimi osiągnięciami Boole’a oraz, jeszcze z wieku XVII, Leibniza. Ten etap realizacji mathesis universalis polegał na stworzeniu bazy pojęciowej integrującej całość matematyki; podstawę tę utworzyła logika matematyczna z teorią mnogości. Na drugi etap, mniej teoretyczny a bardziej praktyczny, przyszła pora w epoce bardzo sprawnych i powszechnie dostępnych komputerów; dopiero wtedy można stworzyć język matematyczny do dialogu z komputerem, który to język jest równie odpowiedni do dialogu matematyków między sobą a językiem powszechnym będzie się stawać automatycznie, przez fakt powszechnego posługiwania się komputerami. Nie jest jednak przesądzone, czy przyszłość ta czeka Mizara, czy inny z języków tej kategorii, nad którymi pracuje się intensywnie w różnych ośrodkach. Trudno przewidzieć, czy któryś, z tych języków wyprze pozostałe, czy też ustali się jakiś podział na strefy wpływów. Gra się zaczęła. Trzeba do niej przystąpić, wierząc w gwiazdę Mizara.

Witold Marciszewski

Archiwum PTI Ewa Łukasik ( elukasik@cs.put.poznan.pl) Grzegorz Przybył ( grzegorz.przybyl@wp.pl ) www.pti.org.pl Kontakt PTI ( pti@pti.org.pl )
Tutorial


Tutorial

Wyszukiwanie

Całość
tylko prodialog
tylko biuletyny
tylko konferencje
tylko multimedia
tylko sprawozdania
tylko uchwały
tylko zawody
tylko zjazdy
pozostałe treści

Rodzaj przeszukiwania
Słowa kluczowe
Pełen tekst

pelen zakres dat
ograniczony zakres
od:

do:




Kontakty

Instytut Informatyki

Polskie Towarzystwo Informatyczne

Nasz Skrzynka Pocztowa

+ - D A