On Tuesday, September 27, 2016 at 9:04:18 AM UTC+2, bartekltg wrote:
> On 27.09.2016 02:22, M.M. wrote:
> > Nie zgadzamy się, bo problem stopu na MT jest rozstrzygalny.
>
> Heh. Jeszcze raz, czego nie rozumiesz w dowodzie na
> nierozstrzygalność problemu stopu na kompie z nieskończoną pamięcią?
>
> Mamy procedurę stop:
>
> stop(program)
>
> zwraca ona true, jeśli program zakończy się, false w p.p.
>
> Procedura stop jest w tej chwili ustalona. Zapisana konkretna liość
> bitów, koniec, ma rozwiązać każdy problem.
>
> Kontrujemy program:
>
> test(X)
> if (stop(X)) //jeśli program X się nie zapętla
> for(;;); //zapętlij się
>
>
>
> Odpalam test(test)
>
> Zapętli się czy nie?
>
> Jeśli twierdzisz, że się zapętli, to
> stop(test)
> wzróci w skończonym czasie false.
> wiec test się zapętli na for(;;)
> Sprzecznosć.
>
> Jeśli twierdzisz, żę się nie zapętli, to
> stop(test)
> w skończonym czasie zwróci false.
> Program wykonał stop(test), sprawdził warunek
> i się zakończył.
> Sprzeczność.
>
> Jakby nie patrzeć, z każdej strony dupa.

Zgadza się, od jakiś 10-15 lat rozumiem ten dowód i się
z nim nie kłócę. Chodzi tylko o to, że jest budowany w
tym dowodzie program o większym rozmiarze od programu
który wykona test-stop. Takiego programu nie ma i
dowód w tym sensie jest poprawny - ale to jest
szczególny przypadek.

Jest to szczególny przypadek, bo program który rozstrzyga
może mieć nieskończony rozmiar. Nazwijmy ten program o
nieskończonym rozmiarze programem X. Program X dla
każdego programu Y o skończonym rozmiarze w skończonym
czasie ustali poprawnie czy program Y się zatrzyma czy
nie dla dowolnego zestawu danych wejściowych. Program X
teoretycznie istnieje, tylko w praktyce nikt nie umie
go (w kompletnej wersji) napisać. Jeśli istnieje program
na MT który rozstrzyga poprawnie problem stopu w skończonym
czasie, to ogólnie problem stopu jest rozstrzygalny.

> A formalniej, istnienie takiej uniwersalnej procedury
> prowadzi do paradoksu (fałszu).
Jak pisałem wyżej, tylko w przypadku szczególnym, gdy
procedura ma np. skończony lub zbyt mały rozmiar. W
przypadku ogólnym nie ma takiego paradoksu.


> A wiec któreś z założeń jest nieprawdziwe. Nie założyliśmy
> za wiele,
No jak to nie za wiele? Założyliśmy że procedura testowa
jest większa od procedury testującej. Tylko nie założyliśmy
tego jawnie, nikt w dowodzie nie mówi: załóżmy że procedura
testowana jest większa od testującej. Proszę Cię bardzo,
wykonaj dowód na odwrotnym przypadku, czyli gdy procedura
testująca ma znacznie większy rozmiar niż testowana.

> więc albo
> matematyka się wali, albo załozenie, że procedura stop
> istenije, jest fałszywe.
No właśnie jest jeszcze jedno założenie w dowodzie: procedura
testowana jest większa od testującej.

Pozdrawiam

do góry

On Tuesday, September 27, 2016 at 12:41:53 PM UTC+2, g...@g...com wrote:
> W dniu wtorek, 27 września 2016 09:04:18 UTC+2 użytkownik bartekltg napisał:
> > On 27.09.2016 02:22, M.M. wrote:
> > > Nie zgadzamy się, bo problem stopu na MT jest rozstrzygalny.
> [...]
> > Jakby nie patrzeć, z każdej strony dupa.
> > A formalniej, istnienie takiej uniwersalnej procedury
> > prowadzi do paradoksu (fałszu). A wiec któreś z założeń
> > jest nieprawdziwe. Nie założyliśmy za wiele, więc albo
> > matematyka się wali, albo załozenie, że procedura stop
> > istenije, jest fałszywe.
>
> Tym niemniej, konstrukcja, którą przedstawił M.M. (która w istocie
> nie dotyczy problemu stopu), wydaje się analogiczna do teorii typów,
> będącej jedną z propozycji rozwiązania Paradoksu Russella
> (o strukturze analogicznej do problemu stopu).
Czy mógłbyś powiedzieć która konstrukcja? Bo było wiele w tym wątku.
Pewnie moja wina, bo niezbyt klarownie piszę i skaczę po zagadnieniach.


> Wydaje się, że tym, czego w istocie dowodzi przedstawiony przez
> Ciebie argument, jest to, że logika dwuwartościowa nie jest
> dość bogata do wyrażania naszych intuicji dotyczących programów
> komputerowych -- bo przecież my jako ludzie nie mamy problemu
> ze zrozumieniem źródła sprzeczności w tym dowodzie. Mianowicie
> dowód ten mówi nam, że pewne programy, które mają explicite
> rozstrzygać o swoich własnych właściwościach, mogą być kłopotliwe
> w analize. (Oczywiście będą również takie, które bez problemu
> rozstrzygają o pewnych swoich właściwościach)
To nie wynika z problemu logiki dwuwartościowej. Logika pięknie
tutaj działa i dowód jest poprawny. Chodzi o to, że logika tutaj
pokazuje nieco inną rzecz niż nierozstrzygalność problemu stopu,
a mianowicie pokazuje szczególny przypadek problemu stopu, gdy
są nałożone ograniczenia na rozmiary programów testowanych i testujących.



> Oczywiście temat jest bardzo słynny i szeroko dyskutowany,
> ale rodzi następujące pytania (gdyby ktoś znał albo umiał
> wymyślić na nie odpowiedzi, prosiłbym o ich tu przedstawienie):
> - czy jeżeli zawęzimy problem stopu tylko do programów, które
> nie odnoszą się do samych siebie, to czy wówczas staje
> się rozstrzygalny?
Jeśli procedura rozstrzygająca ma odpowiednio duży rozmiar względem
procedury rozstrzyganej, to oczywiście tak. Przy stałym lub jakoś
inaczej ograniczonym rozmiarze procedury rozstrzygającej - nie
słyszałem.


> czy może też istnieje jakiś argument,
> w którym nie używa się samoodnośnych programów, a z którego
> również wynika nierozwiązywalność problemu stopu?
Problem stopu jest ogólnie rozstrzygalny, ponieważ MT może udzielić
odpowiedzi czy program się zatrzyma czy nie.


> - czy istnieje jakaś systematyczna procedura rozpoznawania
> programów, które będą popadały w ów paradoks zatrzymywalności?


Pozdrawiam

do góry

On 27.09.2016 18:11, M.M. wrote:

>
> Jest to szczególny przypadek, bo program który rozstrzyga
> może mieć nieskończony rozmiar.

Nie może.


pzdr
bartekltg

do góry

On Tuesday, September 27, 2016 at 7:06:39 PM UTC+2, bartekltg wrote:
> On 27.09.2016 18:11, M.M. wrote:
>
> >
> > Jest to szczególny przypadek, bo program który rozstrzyga
> > może mieć nieskończony rozmiar.
>
> Nie może.

Dlaczego nie może? Taśma jest nieskończona, to zmieści się program o
nieskończonym rozmiarze, czyli może.

Pozdrawiam

do góry

W dniu 2016-09-27 19:16, M.M. pisze:
> On Tuesday, September 27, 2016 at 7:06:39 PM UTC+2, bartekltg wrote:
>> On 27.09.2016 18:11, M.M. wrote:
>>
>>>
>>> Jest to szczególny przypadek, bo program który rozstrzyga
>>> może mieć nieskończony rozmiar.
>>
>> Nie może.
>
> Dlaczego nie może? Taśma jest nieskończona, to zmieści się program o
> nieskończonym rozmiarze, czyli może.

Aż przypomniał mi się stary dowcip, że IBM stworzył dysk o nieskończonej
pojemności, pokazany będzie, jak tylko skończy się formatować.


--
Kaczus
http://kaczus.ppa.pl

do góry

On Wednesday, September 28, 2016 at 9:55:41 AM UTC+2, Tomasz Kaczanowski wrote:
> W dniu 2016-09-27 19:16, M.M. pisze:
> > On Tuesday, September 27, 2016 at 7:06:39 PM UTC+2, bartekltg wrote:
> >> On 27.09.2016 18:11, M.M. wrote:
> >>
> >>>
> >>> Jest to szczególny przypadek, bo program który rozstrzyga
> >>> może mieć nieskończony rozmiar.
> >>
> >> Nie może.
> >
> > Dlaczego nie może? Taśma jest nieskończona, to zmieści się program o
> > nieskończonym rozmiarze, czyli może.
>
> Aż przypomniał mi się stary dowcip, że IBM stworzył dysk o nieskończonej
> pojemności, pokazany będzie, jak tylko skończy się formatować.
>
Dowcip miły, ale mam nadzieję że nie użyłeś tego dowcipu
jako argumentu na nic, bo dowcip nie jest adekwatny do
naszej rozmowy. Dysk jest bytem fizycznym. Taśma maszyny
turinga jest bytem teoretycznym. Dwa zupełnie inne byty.
Na maszynie turinga zmieści się program o nieskończonym
rozmiarze, więc istnieje program który rozstrzyga problem
stopu dla każdego programu o skończonym rozmiarze.

do góry