On Saturday, March 28, 2015 at 9:45:23 AM UTC+1, g...@g...com wrote:
> W dniu sobota, 28 marca 2015 05:04:04 UTC+1 użytkownik M.M. napisał:
>
> > > W takim razie zgoda -- tego rodzaju "poprawność" jest niemożliwa do uzyskania.
> > > Należy jednak mieć na uwadze, że z formalnego punktu widzenia poprzez
> > > "poprawność" dowodu rozumie się to, czy każdy krok jest zgodny z regułami,
> > > natomiast w tym przypadku raczej należałoby użyć słowa "adekwatność"
> > > (na przykład teza Churcha-Turinga postuluje adekwatność maszyny Turinga
> > > jako modelu ujmującego intuicyjne rozumienie obliczalności)
> >
> > Mój (hipotetyczny) klient zamawia najlepszy program do gry w
> > szachy o łącznym rozmiarze kodu i danych nie większym niż 1MB. Napisałem
> > taki program. Jak mam przeprowadzić dowód, że nie istnieje w
> > ramach tego rozmiaru lepszy program?
>
> To akurat nie jest problem metody dowodowej,
Właśnie, tego nie da się udowodnić, a jest to też ważny aspekt
programu. A w testach tak się robi, porównuje się kilka
różnych algorytmów dla różnych danych.

> tylko nieprecyzyjnej
> specyfikacji. Co to znaczy,że "w ramach określonego rozmiaru program
> jest lepszy od innego programu"?
Zakładamy że specyfikacja jest dobra. To jest kwestia jakości
użytych algorytmów/heurystyk.


> Zresztą cechy użytkowe nie są czymś, co dowodzi się formalnie
> (bo są subiektywne). Formalnie chcemy dowodzić raczej pewnych
> inwariantów -- że na przykład w programie wielowątkowym nie dojdzie
> do sytuacji dead-locku (klasyczne zastosowane logik temporalnych),
Nie słyszałem o logice temporalnej. Może się mylę, ale to się
wydaje łatwe. Dla mnie taki dowód sprowadza się do tego, aby
wszystkie pary kodu, który może wykonać się równolegle, były
opatrzone semaforami w tej samej kolejności w sensie wykonania i
w odwrotnej kolejności (też w sensie wykonania).


> że dla określonej klasy danych wejściowych program się zatrzyma,
> że zużycie zasobów w czasie działania programu będzie ograniczona
> określoną funkcją od czasu działania i rozmiaru danych wejściowych
> itd.
To czasami może być trudne, np. problem Collatza. Pytanie czy
czas wykonania i inne zasoby są znanymi/łatwymi funkcjami danych
wejściowych. Jeśli zapotrzebowanie na zasoby w danym programie
nawet da się rozbić na wiele małych-łatwych funkcji, to może
potem wyjść: f1(N) * f2(N) * f3(N) * f4(N) * f5(N). Można
wziąć maksimum każdej z tych pięciu funkcji i podać, jako oszacowanie
górne, iloczyn maksimów. Ale w praktyce oszacowanie górne
może nie mieć nic wspólnego z rzeczywistością, gdy f1
przyjmuje maksimum, to pozostałe funkcje mogą przyjmować
małe wartości. Zależności fi od fj (i!=j) może być bardzo
skomplikowana...

Pozdrawiam