Jak zestrzelić swoje dowody

59

Jakie są ogólne wytyczne dotyczące sprawdzania twoich dowodów? Uważam, że jest to ważne dla absolwentów takich jak ja. Wiem już, co musimy zrobić, aby coś udowodnić, ale zawsze musisz wszystko sprawdzić przed wysłaniem. Nawet do twojego własnego doradcy.

Opracowałem sobie strategie metodą prób i błędów i otrzymałem wiele porad od mojego doradcy. Ale to zawsze jest bardzo żmudna praca. Zwykle, kiedy coś skończysz, po prostu chcesz przejść do następnego problemu, ale nadal musisz trzymać się bieżącego problemu, dopóki wszystko nie będzie idealne. Oto przykład mojej własnej listy sztuczek:

  1. Podaj szczegóły. Wiele błędów jest w miejscach, w których piszesz „jasne jest, że ...”, „bez utraty ogólności ...” itp.
  2. Wypróbuj kilka liczb. Spróbuj ekstremalnych przypadków, takich jak „co się stanie, gdy ustawię lub ”.n=1n=1000
  3. Zachowaj czysty notatnik. Pisz o tym na co dzień i porównuj z szorstkimi notatkami. Próbuję pisać także w lateksie, w ten sposób znalazłem wiele błędów.

Jakie są ogólne strategie stosowane do sprawdzania dowodów?

Celem tego pytania jest uczynienie z niego wiki społeczności.

Marcos Villagra
źródło
Jeśli pytanie wydaje się subiektywne, pomóż mi je poprawić.
Marcos Villagra
jak zrobić to wiki społeczności?
Marcos Villagra
1
Hej, spoko! Naprawdę interesują mnie odpowiedzi na to pytanie. Mogę też docenić twoje # 3. (Kiedy się nad tym zastanawiam, właściwie wszędzie mam stosy papieru rozrzucone wszędzie, gdy intensywnie pracuję nad problemem, który następnie zostaje losowo przeniesiony. Fuj.) Wcześniej popełniłem błąd z tego samego problemu i skończyłem na marnowaniu spory kawałek czasu.
Daniel Apon
@Daniel: Miałem ten sam problem !! Dlatego po skończeniu dowodu od razu piszę wersję lateksową. Dobrze wiedzieć, że nie jestem jedynym nieuporządkowanym facetem, który trzyma wszystko wszędzie :-)
Marcos Villagra
1
oflagujesz go dla uwagi moderatora.
Suresh Venkat

Odpowiedzi:

39

Inżynierowie oprogramowania mają pojęcie, które nazywają „ zapachami kodu ”. Są to objawy w kodzie, które mogą wskazywać na głębszy problem. Inżynierowie oprogramowania zbierają mentalne listy zapachów, o których należy pamiętać (tj. Zbyt długie metody lub zbyt wiele parametrów). Nie musi to oznaczać, że występuje problem, ale po prostu wskazać, że pisarz może chcieć sprawdzić dwukrotnie.

Proponuję, abyśmy również wzięli pod uwagę „nieprzyjemne zapachy” . To nie da ci algorytmu do sprawdzania twoich dowodów, ale daje język i metaforę do rozpoznawania możliwych problemów w dowodach. Kilka przykładów zapachów pachnie:

  1. Przysłówki „wyraźnie”, „oczywiście” itp.
  2. Odniesienie do dowodu poprzedniego wyniku zamiast odniesienia do samego wyniku.
  3. Niekorzystne wykorzystanie wyniku z wieloma warunkami technicznymi.

Są też bardziej subtelne zapachy. Na przykład, jeśli dowód używa twierdzenia dwumianowego do rozwinięcia wyrażenia, a następnie używa twierdzenia dwumianowego, aby powrócić do formy zamkniętej, być może istnieje bezpośrednia manipulacja formą zamkniętą, która daje ten sam wynik.

Moja sugestia to zebranie (mentalnej lub pisemnej) listy takich zapachów i sprawdzanie ich podczas czytania. Przyjemnym efektem ubocznym tego podejścia jest to, że uczyni cię lepszym czytelnikiem.

Uwaga: Moją nadzieją w tej odpowiedzi było udzielenie intuicyjnej strony rygorystycznej odpowiedzi dostarczonej przez Lamporta Jak napisać dowód wymieniony w odpowiedzi M. Alaggana.

Don Sheehy
źródło
4
Mówię to cały czas moim studentom i myślą, że jestem szalony. Oczywiście twierdzę, że wyczuwam błąd, który może być częścią problemu;)
Suresh Venkat
7
@Suresh: Ten uczeń uważa, że ​​jesteś szalony z różnych powodów. ;-)
John Moeller
4
W notatce zapachu kodu rzeczy, które zawsze staram się zbadać w dowodach innych, obejmują łańcuch nierówności. Często naprawdę podstawowe błędy mają zwyczaj wkradać się do trudniejszych pochodnych.
John Moeller
23

Jest bardzo dobra praca Leslie Lamporta ( Jak napisać dowód ). W rzeczywistości jest to jego propozycja dotycząca stylu pisania szczegółowych dowodów w taki sposób, aby:

(1) Umożliwia wykrywanie błędów w prosty sposób

(2) Wyjaśnia, które założenia i twierdzenia zastosowano w poszczególnych częściach, co sprawia, że ​​dość łatwo jest zobaczyć, co się stanie, jeśli chcesz (na przykład) zastosować słabsze założenia

Istnieje również pewne doświadczenie społeczności i inspirujący komentarz do tej techniki na temat MO, który pokazuje ogólnie pozytywne doświadczenia (i niektóre inne zasoby).

Aktualizacja: dostępna jest nowa wersja Jak napisać dowód XXI wieku .

M. Alaggan
źródło
5
Dowody te są bardzo podobne do tego, co napisano by w pracy badawczej PL. Łańcuch logiki jest bardzo wyraźny. Po nauczeniu się, jak czytać i doceniać dowody w stylu PL, trudno mi było zrozumieć „normalne” dowody matematyczne. Takie dowody często wymagają, aby czytelnik myślał w taki sam sposób, jak autor, a kiedy przyzwyczaiłeś się do innego stylu dowodu, po prostu tak nie jest (przynajmniej dla mnie!)
Christopher Monsanto
2
@Christopher Monsanto: PL oznacza języki programowania? Byłbym wdzięczny, gdyby można podać taki przykład (jeden taki artykuł) do sprawdzenia :)
M. Alaggan
5
Zawsze miałem wrażenie, że to, co sugeruje Lamport, nie jest zgodne z „ Lamentem matematyka” Paula Lockharta ( maa.org/devlin/LockhartsLament.pdf ).
Marcos Villagra
14

Wydaje mi się, że pamiętam dawno temu popularne opowiadanie o tym, jak fizycy radzą sobie z analogicznym problemem. Kto wie, jak dokładna jest jego następująca wersja; poprawki są mile widziane. Uważam jednak, że podstawowa strategia jest dość niezwykła.

Wyjaśnili, jak uwierzyli w czarne dziury. Czarne dziury były początkowo konstrukcjami czysto matematycznymi, podobnie jak inne dziwne obiekty w fizyce, takie jak tunele czasoprzestrzenne. Ich strategia była uderzająca: matematycznie rzucali innymi przedmiotami w badany obiekt. Tunele czasoprzestrzenne nie przeszły pomyślnie testów, ponieważ odkryli, że tunel czasoprzestrzenny zapadnie się nawet w obecności normalnego obiektu fizycznego, może asteroidy. Ale czarne dziury przeszły ten test: czarna dziura przetrwałaby po rzuceniu w nią asteroidą. Próbowali więc rzucić w to gwiazdą. Ten sam wynik. W końcu rzucili kolejną czarną dziurę w czarną dziurę i ta przetrwała. W rezultacie nabrali wystarczającej pewności w istnieniu czarnych dziur, aby faktycznie zacząć ich szukać w prawdziwym wszechświecie.

Tak więc stosowność i zastosowanie powyższej strategii polega na tym, aby zacząć rzucać rzeczami na swój dowód. Czy przetrwa kontrolę poczytalności ? Jeśli usuniesz niezbędne założenie, to czy ono się zawali, jak powinno? Czy zwija się tak, jak powinien, gdy jest stosowany do spraw poza jego zakresem? Czy wytrzymuje rozsądne uogólnienia i specjalizacje? Spójrz na listę heurystyk w artykule Polya How to Solve . Spróbuj zmutować swój dowód za pomocą tych heurystyk i sprawdź, czy stoi i spada tak, jak powinien.

Nieśmiała osoba
źródło
Większość odpowiedzi skupia się na sprawdzeniu dowodów, weryfikując, czy stają się one fałszywe w sytuacjach, w których powinny być fałszywe. To nie działa, ponieważ nie sprawdza, czy twierdzenie było prawdziwe tam, gdzie miało być prawdziwe! Załóżmy na przykład, że „udowodniłem”, że każda liczba nieparzysta jest podzielna przez trzy. Sprawdzam, czy mój dowód zawodzi, jeśli rozciągam się również na liczby parzyste: tak, ponieważ czterech nie można podzielić przez trzy. Brawo, mój dowód musi być poprawny!
David Richerby
12

Myślę, że jednym z najbezpieczniejszych sposobów jest opracowanie wielu niezależnych dowodów. Dzięki temu możesz mieć pewność, że główny wynik jest prawidłowy, nawet jeśli popełnisz błąd w niektórych szczegółach dowodu.

Jukka Suomela
źródło
9

Jedną z technik, które uważam za przydatne, jest zastanowienie się, jakie inne wyniki byłaby w stanie udowodnić strategia dowodu. Jeśli z łatwością mogę dostosować strategię dowodu, aby udowodnić duży otwarty problem lub nawet problem, który nie jest otwarty, ale który ma zbyt skomplikowane rozwiązanie w porównaniu ze złożonością strategii sprawdzania, to jest to duży powód do wątpliwości dowód.

Optować
źródło
5
Dałbym to +10, gdybym mógł - szczególnie w teorii złożoności często można wykazać błędne techniki dowodowe, aby udowodnić naprawdę silne stwierdzenia, takie jak , a następnie bardzo łatwo zgadnąć, że twoja technika dowodowa jest błędna. Zwłaszcza jeśli twoja technika dowodu relatywizuje się! PNP
Joshua Grochow
6

Zawsze sprawdzam ponownie swoje dowody za pomocą narzędzia sprawdzającego, takiego jak COQ lub ISABELLE . Jeśli możesz udowodnić swój dowód w dowolnym z tych języków programowania, możesz być pewien, że jest on poprawny. Tak prosty jak termin lambda;).

Gopi
źródło
Nigdy nie korzystałem z Coq, ale powinienem spróbować. W rzeczywistości próbuję udowodnić pewne dolne granice matematyki, ale nie znalazłem właściwej drogi. Może potrzebuję specjalnych pakietów lub czegoś takiego.
Marcos Villagra
1
Być może jest to długi cel, ale jeśli chcesz udowodnić pewne dolne granice za pomocą reals, możesz sprawdzić te biblioteki: coqtail.sourceforge.net/?home/en
Gopi
Uzgodnione, ale każdy język programowania działa. Najczęściej robię to w odwrotnej kolejności. Sformułuj domenę problemową w języku programowania (zwykle Ruby), a następnie użyj tego jako szablonu dla mojego dowodu.
Chad Brewbaker