Suscríbete a RCast en iTunes | Google Play | Grapadora
Christian Williams habla sobre su reciente viaje para estudiar con Marcelo Fiore con Greg Meredith e Isaac DeFrain.
cristiano: Acabo de regresar de un largo viaje por Europa donde asistía a una escuela de verano y conferencias. La mejor parte fue visitar a un profesor en Cambridge llamado Marcelo Fiore. Lo pasamos muy bien comenzando proyectos potenciales juntos y principalmente aprendí de él. Lleva más de dos décadas trabajando en un gran proyecto que ahora se llama Sintaxis abstracta; también se podría llamar teoría del tipo algebraico. De alguna manera, es una gran "teoría de las teorías", pero se podría decir con mayor precisión que está tratando de dar los fundamentos algebraicos de los lenguajes formales.
La idea básica es que una teoría algebraica tradicional, de la que hemos hablado en el pasado en los podcasts de RChain, por ejemplo, la teoría de un monoide. Existe esta buena idea en la teoría de categorías en la que podemos abstraer nociones algebraicas asociadas con conjuntos. Podemos decir, todo lo que realmente queremos decir con, donde antes diríamos que un monoide es un conjunto equipado con la operación binaria y una identidad tal que es asociativa e inmutable, la teoría de categorías nos permite reconocer cuando tenemos estructuras híbridas. Tenemos algún objeto en la categoría que tiene una operación binaria y una identidad tal que es asociativa. Podría tener algo que sea un espacio, que también tenga algún tipo de estructura algebraica.
Esto es muy útil para muchos propósitos. Le permite utilizar esta filosofía llamada internalización. Puedes ver alguna definición complicada y luego te das cuenta de que es solo un espacio en blanco. Es un monoide interno para "gato" o algo así. Hay una limitación básica para estas teorías. Idealmente, queremos dar estructura algebraica a los lenguajes de programación. En particular, el cálculo del proceso que vamos a utilizar en RChain.
Tal como están las cosas, no se puede escribir una teoría del cálculo Rho o una teoría del cálculo Pi, en este sentido de teoría. Este tipo de categorías carecen de una noción de enlace variable. Cuando escribe, por ejemplo, la entrada. La operación de entrada en el cálculo Rho es la que une una variable. Cuando dices 4 y luego X flecha A, estás escuchando en el canal A y recibes algo que vas a llamar X. Luego, en la continuación P, vas a hacer algo con esa X. El punto es esa X en tu notación es solo un marcador de posición. Solo tiene un significado relativo a esta expresión.
La reducción básica de reescritura del cálculo Rho (o el cálculo Pi) es una sustitución en una entrada. Si está ingresando en el canal A y, en paralelo, alguien está enviando en el canal A, en el cálculo de Rho, estas serían citas de procesos, entonces los datos, el proceso que se envía en el canal A, se comunican y se sustituido por esa variable ligada distinguida X. La continuación comienza con lo que fue sustituido.
Eso es lo sutil que no puedes expresar con álgebra normal. Hay un problema similar en el cálculo de Lambda, en los fundamentos de la programación funcional normal. Cuando escribe Lambda X dot X plus X, desea aplicarlo a 2, va a sustituir el 2 y la X y obtendrá 2 más 2. La idea es que una operación que une una variable de esta manera y hace que este distinguido marcador de posición que pretendes sustituir, ese sea un tipo diferente de operación en cualquiera de estos.
Hace unos 20 años, Marcello Fiore y Gordon Plotkin y Danielle Turi escribieron este documento llamado "Sintaxis abstracta con enlace variable". Esencialmente resuelve este problema. Eleva el álgebra normal de las categorías normales llamadas teorías de Lawvere a las categorías de functor. Al igual que la categoría de functores (y las transformaciones naturales entre ellos), cuando arreglas dos categorías, esto contiene una gran cantidad de estructura realmente rica en la que puedes hacer todo el álgebra normal que hiciste antes, pero eres capaz de expresar un muchas cosas que no podías antes.
Eso es lo que vine a Cambridge para aprender de él. He aprendido mucho y siento que ahora tengo las herramientas adecuadas para sentarme y escribir una teoría real enriquecida del cálculo Rho y comenzar a dar los fundamentos algebraicos completos.
Greg: Gracias por eso. Esa es una buena caracterización. Creo que deberíamos mencionar que cuando dices que no hay una teoría, te refieres a una de estas teorías algebraicas o teorías algebraicas abstractas de orden superior que la representan y que satisfacen los criterios de internalización.
Hay algunas otras sutilezas. Una es que la sintaxis de Fiore no tiene en cuenta las reescrituras. Un monoide no tiene reescrituras unidireccionales. Solo tiene reescrituras bidireccionales.
cristiano: Esta es una de estas cosas en las que ha trabajado cómo funciona, pero no lo ha publicado.
Greg: Has estado viendo el enriquecimiento de gráficos como un enfoque particular. La gente ha mirado esto extensamente. Las reglas SOS de Plotkin como formato para expresar reescrituras son muy exitosas. Que yo sepa, no existe un consenso sobre un formato de regla que sea ampliamente aceptado por la comunidad como la captura de todas las cosas que queremos poder capturar. Este es en realidad un punto del que estaba hablando con Mike (Stay) porque el enriquecimiento de gráficos es una buena herramienta, pero no articula toda la estructura que articulan estos formatos de reglas.
Es importante conocer toda esa estructura de grano fino, especialmente si eres alguien que realmente está diseñando un lenguaje. Ya sea que esté hablando de las transiciones en la máquina virtual Java o solo de las reglas de reescritura del cálculo ambiental, hay muchos casos interesantes para cubrir. Necesita una estructura de grano fino para poder articular esos casos de una manera que especifique económicamente el idioma.
Eso me lleva a una pregunta: ¿Marcelo ha intentado esto para el cálculo ambiental? Porque el cálculo ambiental no se basa en la sustitución. Es un rompecabezas muy interesante.
cristiano: No estoy seguro de si lo está haciendo para el cálculo ambiental, pero sé que lo ha hecho para el cálculo de Pi.
Greg: Si recuerdas, tú y Mike y yo estábamos viendo dos problemas. Una es hacer que el conjunto HAM sea una colección del tipo de colección en el caso distributivo. En otras palabras, el conjunto HAM se enriquece de esa manera. El otro es que el conjunto HAM está enriquecido en las reglas de reescritura. Teníamos curiosidad acerca de cómo podrían interactuar esos dos enriquecimientos.
Mike tenía una propuesta alternativa en la que codificaba la teoría de la gráfica, la parte de reescritura de la estructura, como una teoría, que luego separaría las dos. El enriquecimiento sería en términos de la colección y luego la parte del gráfico se agregaría como una teoría adicional. Lo que habla de ese enfoque es que las ecuaciones de origen y destino se convierten en un lenguaje, un lenguaje más fino para su formato de regla.
El punto final que es de interés es que los tipos con los que termina no están relacionados directamente con los tipos que obtenemos de las fórmulas de estilo Caires, como en las lógicas de comportamiento espacial, ni son como los tipos de sesión. Estos son tipos categóricos y su expresividad con respecto a la concurrencia aún no se ha explorado.
El objetivo del programa LADL es proporcionar una base para explicar los tipos de sesión y Caires y mostrar cómo hay algo debajo de ellos que hace el trabajo. Una de las historias de éxito interesantes es que puede unificar el tipo de flecha del cálculo de Lambda de tipo simple con el modal Hennessy-Milner. ¿Qué has hecho con respecto a la investigación de los tipos?
cristiano: Esperaba explicar la idea de los investigadores. Isaac, ¿tienes alguna pregunta?
Isaac: Quería saber más sobre cómo esta idea de enlace variable difiere de estos operadores de arity.
cristiano: La idea es que tenemos una categoría de contextos (en el sentido de la teoría de tipos). Si alguna vez ha visto estos juicios, en donde la hipótesis tiene estos términos de estos tipos, puede deducir estos términos de este tipo. La primera mitad se llama contexto. Es tu lugar actual en tu razonamiento que eres.
Isaac: ¿Como tipo de entorno?
cristiano: Exactamente. La idea es que tenemos una categoría de contextos. Los objetos allí son tipos. Si toma un producto de un montón de ellos, ese es otro objeto que representa tener un término de cada uno de esos tipos. Lo que queremos hacer es pensar en los functores de la categoría de contextos; cuando comencemos a enriquecer, será nuestra categoría enriquecedora.
La idea es que un functor de la categoría de contexto para establecer. Tomemos la categoría como conjuntos finitos. Esto toma solo el conjunto finito N como una especie de genérico en contexto variable y le da el conjunto de todos los términos en algún lenguaje que podría formar con esas N variables. Un functor como Lambda mayúscula, desde conjuntos finitos hasta conjuntos, para cada número natural que le indica para el número natural N, el conjunto de términos en el cálculo Lambda que puede formar dentro de tres variables.
Describe la estratificación del lenguaje. Si imagina el proceso de generar un lenguaje (el cálculo de Lambda se genera por variables, aplicación y abstracción) cuando especifica esto como estas reglas de juicio, dependen del contexto.
El de las variables es realmente fácil. Si se encuentra en el contexto de N variables libres, puede proyectar cualquiera de ellas y puede tener X sub I. Para la aplicación, si tiene N contexto N, puede derivar el término T1 y en el contexto N puede derivar término T2. Luego, en el contexto N, puede derivar su aplicación entre sí.
Esos dos son fáciles. El que está haciendo algo interesante es la abstracción de Lambda porque vincula una variable. La forma en que escribe esto es que si está en el contexto N más 1 y puede derivar el término T, entonces en el contexto N elimina ese distinguido más 1, puede derivar Lambda X de N más 1 punto T. Esto trae desde un nivel más alto de contexto N más 1 de vuelta al contexto N y ha seleccionado ese más distinguido más 1 y lo ha convertido en una variable ligada distinguida. Estaba libre en la parte superior y luego quedó atado en la parte inferior.
Isaac: Eso tiene sentido.
cristiano: El functor realiza un seguimiento de estos niveles. En cualquier nivel, puede decirle exactamente qué variables están ligadas versus libres.
Greg: ¿Funcionalidad está garantizando qué?
cristiano: Garantiza que estos términos son estables al renombrarlos. Más prisiones en esa categoría de contexto son solo renombrar variables, barajarlas. Como estamos en una categoría artesiana, la estructura adicional que tenemos es que puede duplicar variables o eliminarlas. Si alguna vez quieres estar en una teoría de tipos en la que no quieres poder hacerlo, así que en las teorías de tipos lineales, entonces cambias la categoría de contexto a la categoría de conjuntos finitos en bifunciones en lugar de en cualquier funciones Por lo tanto, solo puede barajar variables.
Isaac: ¿Entonces la functorialidad desempeña el papel de congruencia alfa?
Greg: Si. Esa es una de las cosas que hace que esta teoría sea atractiva, al menos desde el punto de vista de un informático. A las personas que se les ocurrió la noción de functorialidad no estamos pensando en la congruencia alfa. El hecho de que la functorialidad de repente explique la congruencia alfa es un punto a favor de este enfoque.
cristiano: Lo que está sucediendo aquí es que, además de las operaciones unarias normales, ahora tenemos este nuevo tipo de arity, que es secretamente un arity de cierto functor de conjuntos finitos a conjuntos; es la inclusión de conjuntos finitos en conjuntos. Se llama variables depreciativas. Cuando ha tomado esto como una aridad de una operación, en lugar de simplemente tomarlo en un cierto número de cosas de ciertos tipos, en realidad está tomando una variable libre distinguida. La abstracción de Lambda es una operación desde delta – se llama delta en minúsculas – de la capital Lambda a Lambda. Toma un término de Lambda más una variable libre distinguida y le da otro término de Lambda donde ahora está vinculado.
Esta es la diferencia clave que le permite comenzar a hablar sobre los lenguajes formales que realmente les interesan a los lógicos y los informáticos porque la sustitución es el corazón de la computación. Depende de la noción de enlace variable. Básicamente, eleva el álgebra normal a estas categorías de functores en categorías de contexto. Puede hacer todo lo que pudo antes, excepto que ahora tiene este enlace variable.
Greg: Por cierto, deberíamos dar un poco de providencia. Sí, mientras que Fiore et al resolvieron esto en este contexto, la intuición original vino de John Reynolds, quien intentaba explicar la semántica de referencia en ML. Quería poder mantener un estado variable, donde puede crecer o reducir ubicaciones de referencia en el entorno.
Si no tiene un estado inmutable en su entorno, puede manejarlo de otras maneras. Cuando tienes un estado mutable, que está más o menos a la par con la nueva construcción en el cálculo de Pi, entonces necesitas una historia diferente. Propuso las categorías functor para modelar esa semántica.
Esta idea ha estado flotando durante unos 40 años y fue adaptada y hecha más bonita y limpia, pero la idea ha existido por un tiempo.
cristiano: No sé mucho sobre ese programa de Reynolds. Isaac, ¿tenía sentido?
Isaac: Sí, definitivamente. Gracias por la explicación adicional.
cristiano: Esa fue la idea básica que Fiore et al esbozaron en un artículo de 1999. Desde entonces, el proyecto se ha ido construyendo cada vez más. La idea básica con los functores en conjuntos finitos a conjuntos tiene que ver con lenguajes sin tipo o de un solo tipo con contexto cartesiano. La categoría de conjuntos finitos, técnicamente, es la categoría opuesta, es la categoría gratuita con productos finitos, en solo uno, la categoría de terminal. En esto, solo puede expresar, por ejemplo, el cálculo Lambda sin tipo.
Por ejemplo, la forma en que podría comenzar a involucrar tipos es que, en lugar de simplemente tomar esa construcción libre en una sola categoría de objeto, podría tomarla en algún conjunto de tipos. Si hace lo mismo, excepto que su categoría de contextos son pares de números naturales, entonces las ranuras de la tupla representan que ahora tiene dos tipos. Y si hace lo mismo donde está tomando functors en esto, ahora su contexto dice que tiene tres del primer tipo y cuatro términos del segundo tipo.
La sutileza sobre el cálculo Rho es que no solo tienes dos tipos que existen en paralelo. Tiene estos operadores de referencia y desreferenciación que convierten los tipos entre sí, o más, si Greg prefiere cuáles recuerdan los tipos. ¿Cómo llamarías la distinción entre nombres y procesos?
Greg: Normalmente eso se llamaría una especie. Entiendo que en la semántica categórica los llamas tipos. En el mundo de la informática, esos son tipos.
cristiano: En este caso, habrá más estructura. En lugar de simplemente tomar como categoría gratuita, si nunca has oído hablar del término libre, básicamente significa que generas algún tipo de estructura en la que no impones ninguna regla adicional. Si quieres tomar un alfabeto y formar el monoide gratis, entonces lo que estás haciendo es hacer el conjunto de todas las palabras que puedes formar en ese alfabeto más una operación que es como juntar palabras. Esto se llama gratuito porque es como la estructura monoide más simple posible que puedes poner en ese conjunto. De manera similar aquí, comenzamos con algunos datos iniciales …
Greg: ¿Te importa si lo interrumpo solo un segundo? La forma en que pienso sobre las estructuras libres versus otras es que las libres no tienen ecuaciones. Mientras que otros monoides pueden exhibir algunas ecuaciones, como la conmutatividad o la potencia del ítem.
cristiano: Entonces técnicamente todavía tiene la ecuación de asociatividad, pero no tiene ecuaciones adicionales.
Greg: No hay ecuaciones adicionales. En general, si no estamos hablando de monoides, sino de estructuras algebraicas arbitrarias, libre significa que no hay ecuaciones. En el caso de los monoides, debe tener al menos las ecuaciones de asociatividad e identidad. Es útil para las personas que piensan en esto cuando agregas ecuaciones, estás borrando la estructura. Free tiene toda la estructura de grano fino. A medida que se limita cada vez más equitativamente, la estructura se borra o identifica.
cristiano: Por ejemplo, esto no es realmente cómo va a funcionar, pero es una aproximación. En lugar de simplemente tener un conjunto de tipos, lo que estamos haciendo es comenzar con una pequeña categoría. Solo tiene un objeto para nombres y un objeto para procesos. Luego, estas dos flechas, una que va de un proceso a otro y otra que va de un nombre a otro, de modo que se mantienen ciertas ecuaciones.
Esta no es la historia completa porque no podrás expresar comunicación en ese nivel. Pero el punto es que, en lugar de simplemente tomar una categoría libre en un conjunto de tipos, los tipos en el cálculo Rho tienen esta estructura mucho más rica. Ya están intrínsecamente relacionados.
Incluso simplemente declarar adecuadamente la teoría del cálculo Rho en este marco va a ser un artículo muy interesante. La incorporación del enriquecimiento podría incluso ser todo el documento además de eso. Es difícil juzgar exactamente qué tan difícil va a ser. Realmente estoy deseando que llegue porque el cálculo Rho trae algunas ideas nuevas, sobre todo reflexión, que nunca se han considerado en este marco de sintaxis abstracta. Creo que agregará nuevas dimensiones realmente interesantes a esas ideas.
Greg: Eso es genial. ¿Puedes darnos algunos pensamientos? ¿Has bajado un poco por la madriguera del conejo para decirnos si hay dragones o reinas rojas en esa madriguera del conejo?
cristiano: Lamentablemente no. Acabo de regresar de estos viajes. Fiore y yo pasamos dos semanas juntos a finales de junio. Desde entonces, he estado en estas conferencias y escuelas de verano. Él piensa que la noción de reflexión es realmente interesante y ciertamente está dispuesto a ayudarnos a trabajar en ella.
Greg: Oh Dios. ¿Tuviste la oportunidad de mostrarle el cálculo del espacio-tiempo, en el que no solo reificas los procesos como nombres, sino que también reificas los contextos? Aquí estamos hablando del contexto del término en lugar del contexto de tipo.
cristiano: No, no le mostré eso.
Greg: Esta bien. La reflexión ya es un gran paso para la comunidad, ya que la sigo encontrando.
cristiano: Es nuevo para casi todos. Está realmente integrado en esta comunidad de investigación de alto nivel. Informarle sobre estas cosas será realmente útil.
Greg: La comunidad informática todavía no comprende la utilidad de los espacios de nombres. En 2005, cuando estaba en el confiable satélite de computación global de Echaps, comencé a tocar la idea de los espacios de nombres. Les di algunos ejemplos, pero luego me retiré de esa comunidad para dedicarme a la biología.
Hacemos espacios de nombres de particiones de forma regular porque eso es lo que hacen las URL. Pero cuanto más pueda hacer esto de una manera abstracta, donde pueda caracterizar lógicamente los espacios de nombres, más poder obtendrá en términos de poder razonar sobre el comportamiento de un sistema de extremo a extremo, como ser capaz de construir una compilación -tiempo de firewall.
Creo que la comunidad aún no ha internalizado el poder de los espacios de nombres. Todavía estoy llegando a comprenderlos como los resultados en las tasas de reacción de codificación en espacios de nombres. Eso fue un shock y una sorpresa para mí. No me esperaba eso. Es un gran paso. La comunidad de la informática avanza a un ritmo deliberado.
Issac: Estoy realmente emocionado de ver a dónde va todo esto porque he estado buscando mucho en una lógica de espacio de nombres recientemente, todos los tipos espaciales de comportamiento. Estoy realmente interesado en ver dónde termina esta investigación que estás haciendo.
cristiano: Con respecto a la lógica del espacio de nombres, cuando se lo estaba mostrando a Marcelo hacia el final de mi estadía, estaba mirando esta interpretación. Si va al documento de lógica de espacio de nombres, está la página donde se presenta la interpretación de todos los operadores de cálculo Rho, pero también aumenta la firma con operadores lógicos. Así es como estamos obteniendo más expresividad en nuestros tipos.
La interpretación de los operadores lógicos es bastante sencilla. Me refiero y corresponde a la intersección o una respuesta a la unión, etc. Los que están haciendo el trabajo duro es la interpretación de par, por ejemplo. Para dividir un átomo así, debe ser capaz de considerar todos los posibles pares de procesos, de modo que cuando se colocan en paralelo, actúan de manera similar al proceso que está interpretando.
Greg: No, no bisimilar.
cristiano: Lo siento. Estructuralmente equivalente.
Greg: Hay una gran diferencia.
cristiano: Fue realmente interesante. Cuando vio que esta es una de las ventajas de ser hipereducado, dijo que esto se parece a esto en la teoría de categorías llamada producto detector. Empezamos a resolverlo. Si tiene una estructura monoidal en una categoría, por ejemplo, está pensando en par como una operación en tipos donde estos términos en la lógica del espacio de nombres se consideran como los tipos, esto le brinda una forma de elevar esa estructura monoidal a una monoidal estructura en la categoría de functores en esa categoría.
Si aquí estamos pensando en todos estos términos en la lógica del espacio de nombres como tipos u objetos en la categoría de contexto, y las operaciones nos están dando operaciones en esa categoría, van a levantar la categoría de functores en ese categoría. Todavía no está definido, pero parece que esto puede proporcionar una forma automática de dividir las operaciones de forma natural. No solo el par, sino cualquiera de estas operaciones binarias o unarias en tipos. Existe la posibilidad de que esto pueda dar una forma simplificada de generar estas funciones de interpretación, donde si tiene una firma para cierto cálculo de proceso, y luego la aumenta con una firma de cierto tipo de lógica que desea agregar, es aún no está definido, pero es muy tentador en este momento.
Isaac: ¿Cómo dijiste que se llama un contrato categórico?
cristiano: Se llama deconvolución. Entonces, el artículo en el laboratorio sobre esto podría ser difícil, pero básicamente solo una imagen: ¿te sientes cómodo pensando en una estructura monoidal en una categoría?
Isaac: Sí, eso creo.
cristiano: Básicamente, es la forma más simple si estás considerando, sigo diciendo functors, pero realmente estamos hablando de preajustes en el contexto de la categoría, es la forma más simple de elevar la estructura monoidal en la categoría de contexto a la categoría de presheaves. Si estamos en la categoría de contexto, esos son nuestros tipos, los preajustes son como los idiomas que se escriben de esa manera. Estamos elevando esas operaciones en los tipos a las operaciones en los propios idiomas a los términos del idioma.
Greg: De las cosas de las que usted y Marcelo han hablado, la desconvolución es la que realmente me interesa. Durante mucho tiempo pensé que debería haber un papel para la deconvolución en el entorno. Si resulta que podemos hacer que eso funcione y nos da una mejor idea de lo que hace que todo esto funcione, eso sería una gran noticia.
cristiano: Si lees esa fórmula para la interpretación de P par Q …
Greg: ¿Te refieres a tarifa par C?
cristiano: Lo siento, si. Está diciendo … ¿fue R?
Greg: Normalmente uso M para ir después de los términos. Entonces, toma el lenguaje total, el conjunto de todos los términos, y encuentra toda la M en ellos de modo que se descomponga en un par M1 en 2, por lo que es estructuralmente equivalente a un par M1 en M2, y M1 satisface la tarifa y M2 satisface DO.
cristiano: Si, exacto. Existe M1, M2 de modo que M1 par M2 es equivalente a M. Esa es precisamente la fórmula para la deconvolución.
Greg: Oh, muy interesante.
cristiano: Existe un cierto tipo de construcción universal en la teoría de categorías llamada final y coeficiente. Son como límites y co-límites que entienden las variantes. El co uno es como una fantasía realmente existe. En realidad es una gran generalización del cuantificador existencial. Entonces dices coend sobre todos los tipos. Está buscando otros tipos porque estos podrían ser otros objetos en su categoría de contexto, que son términos en los nombres de esas lógicas. Sería más fácil con el papel, pero es literalmente una traducción de esa fórmula. Por eso se encendió cuando lo vio y dijo que ese es el producto detector.
Greg: Wow, eso es realmente genial.
cristiano: Creo que es una gran pista de algo. Creo que incluso para hacer la teoría del cálculo Rho correctamente, con el tipo correcto de tipos en este marco, ya debes haber descubierto LADL. Porque si realmente queremos que LAD nos proporcione los tipos, desde el principio tendremos que describir la toma de functors sobre cómo es esta categoría de tipos. Creo que podríamos tener que resolver esto al mismo tiempo que la teoría.
Greg: Creo que probablemente tengas razón. Samson Abramsky describió estas categorías de interacción. Si observa la forma en que describió cuáles son los tipos y cómo genera la categoría, hay una gran invitación abierta.
¿Puedes tomar los tipos de Caires o los tipos de sesión o algo que se encuentra debajo de ellos y construir la categoría donde los tipos son los objetos y el morfismo son los cálculos? Esa es la pregunta realmente interesante. Y hasta ahora nadie lo ha hecho.
cristiano: ¿Qué papel es ese?
Greg: Si solo busca en Google "categorías de interacción", hay un montón de documentos que él y Simon Gay y Rajagopal Nagarajan y Guy McCusker analizaron en varias instancias. Al menos una encarnación de la ontología que Samson estaba esbozando, las categorías de interacción eran la base. Entonces, la semántica del juego era una instancia de categorías de interacción y CCS: podían dar un sistema de tipos para CCS, no podían hacer Pi. El CCS fue otra instancia de categorías de interacción, pero las categorías de interacción fueron la construcción general. Mike y yo nos estamos acercando terriblemente a ese territorio nuevamente porque hemos estado observando los tipos de sesión y los teoremas de no seguir los estimulan.
Los tipos solo pueden tener ciertas formas. Mike dijo qué pasa con los tipos de sesión, donde no tienen esa forma. Luego miramos cuidadosamente eso y resulta que lo hacen, es solo que la negación ahora está plegada en ejecución. Ese no es el caso con los tipos de Caires. La negación de tipos de Caires tiene que ver con la colección, pero en el trabajo de tipos de sesión, o al menos en el sabor Abramsky de los tipos de sesión, la negación se define mutuamente en términos de corte, que es la operación de ejecución. De nuevo, recuperas esta estructura fundamental. Nos estamos acercando terriblemente al territorio del que estás hablando. Entonces podría ser una buena idea que tú, Mike y yo hablemos.
