# 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 User:rpollack for suggesting this example.

Before reading this tutorial, you should learn about hypothetical judgements and their representation in LF: Proving metatheorems: Representing the judgements of the STLC shows how object-language hypothetical judgements can be represented using LF binding. Proving metatheorems: Proving totality assertions in non-empty contexts shows an additional example, and discusses proving totality assertions about higher-order judgements. Proving metatheorems: Proving metatheorems in non-empty contexts shows how to use totality assertions to prove metatheorems about higher-order judgements.

## Contents

## Syntax is a hypothetical judgement

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

```
M ::= x | lam x.M | app M1 M2
```

A traditional story about this definition is that variables `x` are some piece of first-order data such as strings or de Bruijn indices, `lam x.M` is a binder (which means it can be -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 consist of variables `x`, binders `x.t`, and applications of constants such as `lam` and `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 `x1 trm ... xn trm |- M trm`, where the subjects of the judgement `trm` are untyped binding trees. This judgement is defined as follows:

```
x trm in G
```

```
```

G |- x trm

G |- M1 trm G |- M2 trm

G |- (app M1 M2) trm

G , x trm |- M trm

```
G |- lam (x.M) 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, `x1 trm ... xn trm |- M trm` captures exactly the terms with free variables `x1`...`xn`.

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

```
```

```
```

x trm

M trm

```
lam (x.M) 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 `x1 trm ... xn trm |- M trm`. LF provides typed binding trees, so we can define terms by specifying typed operators, rather than a predicate over untyped trees:

trm : type. lam : (trm -> trm) -> trm. app : trm -> trm -> trm.

Then the judgement `x1 trm ... xn trm |- M trm` becomes the LF judgement
`x1 : trm ... xn : trm |- M : trm` where `x` and `M` are LF variables and terms.

## Parallel reduction

Parallel reduction is traditionally defined as follows. For conciseness, we write `\x.M` for `lam x.M` and `M1 M2` for `app M1 M2`

------- var x => x M => M' N => N' -------------------- beta (\x.M) N => M'[N'/x] M => M' N => N' ---------------- app (M N) => (M' N') M => N ------------- lam \x.M => \x.N

However, if we want to treat variables as scoped data, we must be explicit about scoping:

G ::= . | G , x trm x trm in G ----------- var G |- x => x G, x trm |- M => M' G |- N => N' --------------------------------- beta G |- (\x.M) N => M'[N'/x] G |- M => M' G |- N => N' -------------------------- app G |- (M N) => (M' N') G, x trm |- M => N ------------------- lam G |- \x.M => \x.N

Now at least the judgement only talks about well-scoped data. However, the `var` rule is somewhat problematic. In the abstract, it says "derive `G |- J'` if `J` is in `G`", where `J` and `J'` are *different judgements*. This isn't 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?

### Reformulation 1: Hypothetical reductions

While a rule that says "derive `G |- J'` if `J` is in `G`" is suspicious, a rule that says
"derive `G |- J` if

`J`is in

`G`" 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

`var`is just an instance of hypothesis. In particular, whenever we assume a variable

`x trm`, we also

*assume*a derivation

`x => x`:

G ::= . | G , x trm,x => x x => x in G ----------- var G |- x => x G, x trm, x => x |- M => M' G |- N => N' ----------------------------------------- beta G |- (\x.M) N => M'[N'/x] G |- M => M' G |- N => N' -------------------------- app G |- (M N) => (M' N') G, x trm, x => x |- M => N --------------------------- lam G |- \x.M => \x.N

Now the `var` rule is unobjectionable. In the premies of the rules `beta` and `lam`, which deal with binding forms, the context is extended with the assumption that `x => x` for the bound variable `x`. The derivations of this version are isomorphic to the first definition of `G |- M => N`, but the `var` rule here has a more generally acceptable form.

The LF representation of this formulation is quite direct:

=> : trm -> trm -> type. %infix none 10 =>. =>/beta : (app (lam M) N) => M' N' <- ({x:trm} x => x -> M x => M' x) <- N => N'. =>/app : (app M N) => (app M' N') <- N => N' <- M => M'. =>/lam : lam M => lam M' <- ({x:trm} x => x -> M x => M' x). %block =>b : block {x : trm} {=>/x : x => x}. %worlds (=>b) (=> _ _).

Derivations using `var` are represented by LF variables representing the reduction assumptions in `G`. The Twelf `%worlds` declaration documents the form of `G` in our informal definition.

#### Substitution

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

- If
`G, x trm, x => x |- M => N`and`G |- M' trm`and`G |- M' => M'`then`[M'/x]M => [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 definition

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:

G ::= . | G , x trm ----------- refl G |- M => M G, x trm |- M => M' G |- N => N' --------------------------------- beta G |- (\x.M) N => M'[N'/x] G |- M => M' G |- N => N' -------------------------- app G |- (M N) => (M' N') G, x trm |- M => N ------------------- lam G |- \x.M => \x.N

In this case, this reformulation changes the structure of derivations (these are **not** isomorphic to what we started with) but does not change the relation defined by them, as reflexivity was admissible above. This reformulation clearly would not be an option if reflexivity were not admissible, as in the example of complete development (below).

The LF representation looks like this:

=> : trm -> trm -> type. %infix none 10 =>. =>/refl : M => M. =>/beta : (app (lam M) N) => M' N' <- ({x:trm} M x => M' x) <- N => N'. =>/app : (app M N) => (app M' N') <- N => N' <- M => M'. =>/lam : lam M => lam M' <- ({x:trm} M x => M' x). %block trmb : block {x : trm}. %worlds (trmb) (=> _ _).

### Reformulation 3 : tagged variables

(coming soon!)

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

G |- M ==> M' G |- N ==> N' (M is not a lambda) ------------------------------------------------ app G |- (M N) ==> (M' N')

How can we state this side condition more precisely? We need a judgement `notlam M` which holds whenever `M` is not `\x.M'`. It's easy to define this as a hypothetical judgement if we choose our contexts correctly:

G ::= . | G , x trm, notlam x notlam x in G ------------- G |- notlam x ----------------------- G |- notlam (app M1 M2)

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

Then complete development is easy to define:

G ::= . | G , x trm, notlam x, x ==> x x ==> x in G ------------ var G |- x ==> x G, x trm, notlam x, x => x |- M ==> M' G |- N ==> N' ----------------------------------------------------- beta G |- (\x.M) N ==> M'[N'/x] G |- M ==> M' G |- N ==> N' G |- notlam M -------------------------------------------- app G |- (M N) ==> (M' N') G, x trm, notlam x, x => x |- M ==> N ------------------------------------- lam G |- \x.M ==> \x.N

The LF representation is direct:

notlam : trm -> type. notlam/app : notlam (app _ _). %block nlb : block {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 Twelf `%worlds` declaration documents this fact, and causes Twelf to complain if we ever violate this convention.

Then complete development is a simple twist on parallel reduction:

==> : trm -> trm -> type. %infix none 10 ==>. ==>/beta : (app (lam M) N) ==> M' N' <- ({x:trm} notlam x -> x ==> x -> M x ==> M' x) <- N ==> N'. ==>/app : (app M N) ==> (app M' N') <- N ==> N' <- M ==> M' <- notlam M. ==>/lam : lam M ==> lam M' <- ({x:trm} notlam x -> x ==> x -> M x ==> M' x). %block ==>b : block {x : trm} {nlx : notlam x} {==>/x : x ==> x}. %worlds (==>b) (==> _ _).See Twelf's output

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 we have a complete development derivation `G , x trm, notlam x, x ==> x |- M ==> N`
and `G |- M' trm` and `G |- notlam M'` and ` G |- M' ==> M'`
then `G |- M[M'/x] ==> N[M'/x]`. The form of the context ensures that we need a derivation of `notlam M'` to make this substitution: 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.

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

Read more Twelf tutorials and other Twelf documentation.