# 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:

The terms are the variable , 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 containing assumptions of the form . Such a context is well-formed when all variables in it are distinct.

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

- Hypothesis: .
- Weakening: if and is fresh then .
- Exchange: if then .
- Substitution: if and then .

Hypothesis is derivable by the rule . Weakening, exchange, and substitution are admissible.

### LF representation

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

tp : type. arrow : tp -> tp -> tp. unit : tp. tm : type. empty : tm. app : tm -> tm -> tm. lam : tp -> (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 with the LF type family `of`.

of : tm -> tp -> type. of-empty : of empty unit. of-lam : of (lam T2 ([x] E x)) (arrow T2 T) <- ({x: tm} of x T2 -> of (E x) T). of-app : 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 . The reason for this is that we identify the object-language context with the LF context. Specifically, an object-language assumption does two things:

- It binds the variable .
- It declares a typing assumption .

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

`x : tm, dx : of x T ` (where `T` is the encoding of ).

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 ; 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 .

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

## See also

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

This page is incomplete. We should expand it.