Lenguajes internos

Cusco-c01

Para celebrar la publicación en línea de las notas de mi curso sobre las curvas de Shimura, para la escuela AGRA 2015 en Cusco, Perú, sobre aritmética, grupos, y análisis, he decidido escribir este post sobre los lenguajes internos en castellano.*  Si ahora vuelvo al asunto de lenguajes internos, ya considerado en algunas discusiones hace dos meses, es porque Mike Shulman ha publicado un “guest post” por Chris Kapulkin sobre exactamente esas cosas.  Para mí, las explicaciones de Kapulkin son más faciles que lo que he leido en la página “internal logic” de nLab, porque Kapulkin dice claramente lo que es conocido y lo que (todavía) no es.  También he apreciado su utilización de diagramas para indicar que la noción de lenguaje interno es relacionada (por lo menos conjeturalmente) con la construcción de un par de funtores adjuntos.

Lo más importante que he comprendido en el artículo de Kapulkin es que es imposible comprender el significado de la expresión lenguaje interno sin saber lo que es una teoría de tipos.  Hasta ahora la utilización de nociones de la teoría de tipos no ha sido necesario en mi trabajo en teoría de números; puedo afirmar que es más importante para mí aprender a escribir correctamente en castellano.  Pero naturalmente puede ser diferente en el futuro.

Sin embargo, me parece extraño, de un punto de vista puramente topográfico, de hablar de un lenguaje interno a una categoria cuando la representación de esta relación toma la forma de un diagrama donde el lenguaje es puesto al lado de su categoria.  No sería natural decir, por ejemplo, que el latino es el lenguaje interno del castellano, porque existe un diccionario que permite pasar del primero idioma al segundo.

*Google Translate™ is not a functor but it should allow those who don’t read Spanish to get the gist of this post.

Image file is licensed under the Creative Commons Attribution-Share Alike 2.5 Spain license.
Advertisements

4 thoughts on “Lenguajes internos

  1. Pingback: Math and Physics Summer Camps | Not Even Wrong

  2. Laurent

    Et bien dis donc ! Tout cela m’a l’air bien plus rigolo que les conférences à 5 exposés parallèles financées par la NSA. Les résultats des matchs devraient apparaître prochainement sur internet: nombre de personnes ayant participé à chaque exposé pour chaque poule de 5, je ne sais pas quand auront lieu les phases finales, probablement en Alaska, Salt Lake City étant trop facilement accessible (20h de porte à porte me concernant). Étant donné que les vidéos seront bientôt accessibles sur internet il faudra également comptabiliser les “like”. Au moins les locaux sud américains sont sûrement bien plus accueillants que ceux de Salt Lake City, mais peut-être s’agissait-il d’une manœuvre de l’AMS visant à convertir la communauté mathématique à la parole de Joseph Smith dans je ne sais quel but obscure (mais nul doute que la NSA est derrière cela).

    Like

    Reply
  3. jessemckeown

    Latine “ligua interna Castiliano” non mihi videtur esse: Alienus Castilianum solum considerans ut mores ratio Castiliani revelare non Latinam ipse repperirabit, puto. Possibile, Castiliano cum Latina una linguam internam communis habent…

    Like

    Reply
  4. Peter LeFanu Lumsdaine

    Även om jag bor nu i Stockholm, jag ska inte försöka att skriva den här kommentaren på svenska… Where you say:

    > “me parece extraño […] de hablar de un lenguaje interno a una categoria cuando la representación de esta relación toma la forma de un diagrama donde el lenguaje es puesto al lado de su categoria.”.

    I would quite agree: the fix is in the preposition. An internal language in the sense of categorical logic is meant to mean an internal language for a category, not a language internal to the category. It’s a language one can use to reason about things internal to the category; the language itself is indeed external.

    Like

    Reply

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s