Mizar-MSE używany w programie Eddie::MSE różni się nieco od klasycznej wersji Mizara-MSE.
W poniższym tekście opisane są pokrótce same zmiany jak i motywacja stojąca za ich wprowadzeniem.
Mianowicie:
Szczegóły:
W klasycznej wersji Mizar-MSE nie ma instrukcji wprowadzającej sorty explicite.
Sorty są "zbierane", tzn. parser, napotykając na nowy typ (np. w instrukcji reserve)
dodaje go do listy zdefiniowanych typów (nie zgłaszając żadnych błędów).
Może to prowadzić do sytuacji, gdy np. literówka w nazwie sortu (np. POINT i PONT) powoduje,
że wprowadzony zostaje nowy typ. To, z kolei, może prowadzić do dziwnych błędów,
gdy staramy się dowodzić twierdzenia lub korzystać z twierdzeń tak naprawdę zapisanych z innymi typami.
O ile błąd taki doświadczony mizarowiec wykryje dosyć szybko,
osoby z małym doświadczeniem mogą mieć z tym wiele problemów.
Wprowadzona została zatem nowa instrukcja środowiska sort pozwalająca wprowadzać sorty (typy).
W pojedynczej instrukcji sort można zdefiniować jeden lub wiele sortów naraz.
environ
sort set;
sort POINT, LINE, PLANE;
begin
Jeżeli teraz użytkownik spróbuje np. zarezerwować zmienną dla danego typu,
a wprowadzi nazwę typu niezgodną z wcześniej zdefiniowanymi,
zostanie zgłoszony odpowiedni błąd.
Góra
Tak jak w klasycznej wersji Mizara-MSE nie ma instrukcji na wprowadzanie sortów,
tak też nie ma instrukcji na wprowadzanie predykatów.
Parser, napotykając na nowy predykat (w kolejnym aksjomacie czy definicji stałej)
dodaje go do listy zdefiniowanych predykatów nie zgłaszając żadnych błędów.
Zarówno literówki w nazwie predykatu, jak i zmiana kolejności sortów zmiennych w predykacie powodują,
że wprowadzony zostaje nowy predykat. To, z kolei, znowu może prowadzić do nieoczekiwanych błędów.
Wprowadzona została zatem nowa instrukcja środowiska pred pozwalająca wprowadzać predykaty.
W pojedynczej instrukcji pred można zdefiniować tylko jeden predykat,
a sama definicja polega na podaniu nazwy predykatu, następnie listy sortów.
Tylko zmienne i stałe odpowiednich sortów, i w odpowiedniej kolejności,
będą mogły być wykorzystywane w danym predykacie w dalszej części artykułu.
Przykłady:
environ
sort set;
sort LINE, POINT;
pred p[];
pred in[set, set];
pred ON[LINE, POINT];
begin
Jeżeli użytkownik wprowadzi niechcący nowy predykat,
np. zamieniając nieświadomie kolejność zmiennych w predykacie ON,
zostanie zgłoszony odpowiedni błąd.
Góra
W klasycznej wersji Mizara-MSE można korzystać jedynie z prefiksowego zapisu predykatów:
for A, B being POINT, K, L being LINE st
ON[A, K] & ON[A, L] & ON[B, K] & ON[B, L] holds
A = B or K = L;
for X, Y, Z being set holds
SUM[Z, X, Y] iff
for x being set holds
IN[Z, x] iff IN[X, x] or IN[Y, x];
Nie widząc definicji należenia punktu do prostej, czy sumy zbiorów,
w dalszej części artykułu można łatwo zapomnieć, czy w predykacie ON najpierw podajemy prostą, czy punkt.
Czy też czy w predykacie SUM najpierw podajemy składowe sumy, czy sumę zbiorów.
Jasne jest, że w takich przypadkach znacznie bardziej czytelny jest infiksowy zapis predykatów.
Toteż wprowadzona została możliwość definiowania takiego zapisu w Eddie::MSE:
environ
sort LINE, POINT;
sort set;
pred POINT on LINE;
pred set in set;
pred set is_sum_of set, set;
i wtedy:
Ax1:
for A, B being POINT, K, L being LINE st
A on K & A on L & B on K & B on L holds
A = B or K = L;
Ax2:
for X, Y, Z being set holds
Z is_sum_of X, Y iff
for x being set holds
x in Z iff x in X or x in Y;
begin
Wydaje się, że druga forma zapisu znacznie ułatwia zrozumienie tekstu,
zarówno czytelnikom, jak i autorowi. :-)
Choć, dla zachowania wstecznej kompatybilności i "ducha" klasycznego Mizara-MSE,
prefiksowy zapis predykatów jest nadal dozwolony.
Góra
|
Mizar
