Parentesi dopo l'ambiente di digitazione

Question

Ultimamente ho letto di System F Omega e continuo a imbattermi in un costrutto nelle regole di digitazione di cui non riesco a trovare una spiegazione: Γ(x) = k.Ad esempio, nel Una breve introduzione ai sistemi F e F Omega:

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

Vedo lo stesso costrutto in Sostituzione ereditaria per il sistema stratificato F.Capisco bene la parte inferiore.Si leggerebbe qualcosa del tipo:"Nel contesto Γ, a è gentile k".Non sono riuscito a trovare una spiegazione della parte superiore e le fonti a cui ho fatto riferimento presumono entrambe familiarità con questo costrutto.Se dovessi indovinare, sospetto che significhi qualcosa come "Nel contesto a, eseguendo un algoritmo di controllo del tipo su a ti dà gentile k come risultato".È accurato?Quali risorse online descrivono questo costrutto?

Answer 1

$\Gamma$ ecco la notazione sovraccarica.Il significato dell'espressione $\Gamma(x) = au$ sopra la linea di deduzione qui è riportato sotto "Regole di tipo."sezione di Una breve introduzione ai sistemi F e F Omega a pagina 5.In questa impostazione, $\Gamma$ è una funzione definita induttivamente che invia variabili (in $\Gamma$ considerato come un contesto, cioèun elenco di variabili) ai loro tipi.

Un modo più illustrativo e sintattico per scrivere la regola che fornisci potrebbe essere: $\frac{}{\Gamma,\ x : au\ \vdash x : au}$, Dove $\Gamma$ spazia liberamente nei contesti.Nota che l'ordine delle variabili in un contesto qui non ha importanza, quindi questa regola ci consente di proiettare qualsiasi variabile in un contesto come termine.

Answer 2

Per aggiungere alla risposta di Varkor:

Un contesto è semplicemente una funzione che invia (alcune) variabili ai loro tipi.

Quindi la regola dice:"Se $\Gamma$ assegna il tipo $ au$ a variabile $x$, allora possiamo dedurre $\Gamma \vdash x : au$."