Weg zu formalen Methoden

Es ist nicht ungewöhnlich, dass Studenten ihre Doktorarbeit mit nur begrenztem Hintergrund in Mathematik und den formalen Aspekten der Informatik beginnen. Offensichtlich wird es für solche Studenten sehr schwierig sein, theoretische Informatiker zu werden, aber es wäre gut, wenn sie es verstehen könnten, formale Methoden anzuwenden und Papiere zu lesen, die formale Methoden enthalten.

Was ist ein guter kurzfristiger Weg für Doktoranden, um die nötige Erfahrung zu sammeln, um sie dazu zu bringen, Artikel mit formalen Methoden zu lesen und schließlich Artikel zu schreiben, die solche formalen Methoden verwenden?

Im Kontext denke ich eher an Theorie B und formale Verifikation als an die Dinge, die sie lernen sollten, aber auch an klassische TCS-Themen wie die Automatentheorie.

George Pólya schreibt im Vorwort seines Buches „Mathematische Entdeckung - Probleme lösen, verstehen, lernen und lehren“:

Das Lösen von Problemen ist eine praktische Kunst wie Schwimmen, Skifahren oder Klavierspielen: Man kann lernen, dass es nur Nachahmung und Übung ist. Dieses Buch kann Ihnen keinen magischen Schlüssel bieten, der alle Türen öffnet und alle Probleme löst, aber es bietet Ihnen gute Beispiele für Nachahmung und viele Gelegenheiten zum Üben: Wenn Sie schwimmen lernen möchten, müssen Sie ins Wasser gehen und wenn Sie Wenn Sie ein Problemlöser werden möchten, müssen Sie Probleme lösen.

Ich denke, es gibt keinen kurzen Weg, vor allem, um den Stand des Schreibens von Papieren zu erreichen. Es erfordert viel Übung.

Einige Hinweise:

Wenn „limited Hintergrund in Mathematik und die formalen Aspekte“ Mittel „hat noch nie einen Beweis erdacht und geschrieben down“ dann so etwas wie dies könnte ein Anfang sein.

Wenn sich der Schüler auf dem Spickzettel für Theoretische Informatik unwohl fühlt, ist ein Auffrischungskurs des entsprechenden Fachs der Mathematik ratsam.

Es gibt viele Quellen für mathematisches Schreiben: Die Vorlesungsunterlagen des Kurses CS209 der Stanford University von 1978 vielleicht. Oder dieser Artikel von Paul Halmos.

Formale Methoden wie Z, B, TLA und CafeObj stützen sich stark auf Mengenlehre, Logik, Kategorietheorie, Lambda-Berechnung und Automaten, um die Konzepte von Typen, Daten und Berechnungen zu modellieren.

Sie können entweder in eine umfassende Monographie wie Logics of Specification Languages ​​von Dines Bjørner und Martin C. Henson (Hrsg.), Monographs in Theoretical Computer Science, Springer Verlag, 2008, springen und daraus lernen und die dort zitierten Referenzen verwenden. Oder lernen Sie jeweils ein Thema:

1. Mengenlehre
2. Mathematische Logik
3. Zeitliche Logik
4. Universalalgebra
5. Lambda-Kalkül
6. Kategorietheorie

Ich denke wirklich, dass "formale" Methoden keine sehr gute Idee für Bildungszwecke sind. In diesem Fall ist die Programmierung eines Computers eine "formale" Methode. Gelingt es als pädagogisches Instrument?

Was benötigt wird, ist Verständnis, Intuition und die Fähigkeit, mit Abstraktion umzugehen. Formale Methoden behindern das alles. Sie fördern vielmehr Versuch und Irrtum, Hacking, Pattern Matching, Imitation und konzentrieren sich auf die Syntax. Die Liste geht weiter und weiter.

Jedes Stück rigoroser Mathematik bringt den Menschen bei, wie man richtig argumentiert. Je einfacher die Domain, desto besser ist sie. Alles, was ich über das Denken gelernt habe, habe ich in der High School gelernt, als ich ernsthaft Euklidische Geometrie gemacht habe. Analysis und lineare Algebra an der Universität erledigten den Rest.

Eine andere attraktive Alternative ist die philosophische Logik, bei der die Menschen lernen, über Aussagen nachzudenken und zu verstehen, was der Informationsgehalt ist und was eine Folge von was ist. Sie tun dies, ohne die Schüler in Symbolen zu ertränken.

Wenn Sie eine Bestandsaufnahme aller Top-Informatiker machen, werden Sie erstaunt sein, wie viele von ihnen eine formale Ausbildung in Philosophie haben. All das verlieren wir jetzt, weil die Studenten der Philosophie Informatik jetzt als ein alltägliches Fach betrachten. Unsere Schüler dazu zu bringen, etwas Philosophie zu lernen, könnte dem in gewissem Maße entgegenwirken. Lassen Sie sie Bertrand Russells Geschichte der westlichen Philosophie durcharbeiten . Das wird Wunder wirken.

Wenn sie in der Theorie der Programmiersprache arbeiten, können Sie sie auch Quine lesen lassen, den ich als den "Gottvater" der denotationalen Semantik betrachte. (Quine hat im Wesentlichen die Denotationssemantik der natürlichen Sprache in Word und Object durchgeführt , was eine große Inspirationsquelle für Christopher Strachey war. Aber dieses Buch ist ziemlich anstrengend.) Die bearbeitete Sammlung Quintessence ist eine schöne Quelle für Quines Ideen für Anfänger.

[Anmerkung hinzugefügt: Ein Vorteil der Philosophie gegenüber der Mathematik besteht darin, dass die Schüler die Debatte sehen , dh sie können das "richtige" Argument und das "falsche" Argument sehen und sehen, wie die Experten die falschen abreißen. In der Mathematik sieht man nie ein falsches Argument, das den pädagogischen Wert einschränkt.]