Signature and Environment in Type Theory Signature and Environment are both related to the description of constants. I feel confused about the two notions in type theory. Could anyone explain their main difference? Thanks!
 A: Functionally, environment (or contexts) and signatures behave quite similarly, and in some settings you can emulate signatures using environments to place the axioms as variables in the context. However, they should be thought of differently.
An environment or context is typically a list of typed variables, e.g. $x_1 : A_1, \ldots, x_n : A_n$. Terms in this environment may project out the variables, e.g. $x_1 : A_1, x_2 : A_2 \vdash \langle x_2, x_1 \rangle : A_2 \times A_1$. The environment may differ during the course of a derivation, for instance if binding operators, like $\lambda$-abstractions, are used. In a certain sense, environments are a notion internal to the type theory.
A signature in type theory is a set of constants and function symbols (and potentially base types) that are given as axioms for the type theory (the exact form will differ depending on the treatment). These axioms may be used throughout a derivation, just like ordinary rules. However, the signature is fixed for a type theory: the signature may not change over the course of a derivation, unlike an environment. You can think of the type theory as being parameterised by the signature. Therefore, signatures are in some sense an external notion.
If the type theory in question has function types, we can represent function symbols from a signature as variables (of function types) in an environment, but this will only behave the same way as a signature if we do not bind those variables. Another way of thinking about it is that variables in an environment are local (and hence may not be available everywhere), whereas constants in a signature are global (and may be used at any point in a derivation).
