# What are Contexts in Lambda Calculus?

What is a Context? Is it like a scope in C? Does it have a start and an end? Can contexts contain other contexts?

I see Contexts being used in lambda calculi type system rules, but I don't understand concretely what they are and why they are necessary. If they are too abstract, then is there some visual or metaphorical description?

Update: I am referring to "contexts" as what is to the left of ⊢ in typing calculi.

• A context is just a dictionary/hashmap/association-list consisting of name-type pairs: Given a name, if it is in the context, then it is associated a type. That is all ^_^ In some sense, this is the notion of scope in C ;-) – Musa Al-hassy Apr 26 '20 at 9:07
• Do you mean contexts as in what's to the left of $\vdash$ in typed calculi (which is what the current answer and comment are about), or contexts as in $[]$ in reduction rules (with or without types)? They are different concepts. – Gilles 'SO- stop being evil' Apr 26 '20 at 11:50

## 1 Answer

Typing contexts are the way to remember previously declared variables when type-checking a program/term. The rule for term abstraction usually is something like $$\dfrac{\Gamma,x:A\vdash e : B}{\Gamma\vdash \lambda x.e : A\to B}$$ In the conclusion, $$x$$ is not in $$\Gamma$$ yet. At this point, $$x$$ is declared to be the variable of the function $$\lambda x.e$$ and this variable appears in $$e$$. So, $$x$$ is a free variable in $$e$$. The typing rule above expresses that $$\lambda x.e$$ is of type $$A\to B$$ under context $$\Gamma$$ iff $$e$$ is of type $$B$$ under context $$\Gamma,x:A$$. So in the premise of the rule, we are type-checking the body of $$\lambda x.e$$ (which is $$e$$), but we need to remember that $$x$$ (which appears free in $$e$$) is a variable of type $$A$$.