Sé que diferentes autores usan notación diferente para representar la semántica del lenguaje de programación. De hecho, Guy Steele aborda este problema en un video interesante .
Me gustaría saber si alguien sabe si el operador principal de torniquetes tiene un significado bien reconocido. Por ejemplo, no entiendo el operador principal al comienzo del denominador de lo siguiente:
¿Puede alguien ayudarme a entender? Gracias.
type-theory
denotational-semantics
Jim Newton
fuente
fuente
type-checking
Respuestas:
A la izquierda del torniquete, puede encontrar el contexto local, una lista finita de supuestos sobre los tipos de variables disponibles.
Arriba, puede ser cero, lo que resulta en . Esto significa que no se hacen suposiciones sobre las variables. Por lo general, significa esto que es un término cerrado (sin ningún tipo de variables libres) que tiene tipo .⊢ e : T e Tn ⊢e:T e T
A menudo, la regla que menciona está escrita en una forma más general, donde puede haber más hipótesis que la mencionada en la pregunta.
Aquí, representa cualquier contexto, y representa su extensión obtenida al agregar la hipótesis adicional a la lista . Es común requerir que no aparezca en , de modo que la extensión no "entre en conflicto" con un supuesto anterior.Γ Γ,x:T1 x:T1 Γ x Γ
fuente
Como complemento a las otras respuestas, tenga en cuenta que hay tres niveles de "implicación" en las derivaciones de escritura. Y el mismo comentario se aplica a las derivaciones lógicas, ya que en realidad existe una correspondencia entre los dos (llamada correspondencia de Curry-Howard).
La primera implicación es la flecha que aparece en las fórmulas, y corresponde a la implicación lógica en una fórmula (o un tipo de función para el cálculo ).λ
La segunda implicación se materializa mediante el símbolo del torniquete, y significa "suponiendo que cada fórmula de la izquierda, la fórmula de la derecha se mantenga". En particular, la regla que das dice cómo se debe probar una implicación: para probar , entonces se debe probar bajo el supuesto de que cumple. En términos del cálculo , para demostrar que tiene tipo , uno debe mostrar que tiene tipo , suponiendo que es una variable de tipo (¿ve la correspondencia?).A⇒B B A λ λx.t A→B t B x A
El tercer nivel de implicación se materializa mediante la barra horizontal, y significa "si cada premisa (elementos en la parte superior) se cumple, entonces la conclusión (el elemento en la parte inferior) se cumple". Puede vincular eso a la interpretación de la regla de escritura para -abstracción que proporcionó (consulte la explicación en el párrafo anterior).λ
fuente
En los sistemas de verificación de tipos, ( ) representa la relación ternaria sobre entornos de tipos, expresiones y tipos: .⊢ ⊢Env×Exp×Typ
En su ejemplo, la expresión se escribe en el tipo wrt. a un entorno de tipo que tiene una asignación de suposición de tipo a alguna variable de tipot2 T2 T1 x
En este contexto, un entorno de tipo es una función parcial que asigna tipos a variables, generalmente denotadas con dondeΓ Γ∈Env:Var⇀Typ
Tenga en cuenta que el operador se reserva su funcionalidad independientemente de dónde aparezca, ya sea en la premisa o en la conclusión de la regla.
fuente
En cada situación que he visto, significa que hay una prueba de que asume que cumple. Si está vacío, eso significa que es una tautología: tiene una prueba sin necesidad de suposiciones.X⊢Y Y X X Y
fuente