Higher-order judgements

When representing judgments in LF, it is often possible to represent hypothetical judgments using LF binding. We call this representation technique higher-order judgments because judgments are represented using higher-order types in LF. Higher-order representations are advantageous because hypothetical judgment properties such as weakening, exchange, and substitution are inherited “for free” from the corresponding properties of LF.

Example

Hypothetical judgment in standard notation

As an example, we use the typing judgment for the simply-typed lambda calculus. This calculus has the following syntax:

$$\tau ::= \texttt{unit} \,|\, \tau_1 \rightarrow \tau_2$$ $$\texttt{e} ::= x \,|\, \langle\rangle \,|\, \lambda x :\tau . e\ |\, e_1\ e_2$$

The terms are the variable $x$, the empty pair (which has type unit), lambda abstraction (with a type annotation), and application.

The typing rules for the simply typed lambda calculus use a typing context $\gamma$; containing assumptions of the form $x : \tau$. Such a context is well-formed when all variables in it are distinct.

$${ \over \gamma, x : \tau, \gamma' \vdash x : \tau }\textit{of-var} \qquad { \gamma, x: \tau_2 \vdash e : \tau \over \gamma \vdash \lambda x:\tau_2.e : (\tau_2 \rightarrow \tau) }\textit{of-lam}$$ $${ \over \gamma \vdash \langle\rangle : \texttt{unit} }\textit{of-empty} \qquad { \gamma \vdash e_1 : (\tau_2 \rightarrow \tau) \qquad \gamma \vdash e_2 : \tau_2 \over \gamma \vdash \lambda x:\tau_2.e : (\tau_2 \rightarrow \tau) }\textit{of-app}$$

This is a hypothetical judgement, which means that the following structural properties are true:

• Hypothesis: $\gamma, x : \tau \vdash x : \tau$ is derivable.
• Weakening: if $\gamma \vdash e : \tau$ and $x$ is fresh then $\gamma, y: \tau_2, x: \tau_1 \vdash e : \tau$.
• Exchange: if $\gamma, x : \tau_1, y : \tau_2 \vdash e : \tau$ then $\gamma, y : \tau_2, x : \tau_1 \vdash e : \tau$.
• Substitution: if $\gamma, x : \tau' \vdash e : \tau$ and $\gamma \vdash e' : \tau'$ then $\gamma \vdash \{e'/x\}e : \tau$.

Hypothesis is derivable by the rule $\textit{of-var}$. Weakening, exchange, and substitution are admissible.

LF representation

We represent the syntax of this calculus with the following LF signature:

%sort tp %.
%term arrow %pi tp %-> tp %-> tp %.
%term unit tp %.
%sort tm %.
%term empty tm %.
%term app %pi tm %-> tm %-> tm %.
%term lam %pi tp %-> (%pi tm %-> tm) %-> tm %.

Terms are represented using higher-order abstract syntax.

As an example of higher-order representations of judgments, we use LF binding to represent the object-language typing judgement. The following LF signature represents the above judgement $\gamma \vdash e : \tau$ with the LF type family of.

%sort of {_ tm} {_ tp} %.
%term of-empty of empty unit %.
%term of-lam
  %pi (of (lam T2 ([x] E x)) (arrow T2 T))
  %<- ({x tm} %pi (of x T2) %-> (of (E x) T)) %.
%term of-app %pi (of (app E1 E2) T) %<- (of E1 (arrow T2 T)) %<- (of E2 T2) %.

The first thing to note is that the type family is indexed by a tm and a tp but not a representation of the context $\gamma$;. The reason for this is that we identify the object-language context with the LF context. Specifically, an object-language assumption $x:\tau$ does two things:

• It binds the variable $x$.
• It declares a typing assumption $x : \tau$.

Thus, an object-language assumption $x: \tau$ is represented by the following two LF assumptions:

x : tm, dx : of x T (where T is the encoding of $\tau$).

The first LF variable represents an object-language term x, as per the encoding of syntax in the previous section. The second variable represents a derivation that of x T. Consequently, there is no LF constant corresponding to the rule $\textit{of-var}$; uses of this rule are represented by uses of the corresponding LF variable dx.

This representation of hypotheses gives rise to the higher-order premise of the constant of-lam, which has type

{x: tm} of x T2 -> of (E x) T

An LF term of this type has the form ([x] [dx: of x T2] M), where M : of (E x) T in an LF context extended with x : tm, dx : of x T2. Thus, M is the representation of an object-language derivation under the additional assumption $x:\tau$.

The constants of-empty and of-app correspond to the informal inference rules of the same name.

See also

• the introductions to STELF for more discussion of higher-order representations of hypothetical judgments.
• Reformulating languages to use hypothetical judgements
• higher-order abstract syntax