On Friday, March 27, 2015 at 1:21:22 PM UTC+1, g...@g...com wrote:
> W dniu piątek, 27 marca 2015 12:24:48 UTC+1 użytkownik M.M. napisał:
> > On Friday, March 27, 2015 at 10:57:26 AM UTC+1, g...@g...com wrote:
> > > Oczywiście pewien problem natury epistemicznej wiąże się ze sformułowaniem
> > > odpowiedniej listy aksjomatów, które miałyby odzwierciedlać rozważany
> > > przez nas problem
> > Właśnie o tym pisałem. Poprawność dowodu, to też jego poprawność w
> > odzwierciedlaniu oryginalnego zadania.
>
> 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?



>
> Jednak z drugiej strony jeśli mamy na przykład dowód indukcyjny twierdzenia,
> że funkcja "append" zdefiniowana (dajmy na to w czymś haskelopodobnym) jako
>
> append [] y = y
> append (h:t) y = h:(append t y)
>
> jest operatorem łącznym, tzn dla dowolnych skończonych list a, b, c
> append (append a b) c === append a (append b c)
>
> to tak naprawdę trudno jest to kwestionować i podważać, tzn. albo uznajemy
> regułę indukcji, i wtedy musimy uznać dowód za poprawny, albo jej nie uznajemy,
> i obawiamy się, że "mogą istnieć takie listy, dla których append wcale
> nie będzie się zachowywał jako operator łączny" -- choć byłoby czymś
> szokującym, gdyby ktoś był w stanie podać pozbawione błędów rozumowanie,
> które pozwalałoby taki obiekt skonstruować. Tym bardziej trudno byłoby
> tutaj sformułować zarzut nieadekwatności, bo nie za bardzo można wskazać
> jakąś zewnętrzną dziedzinę problemową, do której mielibyśmy odnosić
> dowód
>
> (a przy okazji jak kogoś ciekawi, to znajdzie ten dowód w notatkach
> http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jr
h-1996/all.pdf
> na stronie 86)