Higher-order judgements

From The Twelf Project
Jump to: navigation, search

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.


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

This page is incomplete. We should expand it.