Materiały dla matematyków chcących dowiedzieć się więcej informatyki

tło :

Kończę studia magisterskie z matematyki i rozpocznę doktorat z logiki w sierpniu. Im więcej logiki studiuję, tym bardziej teoretyczna jest informatyka, np. Teoria rekurencji, rachunek lambda, ale leżące u podstaw CS jest szczotkowane pod dywan. Moje główne obszary zainteresowań - teoria zbiorów i teoria kategorii - mają również zastosowania w informatyce, ale do tej pory studiowałem je tylko z punktu widzenia czystej matematyki.

Problem:

Brak jakiegokolwiek zaplecza informatycznego utrudnia czasem dostrzeżenie motywacji lub intuicji stojących za tym, co się dzieje, lub tego, jak można to zastosować. Radzę sobie, ale wydaje mi się, że zdrowiej byłoby trochę rozgałęzić się ... przychodzi mi do głowy, że z korzyścią dla moich przyszłych badań powinnam nauczyć się informatyki.

Większość książek o CS, na które patrzyłem, nie była zbyt odpowiednia do moich celów, ponieważ była zbyt podstawowa i nietechniczna lub zakładała rodzaj CS, którego nie mam. Wydaje się, że są skierowane do osób, które są dość obeznane z komputerem, ale mają niewielkie przeszkody w matematyce - moja sytuacja jest odwrotna.

Pytanie:

Jakie są książki lub inne zasoby, które mogłyby pomóc matematykowi, który został logikiem, w dążeniu do zdobycia praktycznej wiedzy z zakresu (teoretycznej) informatyki?

Szukam czegoś zdrowszego niż kilka wykładów seminaryjnych i bardziej dogłębnego niż The New Turing Omnibus , ale nie mam czasu ani zasobów, aby zrobić kolejny stopień licencjacki. (Być może proszę o coś, co nie istnieje).

Przepraszam, jeśli pytanie jest zbyt niejasne lub źle postawione. Czułem, że jest bardziej odpowiedni tutaj niż na MSE, ale chętnie przeprowadzę migrację, jeśli zajdzie taka potrzeba.

Zasadniczo prosisz o zasoby, które pozwolą ci przekształcić dotychczasową wiedzę z logiki, teorii rekurencji i teorii kategorii w wiedzę o teoretycznej informatyce. Sugerowałbym przyjrzenie się teorii wykonalności, szczególnie poprzez jej powiązania z teorią toposu i teorią dowodu kategorycznego .

Oto garść sugestii; moja rada to wybrać jedną i wejść w głąb. Z wyjątkiem książki Taylora (która to wyjaśnia), moje sugestie zakładają, że byłeś wystarczająco obciążony rachunkiem lambda i teorią kategorii, aby zobaczyć kategoryczne interpretacje rachunku lambda po prostu.

• Książka Paula Taylora Praktyczne podstawy matematyki

  IMO, to prawdopodobnie najlepsze techniczne wprowadzenie do relacji między logiką, teorią kategorii i obliczeniami. Nie zakłada prawie żadnych warunków wstępnych, ale bardzo szybko wchodzi w dość głębokie wody i z pewnością opodatkuje (i znacznie poprawi) matematyczną dojrzałość.

• Notatki Wesleya Phoa Wprowadzenie do fibracji, teorii toposów, skutecznych toposów i skromnych zestawów

  Oto kilka notatek z wykładów, które napisał Wesley Phoa. Jeśli jesteś biegły w kategoriach, te notatki oferują naprawdę szybką ścieżkę do zrozumienia niektórych najważniejszych konstrukcji w zakresie wykonalności i teorii toposu (a mianowicie konstrukcji skutecznych toposów).

• Książka Barta Jacobsa Categorical Logic and Type Theory

  Jest to jedno z ostatecznych odniesień do kategorycznej semantyki teorii typów. Jest również bardzo duży.

W tym samym czasie, gdy czytasz jedną z tych książek, radzę pobrać i dowiedzieć się, jak korzystać z języka programowania Agda . Ten język implementuje wyrafinowane teorie typów opisane powyżej, a IMO jest niezwykle pomocne, aby zobaczyć, jak często dość subtelne konstrukcje semantyczne opierają się na teorii typów.

Andrej Bauer prawdopodobnie udzieli jeszcze lepszych porad. Być może uda się go przekonać do opublikowania. :)

Dwie książki, które przychodzą na myśl, to:

Wprowadzenie do teorii obliczeń Sipsera

i

Wprowadzenie do algorytmów Cormena i in.

Zgadzam się z usulem, który powiedział, że informatyka teoretyczna jest szerokim obszarem i moglibyśmy podać lepsze referencje, gdybyś był bardziej szczegółowy na temat tego, czego chcesz się nauczyć.