Entre parênteses após a Digitação do Ambiente

Question

Estive lendo sobre Sistema F Omega ultimamente, e eu continuo tropeçando em uma construção na digitação regras que eu não encontro uma explicação: Γ(x) = k.Por exemplo, em Uma Breve Introdução aos Sistemas F e F Omega:

Γ(a) = k
--------
Γ ⊢ a : k

Eu vejo o mesmo de construir, de Hereditária de Substituição para um Sistema Estratificado F.Eu entendo a parte inferior multa.Ficaria algo como:"No contexto Γ, a tem tipo k".Eu não tenho sido capaz de encontrar uma explicação para a parte de cima, e as fontes que eu referenciados ambos assumir familiaridade com essa construção.Se eu tivesse que adivinhar, eu suspeito que significa algo como "No contexto a, executando uma espécie de verificação de algoritmo a dá-lhe o tipo k como o resultado".É que precisas?Que recursos on-line descrever essa construção?

Answer 1

$\Gamma$ aqui está sobrecarregado de notação.O significado da expressão $\Gamma(x) = au$ acima da linha de inferência aqui é dada sob a "Digite as regras."seção de Uma Breve Introdução aos Sistemas F e F Omega na página 5.Nesta definição, $\Gamma$ é um indutivamente função definida pelo envio de variáveis (em $\Gamma$ considerado como um contexto, isto é,uma lista de variáveis) para os respectivos tipos.

Mais ilustrativos, sintático maneira de escrever a regra que você dá pode ser: $\frac{}{\Gamma,\ x : au\ \vdash x : au}$, onde $\Gamma$ intervalos livremente sobre os contextos.Note que a ordem das variáveis em um contexto aqui não importa, portanto, esta regra nos permite projetar qualquer variável em um contexto como um termo.

Answer 2

Adicionar ao varkor a resposta:

Um contexto é apenas uma função de envio (alguns) variáveis para os respectivos tipos.

Portanto, a regra é dizer:"Se $\Gamma$ atribui o tipo de $ au$ a variável $x$, e , em seguida, podemos deduzir $\Gamma \vdash x : au$."