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

do góry

> Automatyczne sprawdzanie poprawności to "święty Graal" informatyki.

Może nie informatyki, ale w weryfikacji jako działce inżynierii oprogramowania, na
pewno by się przydało.

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

Nic nie szkodzi. Nikt zdrowy nie robi maszyn Turinga, więc fakt, że jakaś tam jeszcze
inna maszyna Turinga nie może istnieć, nie jest dla nikogo żadnym dramatem.

Ciekawszym tematem jest napisanie programu, np. w C, do sprawdzania poprawności
innego programu, np. w C.

--
Maciej Sobczak * http://www.inspirel.com

do góry

On Thu, 10 Aug 2017 02:34:32 -0700 (PDT), g...@g...com
wrote:
> Naprawdę byłoby fajnie, gdybyś

A mi szczerze wisi co steruje bramą od garażu: może być nawet Proust
a nie Rust.

do góry

On Thu, 10 Aug 2017 03:17:44 -0700 (PDT), "M.M." <m...@g...com>
wrote:
> A matematycy potrafią sprawdzać.

Nie potrafią. Patrz tw. Goedela. Muszą być aksjomaty. A tych się nie
da sprawdzić. Nie dlatego że starożytni Grecy zrobili tabu, ale
dlatego że nie jest to możliwe.

do góry

On Thu, 10 Aug 2017 05:19:16 -0700 (PDT), Maciej Sobczak
<s...@g...com> wrote:
> Nic nie szkodzi. Nikt zdrowy nie robi maszyn Turinga


Robi. Dla zabawy, np. z klocków Lego.

do góry

On Thursday, August 10, 2017 at 2:19:17 PM UTC+2, Maciej Sobczak wrote:
> > Automatyczne sprawdzanie poprawności to "święty Graal" informatyki.
>
> Może nie informatyki, ale w weryfikacji jako działce inżynierii oprogramowania, na
pewno by się przydało.
>
> > Co prawda udowodniono matematycznie że nie może istnieć maszyna Turinga
> > sprawdzająca poprawność innej maszyny Turinga
>
> Nic nie szkodzi. Nikt zdrowy nie robi maszyn Turinga, więc fakt, że jakaś tam
jeszcze inna maszyna Turinga nie może istnieć, nie jest dla nikogo żadnym dramatem.
>
> Ciekawszym tematem jest napisanie programu, np. w C, do sprawdzania poprawności
innego programu, np. w C.

Dlaczego? Na MT też można napisać program w C, jakie różnice masz
na myśli? Z teoretycznego punktu widzenia jest ważna różnica,
ale pomiędzy komputerem a MT, nie pomiędzy językiem. Komputer ma
(póki co) skończoną pamięć, MT nieskończoną.

Pozdrawiam

do góry

On Thursday, August 10, 2017 at 2:57:08 PM UTC+2, slawek wrote:
> On Thu, 10 Aug 2017 03:17:44 -0700 (PDT), "M.M." <m...@g...com>
> wrote:
> > A matematycy potrafią sprawdzać.
>
> Nie potrafią. Patrz tw. Goedela. Muszą być aksjomaty. A tych się nie
> da sprawdzić. Nie dlatego że starożytni Grecy zrobili tabu, ale
> dlatego że nie jest to możliwe.

Zależy o jakie sprawdzenie chodzi. Zwykle sam sposób sprawdzania jest
także aksjomatem, dowodzenie przez indukcję jest aksjomatem. Na wiarę
przyjmujemy, że przeprowadzony dowód przez indukcję oznacza, że
twierdzenie jest prawdziwe.

Natomiast praktyczna i teoretyczna przydatność systemu formalnego
wynikłego z aksjomatów jest pewnym sposobem sprawdzania aksjomatów -
albo są przydatne, albo nie.

Pozdrawiam

do góry

Użytkownik <g...@g...com> napisał:

> C# nie jest ulepszeniem C.

Masz 100% racji.
Ba! C# nawet nie "siedzialo" kolo C.
Siedzialo za to baaaardzo blisko Javy (szczegolnie J++:).

PS: A bylo to tak. Sun raptem cofnal pozwolennie na adoptowac swego niechcianego,
ale wszak calkiem fajnego w swiecie Win dziecka (J++) wiec, MS urodzil swoje (.NET,
C#)

AK

do góry

On Thursday, August 10, 2017 at 8:39:23 PM UTC+2, slawek wrote:
> On Thu, 10 Aug 2017 18:06:59 +0200, "AK" <n...@n...net> wrote:
> > Ba! C# nawet nie "siedzialo" kolo C.
>
> Siedziało, siedziało.
>
> C# jest - według MS - lepszym językiem niż C++. Tak że programiści
> używający dotychczas C++ powinni przesiąść się na C#. Ogólnie jest
> językiem z klamrowymi nawiasami, czyli bliżej mu do C niż do Algolu,
> Fortranu, Lispa czy Basha. Oczywiście jest językiem OOP, ale C++ też
> jest (a zgadzamy się że C++ wywodzi się z C).
>
> Oczywiście że są "podobieństwa" pomiędzy Javą a C#. Twórcy Javy
> celowo zrobili wiele rzeczy tak jak w C++ (choćby operator ==), więc
> i w ten sposób C# dziedziczy niektóre rzeczy po C++, a więc także po
> C.

Panowie, powiedzcie mi, co to jest język programowania? Jak używacie
tego pojęcia? Bo z wyglądu, szczególnie gdy w C++ nie nadużywa się
ficzerów (domyślcie się co mam na myśli), to Java, C# i C++ naprawdę
są podobne. Myślę, że w C# bardzo przyjemnie się programuje, chociaż
mam znikome doświadczenie.


Pozdrawiam

do góry

On Thu, 10 Aug 2017 12:20:12 -0700 (PDT), "M.M." <m...@g...com>
wrote:
> [Czy] w C# bardzo przyjemnie się programuje

C# jest niesamowicie przyjemny, bo Visual Studio niemal samo pisze
programy, wszystko podpowiada itd. Odśmiecanie działa magicznie, są
lambdy itp. wynalazki. A co najważniejsze - jest ładnie, bo MS
wymyślił (czego nie ma Java) słowo kluczowe partial. Więc brzydkie
rzeczy są zamiatane do innych plików.

Jednak jest haczyk. C# to przejście na Ciemną Stronę Mocy, czyli
mocne uzależnienie od MS. Jeżeli ktoś tego nie chce lepiej niech
trzyma się Javy. Praktycznie niemal to samo, ale teoretycznie program
w Javie ruszy na czymkolwiek, z Rasberry Pi i Linuksem włącznie.

Java też nie jest aż tak swobodna. Łapę trzyma Oracle i podobno nawet
groził procesami za niekupienie licencji (potrzebna dla embeded).

do góry