Ressourcen für Mathematiker, die mehr Informatik lernen möchten

Hintergrund :

Ich beende mein Masterstudium in Mathematik und werde im August in Logik promovieren. Je mehr Logik ich studiere, desto mehr theoretische Informatik ist mir ausgesetzt, z. B. Rekursionstheorie, Lambda-Kalkül, aber die zugrunde liegende CS wird unter den Teppich gekehrt. Meine Hauptinteressengebiete - Mengen- und Kategorietheorie - haben auch Anwendungen in der Informatik, aber ich habe sie bisher nur unter dem Gesichtspunkt der reinen Mathematik studiert.

Problem:

Mein Mangel an Informatikhintergrund macht es manchmal schwierig, die Motivation oder Intuition dahinter zu sehen, was vor sich geht oder wie es angewendet werden könnte. Ich komme zurecht, aber ich denke, es wäre gesünder, ein bisschen zu verzweigen. Mir fällt ein, dass ich zum Nutzen meiner zukünftigen Forschung etwas Informatik lernen sollte.

Die meisten CS-Bücher, die ich angeschaut habe, waren für meine Zwecke nicht sehr geeignet, da sie entweder zu einfach und untechnisch waren oder die Art von CS-Hintergrund voraussetzten, die ich nicht habe. Sie scheinen sich an Menschen zu richten, die sich gut mit Computern auskennen, aber wenig mit mathematischen Hintergründen zu tun haben - in meiner Situation ist das Gegenteil der Fall.

Frage:

Welche Bücher oder sonstigen Ressourcen könnten einem Mathematiker, der zum Logiker wird, dabei helfen, sich Kenntnisse in (theoretischen) Informatik anzueignen?

Ich suche etwas Gesünderes als ein paar Seminarvorträge und etwas Ausführlicheres als The New Turing Omnibus , aber ich habe weder die Zeit noch die Ressourcen, um einen anderen Bachelor-Abschluss zu machen. (Es kann sein, dass ich nach etwas frage, das es nicht gibt.)

Tut mir leid, wenn die Frage zu vage oder schlecht gestellt ist. Ich fand es hier passender als auf MSE, aber ich werde es gerne migrieren, wenn es sein muss.

Sie fragen im Wesentlichen nach Ressourcen, mit denen Sie Ihr vorhandenes Wissen über Logik, Rekursionstheorie und Kategorietheorie in Wissen über theoretische Informatik umwandeln können. Ich würde vorschlagen, die Realisierbarkeitstheorie zu betrachten, insbesondere über ihre Verbindungen zur Topos-Theorie und zur kategorialen Beweistheorie .

Hier sind einige Vorschläge; Mein Rat ist, einen auszuwählen und in die Tiefe zu gehen. Mit Ausnahme von Taylors Buch (das dies erklärt) gehen meine Vorschläge davon aus, dass Sie genügend Lambda-Kalkül und Kategorietheorie ausgesetzt waren, um kategoriale Interpretationen des einfach typisierten Lambda-Kalküls zu sehen.

• Paul Taylors Buch Praktische Grundlagen der Mathematik

  IMO, dies ist wahrscheinlich die beste technische Einführung in die Beziehung zwischen Logik, Kategorietheorie und Berechnung. Es setzt fast keine Voraussetzungen voraus, gerät jedoch sehr schnell in tiefe Gewässer und wird Ihre mathematische Reife mit Sicherheit belasten (und erheblich verbessern).

• Wesley Phoas Notizen Eine Einführung in die Fibrationen, die Topos-Theorie, die effektiven Topos und die bescheidenen Mengen

  Dies sind einige Vorlesungsunterlagen, die Wesley Phoa verfasst hat. Wenn Sie kategorisch fließend sind, bieten diese Notizen einen sehr schnellen Weg, um einige der wichtigsten Konstruktionen der Realisierbarkeits- und Topos-Theorie (nämlich die Konstruktion der effektiven Topos) zu verstehen.

• Bart Jacobs 'Buch Kategoriale Logik und Typentheorie

  Dies ist eine der maßgeblichen Referenzen zur kategorialen Semantik der Typentheorie. Es ist auch sehr groß.

Während Sie eines dieser Bücher lesen, empfehle ich Ihnen, die Programmiersprache Agda herunterzuladen und zu lernen . Diese Sprache implementiert die oben beschriebenen hoch entwickelten Typentheorien, und es ist unglaublich hilfreich zu sehen, wie sich die oft recht subtilen semantischen Konstruktionen in der Typentheorie niederschlagen.

Andrej Bauer kann Sie wahrscheinlich noch besser beraten. Vielleicht kann man ihn zum Posten überreden. :)

Die beiden Bücher, die mir in den Sinn kommen, sind

Einführung in die Berechnungstheorie von Sipser

und

Einführung in Algorithmen von Cormen et al.

Ich stimme mit Usul überein, der sagte, dass die theoretische Informatik ein weites Feld ist und wir bessere Referenzen geben könnten, wenn Sie genauer wissen würden, was Sie lernen möchten.