Contexte :
J'arrive à la fin de ma maîtrise en mathématiques et commencerai un doctorat en logique en août. Plus j'étudie la logique, plus l'informatique est théorique à laquelle je suis exposé, par exemple la théorie de la récursivité, le calcul lambda, mais le CS sous-jacent est effleuré sous le tapis. Mes principaux domaines d'intérêt - la théorie des ensembles et la théorie des catégories - ont également des applications en informatique, mais jusqu'à présent, je ne les ai étudiées que du point de vue des mathématiques pures.
Problème:
Mon manque de formation en informatique rend parfois difficile de voir la motivation ou l'intuition derrière ce qui se passe, ou comment cela pourrait être appliqué. Je m'en sors, mais j'ai l'impression qu'il serait plus sain de se ramifier un peu ... il me semble que, pour le bénéfice de mes recherches futures, je devrais apprendre l'informatique.
La plupart des livres CS que j'ai consultés n'étaient pas très adaptés à mes besoins, soit trop basiques et non techniques, soit présupposant le type de contexte CS que je n'ai pas. Ils semblent s'adresser à des gens qui sont assez avertis en informatique mais qui ont peu de connaissances en mathématiques - ma situation est le contraire.
Question:
Quels livres ou autres ressources existe-t-il qui pourraient aider un mathématicien devenu logicien dans son objectif d'acquérir une connaissance pratique de l'informatique (théorique)?
Je recherche quelque chose de plus sain que quelques conférences de séminaire et plus approfondi que The New Turing Omnibus , mais je n'ai pas le temps ni les ressources pour faire un autre diplôme de premier cycle. (Il se peut que je demande quelque chose qui n'existe pas.)
Désolé si la question est trop vague ou mal posée. Je pensais que c'était plus approprié ici que sur MSE mais je serai heureux de le migrer si besoin est.
la source
Réponses:
Vous recherchez essentiellement des ressources qui vous permettront de transformer vos connaissances existantes de la logique, de la théorie de la récursivité et de la théorie des catégories en connaissances sur l'informatique théorique. .
Voici quelques suggestions; mon conseil est d'en choisir un et d'aller en profondeur. À l'exception du livre de Taylor (qui explique cela), mes suggestions supposent que vous avez été exposé à suffisamment de calcul lambda et de théorie des catégories pour avoir vu des interprétations catégoriques du calcul lambda simplement tapé.
Le livre de Paul Taylor Practical Foundations of Mathematics
OMI, c'est probablement la meilleure introduction technique à la relation entre la logique, la théorie des catégories et le calcul. Il ne suppose presque pas de pré-requis, mais il pénètre très rapidement dans les eaux assez profondes et il est sûr de taxer (et d'améliorer considérablement) votre maturité mathématique.
Les notes de Wesley Phoa Une introduction aux fibres, à la théorie des topos, aux topos efficaces et aux ensembles modestes
Voici quelques notes de cours que Wesley Phoa a rédigées. Si vous êtes catégoriquement fluide, ces notes offrent un moyen très rapide de comprendre certaines des constructions les plus importantes de la réalisabilité et de la théorie des topos (à savoir, la construction des topos efficaces).
Livre de Bart Jacobs Logique catégorique et théorie des types
C'est l'une des références définitives sur la sémantique catégorique de la théorie des types. Il est également très grand.
En même temps que vous lisez l'un de ces livres, je vous conseille de télécharger et d'apprendre à utiliser le langage de programmation Agda . Ce langage implémente les théories de type sophistiquées décrites ci-dessus, et à l'OMI, il est incroyablement utile de voir comment les constructions sémantiques souvent assez subtiles se concrétisent dans la théorie des types.
Andrej Bauer peut probablement vous donner de meilleurs conseils. Peut-être peut-on le persuader de poster. :)
la source
Les deux livres qui me viennent à l’esprit sont
Introduction à la théorie du calcul par Sipser
et
Introduction aux algorithmes par Cormen et al.
Je suis d'accord avec l'usul qui a dit que l'informatique théorique est un vaste domaine et nous pourrions donner de meilleures références si vous étiez plus précis sur ce que vous voulez apprendre.
la source