Teoría de dominios y polimorfismo

8

La teoría del dominio ofrece una teoría sorprendente de la computabilidad en presencia de tipos simples. Pero cuando se agrega el polimorfismo paramétrico, no parece haber una buena teoría que explique qué está pasando tan bien como la teoría del dominio explica la computación sobre tipos simples. Ciertamente, no esperaría que exista tal cosa para el Sistema-F porque no existen modelos teóricos establecidos del Sistema-F. ¿Qué pasa con una restricción del Sistema-F que tiene predicción y tiene una jerarquía universal? ¿Se ha estudiado esto? ¿Existe una buena teoría de dominio que se aplique a ella? Yendo más lejos, ¿qué pasa con los tipos dependientes? ¿Puede la teoría de dominio mezclarse de alguna manera con débilω-groupoids para lograr algo?

Jake
fuente
1
Estoy confundido: hay modelos teóricos de dominio de lo no tipificado λ-cálculo, que intuitivamente es un cálculo mecanografiado con un tipo ααα. Esto, por supuesto, tampoco tiene modelos en conjuntos. ¿Por qué esperarías que no haya modelos de dominio del sistema F? ¿Has intentado buscar en línea?
cody
Comprendí que no hay modelos del sistema F en los que las funciones se interpreten como cualquier tipo de función en la teoría de conjuntos. Comprendí que no hay modelos teóricos de conjuntos "ingenuos" del cálculo lambda tipificado, pero que existen modelos teóricos de conjuntos siempre que las funciones sean funciones continuas. Entonces, al igual que las funciones reales continuas tienen la misma cardinalidad que las reales, las funciones continuas de scott también pueden tener el mismo tamaño que su (co) dominio. Entendí que así es como se resolvió el problema de tamaño. Sin embargo, entendí que tal solución no existe para el sistema-F.
Jake
También debo agregar que entendí que la teoría de dominios todavía se establece como teórica en principio. Es decir, las funciones aún están configuradas como funciones teóricas, es solo que solo te preocupas por las funciones continuas cuando interpretas funciones en un cálculo. Por lo tanto, mi comprensión parece descartar el ajuste del Sistema-F en un modelo teórico de dominio. Quizás es uno de mis entendimientos lo que está mal aquí.
Jake
3
Ya veo, gracias por sus aclaraciones. El tratamiento más "similar a la teoría de dominio" del sistema FI conocido es el de "Espacios Coherentes" de Girard, cuyo tratamiento es descrito aquí por Paul Taylor. No sé si esta es una "buena teoría" según su solicitud, pero para ser honesto, realmente no veo que la teoría de dominio sea tan buena en general para la semántica de los idiomas totales ...
cody
1
@cody: tsk, tsk.
Andrej Bauer

Respuestas:

5

Hay muchas maneras de modelar el polimorfismo a través de la teoría de dominios, permítanme describir uno que es fácil de entender, para que pueda pensarlo usted mismo. Es un "modelo PER".

Tome cualquier modelo de lo no tipificado λ-cálculo, por ejemplo un dominio D tal que DD es un retracto de D (por ejemplo, tome D tal que DN×(DD)). DejarΛ:D(DD) y Γ:(DD)D ser la retracción y la sección, respectivamente.

Vamos a interpretar los tipos como relaciones de equivalencia parcial (PER) en D. Recuerde que un PER es una relación simétrica y transitiva, pero que no necesita ser reflexiva. A cada tipoτ así asignamos un PER τ. Pensar enxτx como "x es un elemento de τ"y xτy como "x y y son iguales hasta τ está preocupado ".

Podemos tener algunos tipos básicos (pero no es necesario), por ejemplo, si nos aseguramos de que N es un subdominio de D a través de una incrustación ι:ND entonces podemos definir nat por

xnatynN.x=ι(n)=y.

PERs dados τ y σ, defina el espacio de funciones PER τσ por

xτσyz,wD.zτwΛ(x)(z)σΛ(y)(w)

Los términos se interpretan como sin tipo λ-cálculos como uno los interpretaría normalmente en D.

Aquí está el remate. Puede interpretar el polimorfismo como una intersección de PER, es decir:

xX.τ(X)yfor all PERs xτ()y.
Podemos calcular el PER correspondiente a X.X: es la intersección de todos los PER, pero será el PER vacío. CalculadorX.XXEs un ejercicio interesante. CalculadorX.XXX es un ejercicio difícil (que me mantuvo ocupado durante una semana cuando era estudiante de teoría de dominios).

Si queremos recurrencia en nuestro idioma, entonces debemos tener en cuenta los puntos fijos. Una posibilidad es restringir los PER a aquellos que contienenDy están cerrados bajo suprema de cadenas crecientes. Más precisamente, tome solo esos PER para cual

  • DDy
  • Si x0x1x2 y y0y1y2 están aumentando las cadenas en D tal que xiyi para todos i, entonces supixisupiyi.

Ahora podemos interpretar aplicando el teorema de Kanster-Tarski sobre la existencia de puntos fijos, tal como lo hacemos en la teoría del dominio ordinario. Esta vez, no está vacío, ya que contiene precisamente .fixτ:(ττ)τX.XD

Andrej Bauer
fuente
¡Esta es una respuesta más que fantástica! Básicamente, esto proporciona las mismas herramientas que la parametricidad nos brinda y las herramientas de la teoría de dominios. Esto es exactamente lo que estaba buscando. Bueno, tengo algo que hacer este fin de semana ahora.
Jake
Para el registro, aprendí estas cosas de Dana Scott. Estoy bastante seguro de que John Reynolds conocía los modelos PER cuando inventó la parametricidad. Siempre pensé que la parametricidad provenía de los modelos PER, de todos modos.
Andrej Bauer
Tenía en mi cabeza que era tu asesor. ¿Está escrito en alguna parte o es este folklore?
Jake
Hay muchas cosas escritas sobre esto. ¿Qué estás buscando? El primer artículo histórico (que sería de Dana Scott), un artículo clásico que pone las cosas realmente en marcha, ¿un libro de texto?
Andrej Bauer
2
El libro de texto Dominios y Cálculos Lambda de Roberto Amadio y Pierre-Louis Curien cubre los modelos PER en el Capítulo 15, y un modelo PER del Sistema F en 15.2.
Andrej Bauer
0

Roy Crole da una buena explicación de cómo usar la teoría de dominios para modelar el polimorfismo de tipos en su libro Categorías para tipos , específicamente en la sección 5.6.

Nathan BeDell
fuente
2
¿Podría al menos resumir esa sección en beneficio de las personas que podrían no tener el libro? Un párrafo o dos dando las ideas principales sería suficiente.
David Richerby