Trabajo de Robin Milner sobre Concurrencia

Tuve la oportunidad de conocer el trabajo de Robin Milner debido a varias actividades realizadas durante los años 2016 y 2017 como miembro del grupo de investigación Tlön de la Universidad Nacional de Colombia . Considero que los trabajos de investigación de este científico de la computación deben darse a conocer y estudiarse pues, en mi opinión, impactarán las ciencias de la computación en el presente y el futuro tanto en lo teórico como en lo práctico.

El texto presentado a continuación es la traducción de un reconocimiento para Robin Milner (1934-2010) por su trabajo sobre la teoría de la concurrencia. Este homenaje fue presentado por el profesor Samson Abramsky en la conferencia Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010) realizada en Mayo de 2010 en Canadá.

Para aquellas personas que sigan interesadas sobre la vida de este científico de la computación, recomiendo leer también la entrevista realizada a Robin Milner el 3 de septiembre de 2003.


1. Introducción

Esta breve nota está basada en la conferencia realizada en una sesión en honor al trabajo de Robin [Milner] que tuvo lugar en el MFPS [Mathematical Foundations of Programming Semantics ] en Ottawa el 8 de mayo de 2010, justo unas pocas semanas después de su fallecimiento.

Robin Milner. https://alchetron.com/Robin-Milner-1019871-W
Robin Milner. https://alchetron.com/Robin-Milner-1019871-W

En la misma sesión Bob Harper expuso sobre el trabajo de Robin [Milner] en LCF [Logic for Computable Functions] y ML [Meta Language]. Yo [Samson Abramsky] decidí enfocarme en su trabajo sobre concurrencia. Creo que este fue el trabajo que era más significativo para él – y fue el más importante de sus muchos logros-.

En 1989 escribí que las ideas de Robin [Milner] habían llegado a formar parte del aire que respiramos en la comunidad científica. ¡Esto es más cierto hoy!

Hay tantas cosas que hemos aprendido, y continuaremos aprendiendo de Robin [Milner], acerca de los detalles técnicos de los diferentes formalismos. Trataré de articularlo en el breve texto que sigue.

2. 1979: La primera revolución.

Comencemos con algunos antecedentes.

La década de 1970 tuvo un desarrollo extensivo de la teoría de dominio y la semántica denotacional. El paradigma básico para estos casos es que los programas son modelados como funciones. Esto está bien para la programación funcional (procesamiento secuencial), pero ¿qué sucede con la concurrencia?

Estructuras primitivas en las redes de Petri. [https://www.techfak.uni-bielefeld.de/~mchen/BioPNML/Intro/pnfaq.html]
Estructuras primitivas en las redes de Petri. [https://www.techfak.uni-bielefeld.de/~mchen/BioPNML/Intro/pnfaq.html]
Ya existía una teoría para la concurrencia: las redes de Petri. Esta tenía unas ideas profundas, pero le faltaban algunas características estructurales críticas. Hubo también un número de ideas importantes en programación: los semáforos de Dijkstra, los monitores de Brinch Hansen, las regiones críticas de Hoares, etcétera, pero no había ninguna teoría sistemática y exhaustiva.

Al mismo tiempo, existían imperativos tecnológicos urgentes: sistemas distribuidos, Internet, etc. ¿Quién podría asumir el reto?

Llega CCS [Calculus of Communicating Systems]

Carátula del libro de 1980 sobre CCS [Calculus of Communicating Systems] de Robin Milner.
La introducción de Robin [Milner] de CCS [Calculus of Communicating Systems] transformó el campo de estudio. Los ingredientes cruciales, en mi opinión, son los siguientes:

  • Los procesos son vistos como una estructura matemática (en lugar de un modelo de máquina)
  • En particular, a los procesos se les da una estructura algebraica.

P ::= a.P | 0 | P + Q | P || Q | P \ a | P[S] | . . .

Esto fue enormemente importante: por primera vez, los procesos podían ser estudiados composicionalmente.

  • Sabíamos que las funciones ya estaban. ¿Pero qué son los procesos? CCS [Calculus of Communicating Systems] estableció el punto metodológico fundamental para estudiarlos mediante el comportamiento observado (definido en términos de sistemas de transición etiquetados a través de SOS [Structural Operational Semantics])

Esto lleva inexorablemente a la noción de equivalencia observacional.

CCS [Calculus of Communicating Systems] no solo fue un nuevo cálculo, también fue un nuevo paradigma – que ha jugado un rol central en los desarrollos posteriores de nuestro tema [de investigación]. Nos abrió la puerta al mundo del modelamiento comportamental composicional.

MFPS [Mathematical Foundations of Programming Semantics ] 1989

Muchos otros hubieran descansado en sus laureles, Robin [Milner] nunca lo hizo.

  • Ya había revolucionado el campo de estudio con su libro sobre CCS [Calculus of Communicating Systems] en 1980 [2], estimulando en gran parte el crecimiento de una comunidad de investigación completa, incluyendo desarrollos relacionados tales como el trabajo extensivo sobre CSP [Communicating sequential processes] (Brookes, Hoare, Roscoe y otros) y la escuela alemana de álgebra de procesos (Bergstra, Klop y otros)
  • Ya había liderado los esfuerzos para estandarizar ML [Meta Language] y construirlo personalmente, junto con Bob Harper, Mads Tofte y otros, la definición formal y comentada sobre el lenguaje [5,9]
  • Ya había escrito el texto Communication and Concurrency [3] en 1989 como una presentación pulida y definitiva de CCS [Calculus of Communicating Systems].
Carátula del libro Communication and Concurrency de Robin Milner.
Carátula del libro Communication and Concurrency de Robin Milner.

Sin embargo en su presentación en el MFPS [Mathematical Foundations of Programming Semantics ] fue una de las primeras ocasiones donde él presentó lo que luego se llamaría cálculo π.

En ese evento él se re-energizó, rebosante de ideas. Una nueva fase del tema había comenzado.

La búsqueda de Robin [Milner]: el cálculo λ de la concurrencia

Imagen adaptada de “A Tutorial Introduction to the Lambda Calculus” de Raul Rojas. https://arxiv.org/pdf/1503.09060.pdf

El cálculo λ es una teoría de funciones y de computación funcional increíblemente rica, concisa y exhaustiva. Hay muchas extensiones y variaciones, pero el núcleo central del cálculo puede ser presentado en unas pocas líneas — y hay (esencialmente) ¡solo una!

¿Puede lograrse algo de calidad similar para la concurrencia?

A pesar de todo el éxito de CCS [Calculus of Communicating Systems] y sus variantes, Robin [Milner] se dió cuenta que aún no había alcanzado esa meta. Como evidencia de esto, el cálculo λ en sí mismo no podía codificarse composicionalmente en CCS [Calculus of Communicating Systems] de forma satisfactoria.

Con una extraordinaria sagacidad, Robin [Milner] observó que se podía utilizar la noción de nombre como un bloque de construcción para expresar la movilidad de un proceso y de esta forma abrir la puerta a un sorprendente poder expresivo en el cálculo de procesos.

La importancia de usar nombres, nombres únicos y que cumplan la condición de frescura [freshness] es algo que conocen desde hace mucho tiempo los investigadores en sistemas, pero hasta ese momento nadie había imaginado cómo podía aprovecharse su esencia en una teoría elegante y expresiva.

3. El cálculo π

Carátula del libro sobre cálculo π de Robin Milner.
Carátula del libro sobre cálculo π de Robin Milner.

El cálculo π, creado por Robin [Milner] junto con Joachim Parrow y David Walker [8] es un cálculo magnífico, conciso y expresivo.

El núcleo central del cálculo se puede comunicar en una sola línea:

P ::= x(y).P | x’y.P | 0 | P || Q | νx.P | !P . . .

De nuevo, lo que se creó no fue solo un cálculo en particular, si no un paradigma. A partir de este se han generado un gran número de sub-generos de cálculos ‘móviles’ y cálculos ‘nominales’.

Algunos de los ingredientes clave del cálculo π son:

  • Congruencia estructural. Esta fue una transmutación de Robin [Milner] a partir de la idea de la Máquina Química Abstracta [Chemical Abstract Machine] de Berry y Boudol y ha probado ser una idea extremadamente útil que ha sido adoptada de forma amplia.
  • Nombres, nombres que cumplan la condición de frescura [freshness], extrusión de ámbito [scope extrusion]. Esto lleva al sub-paradigma completo de ‘cálculo nominal’, tanto en la forma funcional como de procesos.
  • Tipos comportamentales, que restringen la dinámica del comportamiento de los procesos en lugar de clasificar valores estáticamente como ocurre en las teorías de tipos clásicas.
  • La posibilidad de representar un amplio rango de fenómenos computacionales, incluyendo computación de alto orden y computación orientada a objetos, protocolos de seguridad, modelamiento biológico, procesos de negocios y más.

El cálculo π probó ser aún más exitoso que CCS [Calculus of Communicating Systems]. Robin [Milner] le dió una presentación pulida y magistral en su libro Communicating and Mobile Systems: the Pi-Calculus en 1999 [6].

¿Él quedó satisfecho?

4. La búsqueda continúa

Con toda la belleza y el éxito del cálculo π, Robin [Milner] se dió cuenta que éste no era el cálculo λ de la concurrencia. Había demasiadas variaciones y alternativas posibles.

Con mucha energía y convicción Robin [Milner] reescribió el guión nuevamente. Ahora él buscaba, antes que un único y exhaustivo cálculo, una estructura canónica y exhaustiva en un metanivel.

Esto llevó al trabajo sobre cálculo de acción [action calculi] y estructuras de control [control structures] [4,1].

Esto permitió descubrir estructuras estáticas fascinantes , sin embargo parecía estancado en el problema de capturar la dinámica comportamental de los sistemas a ese nivel de generalidad.

Una vez más, Robin [Milner] tenía otras preocupaciones por un tiempo, como jefe de departamento en [la universidad de] Cambridge. ¿Qué sigue?

5. Bigrafos

Carátula del libro sobre Bigrafos de Robin Milner.
Carátula del libro sobre Bigrafos de Robin Milner.

La última fase del trabajo de Robin [Milner] fue sobre bigrafos, culminando en su último libro, publicado en 2009, The Space and Motion of Communicating Agents [7].

[Nota: para quien esté interesado en profundizar sobre este tema, además de intentar leer el libro, puede visitar la página Learning about Bigraphs - https://www.cl.cam.ac.uk/archive/rm135/uam-theme.html]

Nuevamente Robin [Milner] reformó el paradigma. Las siguientes son algunas de las características sobresalientes:

  • Se reconocen dos clases de estructuras de encadenamiento [linking structrure], que son sorprendentemente ortogonales: una del tipo de encadenamiento por nombres presentada en el cálculo π, la otra una estructura espacial, como la presentada por Cardelli y Gordon en el Ambient Calculus, y desarrollada subsecuentemente de forma extensiva como un sub-paradigma.
  • La estructura estática es analizada en términos de categorías monoidales simétricas, construida con base en el trabajo anterior sobre estructuras de acción.
  • Hay un tratamiento importante de las dinámicas, resolviendo los problemas que había frustrado el trabajo anterior, utilizando ideas de cuadrados cocartesianos relativos de una forma muy original – de ninguna manera es una teoría de categorías ‘lista para usar’.
  • Un formalismo gráfico atractivo y natural.
  • Un mayor empuje hacia las herramientas de soporte y las aplicaciones en computación obicua y sistemas biológicos, liderado, fomentado y guiado por Robin [Milner].

¿Qué tan importante será este nuevo paradigma? Es demasiado pronto para saberlo.

6. Algunas lecciones que podemos aprender de Robin [Milner]

  • ¡Nada está escrito en piedra! ¡No queremos seguidores ciegos!

Después de crear un paradigma, él lo reajusta y construye uno nuevo, no una vez, si no en tres fases formidables. Siempre con un propósito, llevando el tema a un nivel más alto.

  • ¡Seguir hasta el final!

Cuatro libros importantes sobre concurrencia: 1980, 1989, 1999, 2009. Lideraron, inspiraron y fomentaron un extenso cuerpo de trabajo, que va desde la teoría hasta las herramientas de soporte y las aplicaciones.

  • Estar abierto al trabajo de los demás y aprender de ellos.

(Aunque en manos de Robin [Milner], usualmente las ideas eran transformadas de alguna manera)

Ejemplos clave incluyen: SOS [Structural Operational Semantics] (Gordon Plotkin), bisimulación (David Park), congruencia estructural [structural congruence] (Gérard Berry y Gérard Boudol), categorías monoidales de procesos (José Meseguer y Ugo Montanari), estructura espacial [spatial structure] (Luca Cardelli y Andy Gordon).

  • Usar las matemáticas correctas para apropiarse de su visión científica, sin ajustar el enfoque con el fin de adaptarlo a las matemáticas [preconcebidas] que a uno le gustaría que fueran.

Las estructuras matemáticas usadas por Robin [Milner] en las diversas fases de su trabajo incluyó dominios, sistemas de transición etiquetados y SOS [Structural Operational Semantics]), categorías y más.

  • Reflexionar los temas de principio a fin

Siempre que alguien hacia una pregunta relacionada con el por qué alguna característica de uno de sus cálculos estaba de cierta manera o sugería alguna posible alternativa, era claro que Robin [Milner] los había considerado profunda y cuidadosamente.

think

Robin [Milner] no daba respuestas apresuradas ni ofrecía pirotecnia intelectual . Intelectualmente, él tenía la rapidez de un corredor de largas distancias. Sus ideas, igualmente, han mostrado su capacidad para permanecer.

Y hay mucho más…

7. Palabras finales

Robin [Milner] fue a la vez un gran científico y un gran ser humano. Ciertamente nuestra comunidad ha sido afortunada en tener a alguien para inspirarnos como ser humano y como intelectual.

Gracias Robin.

Referencias

[1] Mifsud, A., R. Milner and J. Power, Control structures, en: Symposium on Logic in Computer Science (LiCS), Published by the IEEE Computer Society Press, 1995, p. 188.

[2] Milner, R., “A Calculus of Communicating Systems,” Lecture Notes in Computer Science 92, Springer-Verlag, 1980.

[3] Milner, R., “Communication and Concurrency,” Prentice Hall, 1989.

[4] Milner, R., Action calculi, or syntactic action structures, Mathematical Foundations of Computer Science 1993 (1993), pp. 105–121.

[5] Milner, R., “The Definition of Standard ML: revised,” The MIT Press, 1997.

[6] Milner, R., “Communicating and Mobile Systems: the π-calculus,” Cambridge Univ Pr, 1999.

[7] Milner, R., “The Space and Motion of Communicating Agents,” Cambridge University Press, 2009.

[8] Milner, R., J. Parrow and D. Walker, A calculus of mobile processes, I, Information and Computation 100 (1992), pp. 1–40.

[9] Milner, R. and M. Tofte, “Commentary on Standard ML,” MIT press, Cambridge, MA, 1991.

[10] Lope Programming Language – http://www.expdev.net/lope/