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.

Contents

[edit] Example

[edit] 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:

\texttt{}\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 \texttt{}\gamma containing assumptions of the form \mathsf{}x : \tau. Such a context is well-formed when all variables in it are distinct.

{ \; \over \gamma, x : \tau, \gamma' \vdash x : \tau}\,\mbox{of-var}           { \gamma , x : \tau_2 \vdash e : \tau \over \gamma \vdash \lambda x:\tau_2.e : (\tau_2 \rightarrow \tau)}\,\mbox{of-lam}          

{ \; \over \gamma \vdash \langle\rangle : \texttt{unit}}\,\mbox{of-empty}           { \gamma \vdash e_1 : (\tau_2 \rightarrow \tau) \qquad \gamma \vdash e_2 : \tau_2 \over \gamma \vdash e_1 e_2 : \tau}\,\mbox{of-app}

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

  • Hypothesis: \gamma,x : \tau \vdash x : \tau.
  • Weakening: if \gamma \vdash e : \tau and \mathsf{}x is fresh then \gamma,x:\tau' \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 of-var. Weakening, exchange, and substitution are admissible.

[edit] 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 \gamma \vdash e : \tau 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 x:τ does two things:

  • It binds the variable \mathsf{}x.
  • It declares a typing assumption x:τ.

Thus, an object-language assumption x:τ 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 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 \mathsf{}x:\tau.

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

[edit] See also

This page is incomplete. We should expand it.
Retrieved from "http://twelf.plparty.org/wiki/Higher-order_judgements"
Personal tools