On Thursday, August 10, 2017 at 7:48:35 AM UTC+2, Borneq wrote:

> Co prawda udowodniono matematycznie że nie może istnieć maszyna Turinga
> sprawdzająca poprawność innej maszyny Turinga,

A matematycy potrafią sprawdzać. Czy to by oznaczało, że człowiek jest
komputerem lepszej jakości niż MT?

Moim zdaniem może sprawdzać, co łatwo udowodnić: Na nieskończonej
taśmie MT mamy pary uporządkowanie (X,Y), gdzie:

X) ciąg instrukcji
Y) zero lub jedynka (lub informacje o problemie stopu, itd)

Pary są oddzielone symbolem specjalnym, który nie pojawia się w żadnym
programie. Przykładowo, rozpatrujemy programy o N instrukcjach, więc
zero to jest symbol N+1, jedynka N+2, symbol specjalny N+3.
Pary na taśmie są uporządkowane według programów, tzn kolejne programy z
taśmy po zdekodowaniu są kolejnymi liczbami naturalnymi. Zadajemy
MT ciąg instrukcji. Maszyna dekoduj go na liczbę, następnie omija
tyle znaków specjalnych, ile równa jest ta liczba. Innymi słowy: odszukuje
zadany ciąg instrukcji. Po odnalezionym ciągu instrukcji znajduje zero lub
jedynkę lub jeszcze jakieś inne ciekawe informacje. Jeśli znalazła zero, to
daje odpowiedź że program jest niepoprawny. Jeśli znalazła jedynkę, to
daje odpowiedź że ciąg instrukcji jest poprawny (w jakimś sensie).

MT może udzielać odpowiedzi czy program jest poprawny, czy nie, w czasie
wykładniczym względem ilości instrukcji w programie. Gdyby na MT można
było zaimplementować hash-table, to by mogła udzielać odpowiedzi w
czasie O(1), ale z tego co wiem, na taśmie nie można.

Poza tym można zdefiniować minimalną i maksymalną pozycję głowicy. Jeśli
głowica przekroczy którąś z tych pozycji, to program uznajemy za niepoprawny.
W ramach zakresu od min do maks może istnieć skończona ilość stanów, równa
N ^ (max-min+1), gdzie N to ilość symboli. Na drugiej maszynie można
każdemu stanowi przypisać zero lub jedynkę. Druga maszyna może symulować
pierwszą maszynę dla skończonej ilości danych wejściowych. Gdy pierwsza
maszyna chociaż dla jednych danych osiągnie stan z tabeli oznaczony
zerem, to druga maszyna udzieli odpowiedzi że program jest niepoprawny.
Podobnie, jeśli pierwsza maszyna chociaż dla jednych danych przekroczy
zakres <min,max>, to też druga udzieli odpowiedzi że program jest
niepoprawny. Druga maszyna w trakcie symulowania zapamiętuje stany
pierwszej maszyny, które nie są zdefiniowane. Jeśli któryś ze stanów
powtórzy się, to druga maszyna udzieli odpowiedzi, że pierwsza maszyna
się pętli w nieskończoność dla przynajmniej jednego zestawu danych
wejściowych.

Czyli dużo można, ale są to zazwyczaj możliwości teoretyczne, bo
wymagają czasu wykładniczego. Poza tym jest drugi problem: skąd wziąć
maszynę z odpowiedziami który stan jest poprawny, albo który
ciąg instrukcji jest poprawny? Niemniej, to że nie umiemy podać
takiego programu z odpowiedziami, nie uprawnia nas do mówienia
że W OGÓLE nie można automatycznie weryfikować.



> ale z jednej strony w
> Javie stosuje się system asercji czy unit testy, w C++ jest biblioteka
> GSL i odpowiedni plugin sprawdzający zgodność z nią.
> A Rust wymusza swoje reguły. Trudno początkującemu w Rust jest wręcz
> nieraz dla pewnych przypadków napisać kod który się skompiluje (te
> problemy z mutualnością) ale to jest wymuszone automatycznie, nie musi
> tego sprawdzać programista i czegoś przeoczyć.

Ja bym chciał jakiś tego typu język, ale żeby można było go całkowicie
skompilować do kodu maszynowego i żeby dostępne optymalizatory generowały
tak wydajny kod jak dla C++.

Pozdrawiam