Antecedentes :
Estoy llegando al final de mi maestría en matemáticas y comenzaré un doctorado en lógica en agosto. Mientras más lógica estudio, más informática teórica estoy expuesta, por ejemplo, teoría de la recursión, cálculo lambda, pero el CS subyacente está debajo de la alfombra. Mis principales áreas de interés, la teoría de conjuntos y la teoría de categorías, también tienen aplicaciones en informática, pero hasta ahora solo las he estudiado desde el punto de vista de las matemáticas puras.
Problema:
Mi falta de experiencia en informática a veces hace que sea difícil ver la motivación o la intuición detrás de lo que está sucediendo o cómo se podría aplicar. Me las arreglo, pero siento que sería más saludable diversificarse un poco ... se me ocurre que, en beneficio de mi investigación futura, debería aprender algo de informática.
La mayoría de los libros de CS que he visto no han sido muy adecuados para mis propósitos, ya que son demasiado básicos y poco técnicos, o presuponen el tipo de antecedentes de CS que no tengo. Parecen estar dirigidos a personas que saben bastante de informática pero que tienen pocos conocimientos matemáticos: mi situación es todo lo contrario.
Pregunta:
¿Qué libros u otros recursos hay que podrían ayudar a un matemático convertido en lógico en su objetivo de obtener un conocimiento práctico de la informática (teórica)?
Estoy buscando algo más saludable que unas pocas charlas en seminarios y más en profundidad que The New Turing Omnibus , pero no tengo el tiempo ni los recursos para hacer otro título universitario. (Puede ser que estoy pidiendo algo que no existe).
Lo siento si la pregunta es demasiado vaga o mal planteada. Sentí que era más adecuado aquí que en MSE, pero estaré encantado de migrarlo si es necesario.
fuente
Respuestas:
Básicamente, está solicitando recursos que le permitan convertir su conocimiento existente de lógica, teoría de la recursión y teoría de la categoría en conocimiento sobre informática teórica. Sugeriría mirar la teoría de la realizabilidad, especialmente a través de sus conexiones con la teoría de topos y la teoría de prueba categórica .
Aquí hay un puñado de sugerencias; Mi consejo es elegir uno y profundizar. Con la excepción del libro de Taylor (que explica esto), mis sugerencias asumen que has estado expuesto a suficiente cálculo lambda y teoría de categorías para haber visto interpretaciones categóricas del cálculo lambda de tipo simple.
El libro de Paul Taylor Fundamentos prácticos de las matemáticas
En mi opinión, esta es probablemente la mejor introducción técnica a la relación entre lógica, teoría de categorías y computación. Casi no supone requisitos previos, pero se mete en aguas bastante profundas muy rápidamente y seguramente gravará (y mejorará) su madurez matemática.
Notas de Wesley Phoa Introducción a las fibras, teoría de topos, topos efectivos y conjuntos modestos
Estas son algunas notas de clase que Wesley Phoa escribió. Si es categóricamente fluido, estas notas ofrecen un camino realmente rápido para comprender algunas de las construcciones más importantes en la realizabilidad y la teoría de topos (es decir, la construcción de topos efectivos).
Libro de Bart Jacobs Lógica categórica y teoría de tipos
Esta es una de las referencias definitivas sobre la semántica categórica de la teoría de tipos. También es muy grande.
Al mismo tiempo que está leyendo uno de estos libros, le aconsejo que descargue y aprenda a usar el lenguaje de programación Agda . Este lenguaje implementa las sofisticadas teorías de tipos descritas anteriormente, y en mi opinión, es increíblemente útil ver cómo las construcciones semánticas, a menudo bastante sutiles, se liquidan en la teoría de tipos.
Andrej Bauer probablemente pueda darte mejores consejos. Quizás pueda ser persuadido para publicar. :)
fuente
Los dos libros que vienen a la mente son
Introducción a la teoría de la computación por Sipser
y
Introducción a los algoritmos por Cormen et al.
Estoy de acuerdo con usul, quien dijo que la informática teórica es un área amplia y que podríamos darle mejores referencias si fuera más específico sobre lo que quiere aprender.
fuente