W dniu wtorek, 31 marca 2015 14:48:38 UTC+2 użytkownik M.M. napisał:
> >
> > To, że "nie istnieje w ramach określonego rozmiaru >>lepszy<< program"
> > jest "ważnym aspektem programu"? Dla kogo jest to ważne?
> Uprościłem pewien aspekt złożoności do 'rozmiaru' - miałem bardzo
> podobną sytuację w praktyce. Ale ok, nie ciągnijmy.
>
> > Klienta interesuje, żeby program działał zadowalająco dobrze, a nie to, żeby
> > "w ramach określonego rozmiaru programu nie istniał jakiś lepszy".
> Nie zgodzę się, klient może chcieć aby program działał jak najlepiej
> to możliwe - w ramach jakiś ograniczeń.

"Najlepiej jak to możliwe" -- to też nieprecyzyjne określenie.
Można je rozumieć jako "najlepiej jak komputer potrafi", albo
"najlepiej jak programista potrafi". To ostatnie jest zresztą
zazwyczaj twardym limitem, chyba że klient znajdzie lepszego
programistę

> > (W każdym razie ja nie spotkałem nigdy klienta o tak osobliwych
> > zainteresowaniach. Ale nawet gdybym spotkał, pewnie po prostu nie
> > uwierzyłbym własnym uszom)
> Dlaczego byś nie uwierzył? Program wspomaga decyzje. Od decyzji zależy
> (w jakimś stopniu) generowanie zysków. Co w tym dziwnego, że chcemy
> aby taki program działał jak najlepiej.

Powiedzieć, że coś "działa jak najlepiej", to coś innego, niż
powiedzieć, że "nie istnieje w ramach pewnych ograniczeń lepszy program"
(nie jest nawet jasne, co się tutaj rozumie w kwestii "istnienia programu"
-- czy chodzi o jakiś program dostępny na rynku, czy taki, który
ktoś potencjalnie mógłby napisać)

> Inny przykład, program do translacji języków naturalnych. Dlaczego
> chciałbyś używać gorszy program niż lepszy?

Ja nie wiem, co to znaczy w tym kontekście "gorszy", a co "lepszy"

> Następny problem: gra w szachy. Dlaczego używać słabszego programu niż
> silniejszego? Można mnożyć...

Zgaduję teraz, że pisząc o "program do gry w szachy" masz na myśli
"program grający w szachy"? Jeśli tak, to ok -- rozumiem, co to znaczy
"lepszy", a co "gorszy" (choć oczywiście jest to tylko częściowy
porządek)

> > Nie widzę też, w jaki sposób testy miałyby tu być pomocne.
> Bierzesz wiele danych wejściowych, porównujesz jakość odpowiedzi i
> oceniasz. A jak na podstawie kodu udowodnić, że jeden program lepiej
> translatuje, albo lepiej gra w szachy, od drugiego?

Oczywiście, kiedy masz już pewne kryterium jakości, to możesz się
pokusić o przeprowadzenie formalnego dowodu w odniesieniu do tego
kryterium

> > To, co piszesz, nic nie wyjaśnia.
> > Powiedzenie, że coś jest najlepsze, jest po prostu powiedzeniem
> > nieprecyzyjnym.
> Wiadomo że jest nieprecyzyjnym. W każdym przypadku co innego
> oznacza najlepszy. W każdym przypadku chodzi o inną jakość algorytmów czy
> heurystyk. Obojętnie o jaką jakość chodzi, to trudno dowieść jej
> formalnie na podstawie kodu.

Przeciwnie. Dla pewnych kryteriów przeprowadzenie formalnych dowodów
będzie prostsze, dla innych trudniejsze, a dla jeszcze innych niemożliwe.

> > Co to znaczy "najlepsze"? Że przynosi najwięcej
> > pieniędzy? Że ma najwięcej użytkowników? Że najbardziej podoba
> > się klientowi?
> Tak, dobre przykłady.
>
> > Jeżeli podajesz jawnie złą specyfikację, to potem nie możesz mówić
> > "zakładamy, że specyfikacja jest dobra", bo nie jest.
> Można tak mówić, ponieważ to generalne określenie w każdym przypadku
> się konkretyzuje. Bez względu na to jak się skonkretyzuje, to ciężko
> dokonać takiego dowodu formalnego.

Nieprawda. To, jak się coś skonkretyzuje (oraz co się skonkretyzuje),
ma kluczowe znaczenie dla łatwości/trudności przeprowadzenia dowodu.

> > > > 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).
> >
> > Mylisz się z pewnością, choćby dlatego, że semafor nie jest jedynym
> > mechanizmem synchronizującym używanym w programach wielowątkowych.
> Jeśli odebrałeś moje słowa dosłownie, to mam prośbę. Najpierw uogólnij
> sobie mój 'semafor' na inne mechanizmy synchronizowania, a potem
> przeanalizuj czy się mylę. Potem pogadamy dalej.

Na przykład w API CUDA dla GPU nVidii masz polecenie __syncthreads(), które
działa w taki sposób, że wszystkie wątki czekają, aż ostatni wątek wywoła
owo polecenie. Deadlocka otrzymamy w każdym przypadku, gdy którykolwiek
z wątków w danej jednostce uruchomieniowej nie wywoła polecenia __syncthreads().
W jaki sposób przetłumaczyłbyś tę sytuację na swój "ogólniony semafor"?