¿Cómo leer las reglas de mecanografía?

18

Empecé a leer más y más trabajos de investigación lingüística. Me parece muy interesante y una buena manera de aprender más sobre la programación en general. Sin embargo, generalmente viene una sección en la que siempre lucho (tome, por ejemplo, la tercera parte de esto ) ya que no tengo los antecedentes teóricos en informática: Reglas de tipo.

¿Hay buenos libros o recursos en línea disponibles para comenzar en esta área? Wikipedia es increíblemente vaga y realmente no ayuda a un principiante.

suls
fuente
1
¿Has leído el artículo vinculado sobre las reglas de inferencia ?
Raphael
2
TAPL de Benjamin Pierce es realmente bueno.
Gilles 'SO- deja de ser malvado'

Respuestas:

25

En la mayoría de los sistemas de tipos, las reglas de tipos trabajan juntas para definir juicios de la forma:

Γe:τ

Esto establece que en el contexto la expresión e tiene el tipo τ . Γ es un mapeo de las variables libres de e a sus tipos.Γeτ
Γe

Un sistema de tipos consistirá en un conjunto de axiomas y reglas (un sistema formal de reglas de inferencia , como señala Rafael).

Un axioma es de la forma

Γe:τ

Esto establece que el juicio es válido (siempre).Γe:τ

Un ejemplo es

x:τx:τ

que establece que bajo el supuesto de que el tipo de variable es τ , entonces la expresión x tiene el tipo τ .xτxτ

Las reglas de inferencia toman hechos que ya han sido determinados y construyen hechos más grandes a partir de ellos. Por ejemplo, la regla de inferencia

Γe1:ττΓe2:τΓe1 e2:τ

dice que si tengo una derivación del hecho y una derivación del hecho Γ e 2 : τ , entonces puedo obtener una derivación del hecho Γ e 1 e 2 : τ . En este caso, esta es la regla para escribir la aplicación de función.Γe1:ττΓe2:τΓe1 e2:τ

Hay dos formas de leer esta regla:

  • De arriba hacia abajo: dadas dos expresiones (una función y otra expresión) y algunas restricciones sobre su tipo, podemos construir otra expresión (la aplicación de la función a la expresión) con el tipo dado.
  • De abajo hacia arriba: dada una expresión que es, en este caso, la aplicación de una función a alguna expresión, la forma en que se escribe es escribiendo primero las dos expresiones, asegurando que sus tipos satisfagan algunas restricciones, a saber, que la primera es una tipo de función y que el segundo tiene el tipo de argumento de la función.

Algunas reglas de inferencia también manipulan al agregarle nuevos ingredientes (ver de abajo hacia arriba). Aquí está la regla para la abstracción λ :Γλ

Γx:τe:τΓλx.e:ττ

Las reglas de inferencia se aplican inductivamente en función de la sintaxis de la expresión que se considera que forma un árbol de derivación. En las hojas del árbol (en la parte superior) habrá axiomas, y las ramas se formarán aplicando reglas de inferencia. En la parte inferior del árbol está la expresión que le interesa escribir.

Por ejemplo, una derivación de la tipificación de la expresión esλf.λx.f x

Dos libros muy buenos para aprender sobre sistemas de tipos son:

F:ττ,X:τF:ττF:ττ,X:τX:τF:ττ,X:τF X:τF:ττλX.F X:τλF.λX.F X:τ

Ambos libros son muy completos, pero comienzan lentamente, construyendo una base sólida.

Dave Clarke
fuente
8

Hay un lindo tutorial interactivo en línea sobre cálculo secuencial, que puede ayudar a construir algunas intuiciones y sentir cómo funciona la inferencia: un tutorial interactivo del cálculo secuencial

aemxdp
fuente
3
Eso es realmente genial.
Dave Clarke
1
Increíble. Tengo que encontrar alguna etiqueta wiki para poner esto.
Raphael
5

En esa página de Wikipedia se recomienda " Type Systems, Luca Cardelli, ACM Computing Surveys ", que es una encuesta de 2 páginas que puede ayudarlo a comprender cómo leer una regla. De todos modos, cómo leer una regla se explica perfectamente en esa página de Wikipedia (o incluso mejor en la encuesta de 2 páginas). Sin embargo, para comprenderlo todo, debe comprender qué es un sistema de mecanografía (compuesto por varias reglas), para el cual el artículo de Wikipedia " Sistema de texto " es un buen comienzo (y tiene varios libros en la sección " Referencias " de ese página si quieres ir más allá).

Alejandro DC
fuente