# Higher-order judgements

(Redirected from Higher-order judgment)

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.