Reformulating languages to use hypothetical judgements

It’s easy to represent hypothetical judgements in LF, exploiting higher-order representation techniques. This tutorial presents some object-language judgements which are not typically phrased as hypothetical judgements, but can easily be reformulated as such, making the correspondence with their LF representation quite clear. In particular, we discuss parallel reduction and complete development for the lambda-calculus; thanks to Randy Pollack for suggesting this example.

Before reading this tutorial, you should learn about hypothetical judgements and their representation in LF:

• Representing the judgements of the STLC shows how object-language hypothetical judgements can be represented using LF binding.
• Proving totality assertions in non-empty contexts shows an additional example, and discusses proving totality assertions about higher-order judgements.
• Proving metatheorems in non-empty contexts shows how to use totality assertions to prove metatheorems about higher-order judgements.

Syntax is a hypothetical judgement

First, we need to define the syntax of the untyped lambda-calculus:

$$M ::= x \mid \mathsf{lam}(x.M) \mid \mathsf{app}(M_1, M_2)$$

A traditional story about this definition is that variables $x$ are some piece of first-order data such as strings or de Bruijn indices, $\mathsf{lam}(x.M)$ is a binder (which means it can be $\alpha$-converted and can be substituted for) and so on.

However, suppose we were given a single untyped datatype of tree-structured data with binding as a primitive notion, where such trees $t$ consist of variables $x$, binders $x.t$, and applications of constants such as $\mathsf{lam}$ and $\mathsf{app}$. Then we can save ourselves the trouble of recapitulating the construction of binding for each object language by simply carving out those trees that represent the language in question. We can do so with a hypothetical judgement of the form

$$x_1\,\mathtt{trm} \; \ldots \; x_n\,\mathtt{trm} \vdash M\,\mathtt{trm}$$

where the subjects of the judgement "$\_\,\mathtt{trm}$" are untyped binding trees. This judgement is defined as follows:

$${ {x\,\mathtt{trm} \in \Gamma} \over {\Gamma \vdash x\,\mathtt{trm}} } \qquad { {\Gamma \vdash M_1\,\mathsf{trm} \qquad \Gamma \vdash M_2\,\mathsf{trm}} \over {\Gamma \vdash \mathsf{app}(M_1, M_2)\,\mathtt{trm}} }$$ $${ {\Gamma, x\,\mathtt{trm} \vdash M\,\mathtt{trm}} \over {\Gamma \vdash \mathsf{lam}(x.M)\,\mathtt{trm}} }$$

A variable is a term if it was assumed to be a term; at a binder, we extend the context by assuming a new term. The important point about this style of definition is that variables are inherently scoped and given meaning only by assumption: $x$ is only meaningful if we are in a context where we have some assumptions about it. Consequently,

$$x_1\,\mathtt{trm} \; \ldots \; x_n\,\mathtt{trm} \vdash M\,\mathtt{trm}$$

captures exactly the terms $M$ with free variables $x_1$…$x_n$.

When you’re working with an inherently scoped type of binding trees, you can’t give an unconditional definition of what it means to be a term with rules like

$$\color{red} { \over {x\,\mathtt{trm}} } \qquad { M\,\mathtt{trm} \over \mathsf{lam}(x.M)\,\mathtt{trm} }$$

where the first rule means “all those trees that happen to be variables are terms”: it would break the abstraction of variables-as-scoped-data to state a rule about all those trees that happen to be variables.

The moral of the story is that syntax with binding can be thought of as a hypothetical judgement. The LF encoding of this syntax can be thought of as an intrinsic encoding of the above judgement $\Gamma \vdash M\,\mathtt{trm}$. LF provides typed binding trees, so we can define terms by specifying typed operators, rather than a predicate over untyped trees:

%sort trm %.
%term lam %pi (%pi trm %-> trm) %-> trm %.
%term app %pi trm %-> trm %-> trm %.

Then this judgement:

$$x_1\,\mathtt{trm} \; \ldots \; x_n\,\mathtt{trm} \vdash M\,\mathtt{trm}$$

becomes the following LF judgment:

$$x_1 : \mathtt{trm} \; \ldots \; x_n : \mathtt{trm} \vdash M : \mathtt{trm}$$

where the $x_i$ and $M$ are LF variables and terms.

Parallel reduction

Parallel reduction is traditionally defined as follows. For conciseness, we write $\lambda x.M$ instead of $\mathsf{lam}(x.M)$ and $M_1\,M_2$ instead of $\mathsf{app}(M_1,M_2)$

$${ \over x \Rightarrow x }\mathit{var} \qquad { M \Rightarrow M' \qquad N \Rightarrow N' \over (\lambda x.M)\,N \Rightarrow M'[N'/x] }\mathit{beta}$$ $${ M \Rightarrow M' \qquad N \Rightarrow N' \over M\,N \Rightarrow M'\,N' }\mathit{app} \qquad { M \Rightarrow M' \over \lambda x.M \Rightarrow \lambda x.M' }\mathit{lam}$$

But there’s a problem with this presentation: it’s not explicit about scoping! The first rule has the exact same problem as the “bad” rule above that had $x\,\mathtt{trm}$ as a premise and no conclusion.

If we want to treat variables as scoped data, we must be explicit about scoping. This suggests the following presentation:

$$\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}$$ $${ x\,\mathtt{trm} \in \Gamma \over \Gamma \vdash x \Rightarrow x }\mathit{var} \qquad { \Gamma, x\,\mathtt{trm} \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \over \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x] }\mathit{beta}$$ $${ \Gamma \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \over \Gamma \vdash M\,N \Rightarrow M'\,N' }\mathit{app} \qquad { \Gamma, x\,\mathtt{trm} \vdash M \Rightarrow M' \over \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M' }\mathit{lam}$$

Now at least the judgement only talks about well-scoped data. However, the $\mathit{var}$ rule that concludes $\Gamma \vdash x \Rightarrow x$ can be a stumbling block for encoding in LF. It has the form “derive $\Gamma \vdash J'$ if $J \in \Gamma$” where $J$ and $J'$ are different judgements. That’s not one of the structural principles of a hypothetical judgement, and allowing this strange sort of access to the context could invalidate the substitution principle (if I substitute for $J$, I can no longer derive $J'$!). So what are we to do?

We’ll give three possibilities here. The third is in some sense the “most faithful” to the informal specification above. However, when one is not committed to a specific presentation, it’s often best to let the formalization guide the informal specification!

Reformulation 1: Hypothetical reductions

While a rule that says “derive $\Gamma \vdash J'$ if $J \in \Gamma$” is suspicious, a rule that says “derive $\Gamma \vdash J$ if $J \in \Gamma$” is just the usual hypothesis/identity axiom that we expect from all hypothetical judgements. So, one solution is to change the notion of context we consider so that $\mathit{var}$ is just an instance of hypothesis. Whenever we assume a variable $x\,\mathtt{trm}$, we also assume a derivation $x \Rightarrow x$:

$$\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}, x \Rightarrow x$$ $${ x \Rightarrow x \in \Gamma \over \Gamma \vdash x \Rightarrow x }\mathit{var}_1 \qquad { \Gamma, x\,\mathtt{trm}, x \Rightarrow x \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \over \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x] }\mathit{beta}_1$$ $${ \Gamma \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \over \Gamma \vdash M\,N \Rightarrow M'\,N' }\mathit{app}_1 \qquad { \Gamma, x\,\mathtt{trm}, x \Rightarrow x \vdash M \Rightarrow M' \over \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M' }\mathit{lam}_1$$

In this presentation, the $\mathit{var}$ rule is totally unobjectionable. In the premies of the rules $\mathit{beta}$ and $\mathit{lam}$ , which deal with binding forms, the context is extended with the assumption that $x \Rightarrow x$ for the bound variable $x$ . The derivations of this version are isomorphic to the first definition of $\Gamma \vdash M \Rightarrow N$ , but the $\mathit{var}$ rule here works as a use of hypothetical judgements.

The LF representation of this formulation is quite direct:

%sort => {_ trm} {_ trm} %.
%prec %none 10 => %.
%term =>/beta
  %pi (app (lam M) N => M' N')
  %<- ({x trm} %pi (x => x) %-> (M x => M' x))
  %<- (N => N') %.
%term =>/app %pi (app M N => (app M' N')) %<- (N => N') %<- (M => M') %.
%term =>/lam %pi (lam M => lam M') %<- ({x trm} %pi (x => x) %-> (M x => M' x)) %.
%block =>b {x trm} {=>/x x => x}%.
%worlds (=>b) (=> _ _) %.

Derivations using $\mathit{var}$ are represented by LF variables representing the reduction assumptions in $\Gamma$. The STELF %worlds declaration documents the form of $\Gamma$ in our informal definition.

Adequacy

This is an adequate encoding of the informal judgment we started with: there’s a 1-to-1 correspondence between derivations like this with the rules subscripted with $1$:

$$x_1\,\mathtt{trm}, x_1 \Rightarrow x_1, \ldots, x_k\,\mathtt{trm}, x_k \Rightarrow x_k \vdash M \Rightarrow M'$$

and with LF derivations $D$ such that the following is derivable according to the rules of LF:

$$x_1 : \mathtt{trm}, d_1 : x_1 \Rightarrow x_1, \ldots x_k : \mathtt{trm}, d_k : x_k \Rightarrow x_k \vdash D : M \Rightarrow M'$$

Substitution

This reformulation elucidates a substitution principle for parallel reduction, as an instance of the general substitution principle for hypothetical judgements:

If $\Gamma, x\,\mathtt{trm}, x \Rightarrow x \vdash M \Rightarrow N$
and $\Gamma \vdash M'\,\mathtt{trm}$
and $\Gamma \vdash M' \Rightarrow M'$,
then $\Gamma \vdash [M'/x]M \Rightarrow [M'/x]N$.

In the LF representation, this substitution principle comes “for free” from the general substitution principle for LF terms.

Reformulation 2: Change the relation

Another option is to change the definition of the judgement so that it doesn’t have a variable-specific rule. In this case, we can generalize the variable rule to a general reflexivity rule:

$$\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}$$ $${ \over \Gamma \vdash M \Rightarrow M }\mathit{refl}_2 \qquad { \Gamma, x\,\mathtt{trm} \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \over \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x] }\mathit{beta}_2$$ $${ \Gamma \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \over \Gamma \vdash M\,N \Rightarrow M'\,N' }\mathit{app}_2 \qquad { \Gamma, x\,\mathtt{trm} \vdash M \Rightarrow M' \over \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M' }\mathit{lam}_2$$

This is a different definition than the informal one we started with: derivations with the rules subscripted $2$ are not isomorphic to those subscripted $1$. However, the while this change changes the possible derivations, it does not change the relation $M \Rightarrow N$, because reflexivity was admissible before. Maybe that’s an acceptable change, that actually simplifies the definition.

The LF representation looks like this:

%sort => {_ trm} {_ trm} %.
%prec %none 10 => %.
%term =>/refl M => M %.
%term =>/beta %pi (app (lam M) N => M' N') %<- ({x trm} M x => M' x) %<- (N => N') %.
%term =>/app %pi (app M N => (app M' N')) %<- (N => N') %<- (M => M') %.
%term =>/lam %pi (lam M => lam M') %<- ({x trm} M x => M' x) %.
%block trmb {x trm}%.
%worlds (trmb) (=> _ _) %.

Substitution

The substitution principle implied by this LF development looks a bit simpler than the previous one, though this is only because it lacks the premise $\Gamma \vdash M' \Rightarrow M'$, which as we’ve previously mentioned is always derivable even in the first reformulation.

If $\Gamma, x\,\mathtt{trm} \vdash M \Rightarrow N$
and $\Gamma \vdash M'\,\mathtt{trm}$
then $\Gamma \vdash [M'/x]M \Rightarrow [M'/x]N$.

Reformulation 3 : Tagged variables

If we’re really committed to the original informal specification, with the rule that said we could immediately derive the reflexive conclusion $\Gamma \vdash x \Rightarrow x$ when $x$ was specifically a variable in the context, then it’s possible to capture that by having an new judgment $x\,\mathtt{isvar}$, which is only ever derivable from a hypothetical judgment.

$$\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}, x\,\mathtt{isvar}$$

Then, we can use the $x\,\mathtt{isvar}$ judgment as a regular, uncontroversial hypothetical judgment, where a premise $J \in \Gamma$ allows you to prove the conclusion $\Gamma \vdash J$

$${ x\,\mathtt{isvar} \in \Gamma \over \Gamma \vdash x\,\mathtt{isvar} } \qquad { \Gamma \vdash M\,\mathtt{isvar} \over \Gamma \vdash M \Rightarrow M }$$

This presentation is pedantically appropriate, but it’s entirely more common to take these two rules and compress them into the single on-paper rule $\mathit{var}_3$ shown below:

$${ x\,\mathtt{isvar} \in \Gamma \over \Gamma \vdash x \Rightarrow x }\mathit{var}_3 \qquad { \Gamma, x\,\mathtt{trm}, x\,\mathtt{isvar} \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \over \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x] }\mathit{beta}_3$$ $${ \Gamma \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \over \Gamma \vdash M\,N \Rightarrow M'\,N' }\mathit{app}_3 \qquad { \Gamma, x\,\mathtt{trm}, x\,\mathtt{isvar} \vdash M \Rightarrow M' \over \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M' }\mathit{lam}_3$$

When all is said and done, this actually looks a lot like the first reformulation, but we’re using a one place relation $\mathtt{isvar}$ instead of the two-place relation where hypothetical occurrences are, by invariant, always reflexive.

Unlike the first reformulation, where the $\mathit{var}_1$ rule came “for free” from LF, this formulation has four rules. The rule looks a little different in LF than in the on-paper derivation, because we use the uppercase M in LF instead of the lowercase $x$ in $\mathit{var}_3$, but the meaning is the same, since we will only ever derive a term of type isvar M when M is a variable in the context.

%sort => {_ trm} {_ trm} %.
%prec %none 10 => %.
%sort isvar {_ trm} %.
%term =>/var %pi (M => M) %<- (isvar M) %.
%term =>/beta
  %pi (app (lam M) N => M' N')
  %<- ({x trm} %pi (isvar x) %-> (M x => M' x))
  %<- (N => N') %.
%term =>/app %pi (app M N => (app M' N')) %<- (N => N') %<- (M => M') %.
%term =>/lam %pi (lam M => lam M') %<- ({x trm} %pi (isvar x) %-> (M x => M' x)) %.
%block isvarb {x trm} {isvar/x isvar x}%.
%worlds (isvarb) (isvar _) (=> _ _) %.

Substitution

As always when we are defining judgments in non-closed worlds, LF provides us a substitution principle for free. But, this time, the substitution principle is basically useless:

If $\Gamma, x\,\mathtt{trm}, x \Rightarrow x \vdash M \Rightarrow N$
and $\Gamma \vdash M'\,\mathtt{trm}$
and $\Gamma \vdash M'\,\mathtt{isvar}$,
then $\Gamma \vdash [M'/x]M \Rightarrow [M'/x]N$.

We only ever get to prove $\Gamma \vdash M'\,\mathtt{isvar}$ when $M'$ is a variable! The for-free substitution properties in the last two formulations actually told us something, but here we’ve got. It is possible to prove the substitution theorem that we expect --- the same substitution theorem that LF gave for free in the first reformulation --- but we have to prove a metatheorem to do so. It’s quite a bit of development for what is, at the end of the day, a straightforward proof by induction:

%sort subst {_ {x trm} {d isvar x} M x => N x} {_ M' => M'} {_ M M' => N M'} %.
%mode subst %in %in %out %.
%term _ subst ([x] [dx isvar x] =>/var dx) (%the (M' => M') D2) D2 %.
%term _ subst ([x] [dx isvar x] =>/var D) (%the (M' => M') D2) (=>/var D) %.
%term _
  %pi (subst ([x] [dx isvar x] =>/beta (%the (M2 x => N2 x) (D1 x dx)) ([y] [dy isvar y] %the (M1 x y => N1 x y) (D1' x dx y dy))) (%the (M' => M') D2) (%the (app (lam ([y] M1 M' y)) (M2 M') => N1 M' (N2 M')) (=>/beta D3 D3')))
  %<- (subst D1 D2 (%the (M2 M' => N2 M') D3))
  %<- ({y} {dy isvar y} subst ([x] [dx isvar x] D1' x dx y dy) D2 (%the (M1 M' y => N1 M' y) (D3' y dy))) %.
%term _
  %pi (subst ([x] [dx isvar x] =>/app (%the (M1 x => N1 x) (D1 x dx)) (%the (M2 x => N2 x) (D1' x dx))) (%the (M' => M') D2) (%the (app (M1 M') (M2 M') => app (N1 M') (N2 M')) (=>/app D3 D3')))
  %<- (subst D1 D2 (%the (M1 M' => N1 M') D3))
  %<- (subst D1' D2 (%the (M2 M' => N2 M') D3')) %.
%term _
  %pi (subst ([x] [dx isvar x] =>/lam ([y] [dy isvar y] %the (M x y => N x y) (D1 x dx y dy))) (%the (M' => M') D2) (%the (lam ([y] M M' y) => (lam ([y] N M' y))) (=>/lam D3)))
  %<- ({y} {dy isvar y} subst ([x] [dx isvar x] D1 x dx y dy) D2 (%the (M M' y => N M' y) (D3 y dy))) %.

The %worlds for the metatheorem is the same isvarb block used in the third reformulation.

%worlds (isvarb) (subst _ _ _) %.
%total T (subst T _ _) %.

Conclusion: the cost of losing substitution

The third reformulation above was almost without a doubt the one most akin to the initial presentation. But the cost was that the substitution principle needed to be established separately, which requires a bit of work.

This is sometimes the correct call: in the development of structural focalization on the wiki, there were two “focal substitution principles.” It was ultimately the most convenient to balance clarity and convenience prove one of the two principles by hand (as in the third reformulation above) while letting the other be inhereted from LF’s substitution principles (as in the first two reformulations above).

Complete development

Parallel reduction is non-deterministic: any left-hand term that can be reduced by the beta rule can also be reduced by the app rule, which is why the relation can be reflexive. Complete development is a restriction of parallel reduction where beta takes precedence over app. In each step of complete development, all of the beta-redices in the left-hand term are reduced.

Informally, we add a side condition to the app rule:

$${ \Gamma \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \qquad (M \textit{ is not a lambda}) \over \Gamma \vdash M\,N \Rightarrow M'\,N' }\mathit{app}$$

How can we state this side condition more precisely? We need a judgement $M\,\mathtt{notlam}$ which holds whenever $M$ does not have the form $\lambda x.M'$. It’s easy to define this as a hypothetical judgement if we choose our contexts correctly:

$$\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}, x\,\mathtt{notlam}$$ $${ x\,\mathtt{notlam} \in \Gamma \over \Gamma \vdash x\,\mathtt{notlam} } \qquad { \over \Gamma \vdash (M_1\,M_2)\,\mathtt{notlam} }$$

That is, with each variable, we make the additional assumption that it is not a lambda.

Then complete development is easy to define:

$$\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}, x\,\mathtt{notlam}, x \Rightarrow x$$ $${ x \Rightarrow x \in \Gamma \over \Gamma \vdash x \Rightarrow x }\mathit{var}_c$$ $${ \Gamma, x\,\mathtt{trm}, x\,\mathtt{notlam}, x \Rightarrow x \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \over \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x] }\mathit{beta}_c$$ $${ \Gamma \vdash M \Rightarrow M' \qquad \Gamma \vdash N \Rightarrow N' \qquad M\,\mathtt{notlam} \over \Gamma \vdash M\,N \Rightarrow M'\,N' }\mathit{app}_c$$ $${ \Gamma, x\,\mathtt{trm}, x\,\mathtt{notlam}, x \Rightarrow x \vdash M \Rightarrow M' \over \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M' }\mathit{lam}_c$$

The LF representation is direct:

%sort notlam {_ trm} %.
%term notlam/app notlam (app _ _) %.
%block nlb {x trm} {nlx notlam x}%.
%worlds (nlb) (notlam _) %.

Whenever we add a trm assumption to the LF context, we assume that it is not a lambda. The STELF %worlds declaration documents this fact, and causes STELF to complain if we ever violate this convention.

Then complete development is a simple twist on parallel reduction:

%sort ==> {_ trm} {_ trm} %.
%prec %none 10 ==> %.
%term ==>/beta
  %pi (app (lam M) N ==> M' N')
  %<- ({x trm} %pi (notlam x) %-> (x ==> x) %-> (M x ==> M' x))
  %<- (N ==> N') %.
%term ==>/app %pi (app M N ==> (app M' N')) %<- (N ==> N') %<- (M ==> M') %<- (notlam M) %.
%term ==>/lam
  %pi (lam M ==> lam M')
  %<- ({x trm} %pi (notlam x) %-> (x ==> x) %-> (M x ==> M' x)) %.
%block ==>b {x trm} {nlx notlam x} {==>/x x ==> x}%.
%worlds (==>b) (==> _ _) %.

Every time we extend the context, we add an assumption notlam x for that variable. We also add a reflexivity assumption for each variable because the informal definition of complete development still has a reflexivity rule for variables (even though the relation is not reflexive in general).

Substitution

As above, this formulation gives a “free” substitution principle for complete development:

If $\Gamma, x\,\mathtt{trm}, x\,\mathtt{notlam}, x \Rightarrow x \vdash M \Rightarrow N$
and $\Gamma \vdash M'\,\mathtt{trm}$
and $\Gamma \vdash M'\,\mathtt{notlam}$
and $\Gamma \vdash M' \Rightarrow M'$,
then $\Gamma \vdash M[M'/x] \Rightarrow N[M'/x]$.

The form of the context ensures that we need a derivation of $M\,\mathtt{notlam}$ to make this substitution. This restriction is similar to the restriction that made the third reformulation’s “free” substitution principle useless, but it’s more reasonable in this case: it’s not obvious that you can substitute lambdas for variables while preserving complete development, since you’d have to replace instances of app with something else.

Examples

We can give a few examples of parallel reduction in action using the %query mechanism.

%query 1 _ _ app (lam ([x] app x x)) (lam ([x] app x x)) ==> N %.
%define z lam ([f] lam ([x] x)) %.
%define s lam ([n] lam ([f] lam ([x] app f (app (app n f) x)))) %.
%query 1 _ _ app (app s z) (lam ([f] lam ([x] app f (app f x)))) ==> N %.

See also

• Hypothetical judgements
• Higher-order judgements
• The case study on Church-Rosser via complete development for some proofs about the judgements defined here, illustrating the use of regular worlds.