Справочная информация :
Я заканчиваю магистратуру по математике и в августе начну работу над докторской диссертацией по логике. Чем больше логики я изучаю, тем больше теоретической информатики, с которой я сталкиваюсь, например, теория рекурсии, лямбда-исчисление, но лежащий в основе CS лежит под ковром. Мои основные области интересов - теория множеств и теория категорий - также имеют применение в информатике, но до сих пор я изучал их только с точки зрения чистой математики.
Проблема:
Отсутствие у меня знаний в области компьютерных наук иногда затрудняет понимание мотивации или интуиции, стоящей за тем, что происходит, или того, как это можно применить. Я справляюсь, но чувствую, что было бы полезнее немного расшириться ... мне приходит в голову, что в интересах моих будущих исследований я должен изучить некоторые компьютерные науки.
Большинство книг по CS, которые я просмотрел, были не очень подходящими для моих целей, потому что они были слишком простыми и нетехническими, или предполагали, что у меня нет опыта работы с CS. Похоже, они нацелены на людей, которые хорошо разбираются в компьютерах, но мало занимаются математическим образованием - моя ситуация противоположна.
Вопрос:
Какие есть книги или другие ресурсы, которые могли бы помочь математику, ставшему логиком, в достижении практических знаний (теоретической) информатики?
Я ищу что-то более полезное, чем несколько выступлений на семинарах и более глубокое, чем «Омнибус нового Тьюринга». , но у меня нет ни времени, ни ресурсов, чтобы получить еще одну степень бакалавра. (Может быть, я спрашиваю о том, чего не существует.)
Извините, если вопрос слишком расплывчатый или некорректный. Я чувствовал, что это было более подходящим здесь, чем на MSE, но я буду рад перенести его, если потребуется.
источник
Ответы:
По сути, вы запрашиваете ресурсы, которые позволят вам превратить имеющиеся у вас знания в области логики, теории рекурсии и теории категорий в знания о теоретической информатике. Я бы предложил взглянуть на теорию реализуемости, особенно через ее связи с теорией топосов и теорией категориальных доказательств. ,
Вот несколько предложений; Мой совет - выбрать один и углубиться. За исключением книги Тейлора (которая объясняет это), мои предположения предполагают, что вы подвергались достаточному воздействию лямбда-исчисления и теории категорий, чтобы увидеть категориальные интерпретации лямбда-исчисления простого типа.
Книга Пола Тейлора « Практические основы математики»
ИМО, это, вероятно, единственное лучшее техническое введение в отношения между логикой, теорией категорий и вычислениями. Он предполагает почти никаких предварительных условий, но очень быстро проникает в глубокие воды и обязательно облагает налогом (и значительно улучшает) вашу математическую зрелость.
Заметки Уэсли Фоа: введение в расслоения, теория топосов, эффективные топосы и скромные множества
Вот некоторые записи лекций, которые написал Уэсли Фоа. Если вы категорически свободно говорите, то эти заметки предлагают действительно быстрый путь к пониманию некоторых наиболее важных конструкций в теории реализуемости и теории топосов (а именно, к построению эффективных топосов).
Книга Барта Джейкобса « Категориальная логика и теория типов»
Это одна из окончательных ссылок на категориальную семантику теории типов. Это также очень большой.
В то же время, когда вы читаете одну из этих книг, я бы посоветовал скачать и научиться использовать язык программирования Agda. . Этот язык реализует сложные теории типов, описанные выше, и IMO невероятно полезно увидеть, как часто довольно тонкие семантические конструкции обмениваются в теории типов.
Андрей Бауэр, вероятно, может дать вам еще лучший совет. Возможно, его можно убедить опубликовать. :)
источник
Две книги, которые приходят на ум
Введение в теорию вычислений от Sipser
и
Введение в алгоритмы Cormen et al.
Я согласен с Усулом, который сказал, что теоретическая информатика - это широкая область, и мы могли бы дать более точные ссылки, если бы вы были более точными в том, что вы хотите изучить.
источник