Walkthrough: Subject Reduction

In this walkthrough you will learn...

• How to express specifications
• How to state theorems
• How to conduct proofs

Introduction

Abella is designed for reasoning about the meta-theory of programming languages and other logical systems which manipulate objects with binding. The simplest example of a programming language is the lambda-calculus, so in this walkthrough we'll encode the semantics of evaluation in the lambda-calculus as well as typing rules for lambda-terms. We'll then show that the type of a term is not changed by evaluation. This is called subject reduction.

Before we start using Abella, we recall the rules for evaluation and typing of lambda-terms. Evaluation is defined by the following rules.

The first rule says abstractions evaluate to themselves. The second rule says applications are evaluate by evaluating the function component to an abstraction, substituting the argument component into abstraction, and evaluating the result. Notice that the second rule assumes a notion of capture-avoiding substitution.

Typing judgments on lambda-terms are defined as follows.

These typing rules make use of a typing context which stores the binding for variables. The first rule says that a variable x has type T if we find such a binding in the typing context. The second rule says that we find the type of an abstraction by assuming a type for its variable while finding a type for the body. The resulting type is an arrow from the type of the variable to the type of the body. The side condition here implies that we must occasionally rename the bound variable x before we can apply the rule. The last rule says that an application is typed by determining the function component has an arrow type and the argument component has a type which matches the input of this arrow type. The resulting type is then the output of the arrow type.

A note about the structure of Abella

Abella takes a two-level logic approach.

• The specification logic is used to express inference rules of the kind shown for evaluation and type assignment above; these rules are known as structural operational semantics rules. Specifications in this logic can be given an executable interpretation and execution traces generated in this way correspond naturally to derivations based on the structural operational semantics rules.
• The reasoning logic is used to express and prove properties about atomic predicates that are defined by specifications provided through the specification logic. The proof of such properties leads naturally to a style of argument that is based on the execution traces in the specification logic. Thus the properties that are proved are essentially ones about the logical system described by structural operational semantics rules.

When you use Abella, you should distinguish between the logical system you want to specify and the properties you want to prove about that system, and you should use the two separate logics to encode these. Another important feature of Abella is that it supports a lambda-calculus based representation of binding in the objects of the logical system which is described. This support is provided in both the specification logic and the reasoning logic.

Executable Specification

Abella's specification and reasoning logics are simply-typed. Before we can specify the rules for evaluation and typing for the lambda-calculus we must first introduce the types and terms used to construct the objects from and judgments over the lambda-calculus. This is done via the following signature which we assume is saved in the file eval.sig.

sig eval.

kind    tm, ty     type.

type    i          ty.
type    arrow      ty -> ty -> ty.

type    app        tm -> tm -> tm.
type    abs        (tm -> tm) -> tm.

type    eval       tm -> tm -> o.
type    of         tm -> ty -> o.

This signature declares that we have two types called tm and ty for representing the terms and types of the lambda-calculus, respectively. It then declares a base type called i and a constructor for function types called arrow. Terms are constructed as either applications using app or abstractions using abs. Note that the abs constructor takes a single argument which is an abstraction in the specification logic so we do not need an explicit constructor for variables. Instead, the specification logic's notion of binding is used to model the binding behavior of our lambda-calculus specification. For example, the term λx.λy.xy is represented by abs (x\ abs (y\ app x y)) where x\ ... is the syntax of an abstraction in the specification logic. Finally, this signature declares that we will form two judgments called eval for evaluation and of for typing. The type o in these declarations is the type of formulas in the specification logic.

Abella uses a Prolog-like specification logic that treats binding as a fundamental notion and provides operators for manipulating binding, such as capture-avoiding substitution and the implicit renaming of bound variables. The rules for evaluation and typing can be encoded in this specification logic via the following module which we assume is saved in the file eval.mod.

module eval.

eval (abs R) (abs R).
eval (app M N) V :- eval M (abs R), eval (R N) V.

of (abs R) (arrow T U) :- pi x\ (of x T => of (R x) U).
of (app M N) T :- of M (arrow U T), of N U.

The first rule for evaluation says abstractions evaluate to themselves. The second rule says an application (app M N) evaluates to V if there exists an R such that M evaluates to (abs R) and (R N) evaluates to V. An important point is that the term R in (abs R) is an abstraction at the specification level. Thus we do not need to keep track of bound variable names for abstractions, and we also get capture-avoiding substitution "for free" in the second rule by applying R to N.

The rules for typing use two more features of our specification logic: generic and hypothetical judgments. A generic judgment introduces a new constant which is distinct from all other variables and constants. We use this when encoding the typing rule for abstractions since it allows us to generate a variable which we know for sure cannot already be in the typing context. In syntax, the generic judgment is denoted by pi x\ G where x is the new constant and G is the goal to prove. A hypothetical judgment introduces a locally scoped assumption under which another goal is proven. We use the hypothetical judgments of our specification logic to keep track of typing assumptions for variables rather than using an explicit context. The hypothetical judgment is written H => G where H is assumed while proving G.

With this understanding, we can read the first typing rule as saying an abstraction (abs R) has type (arrow T U) if for some fresh constant x which we assume has type T we can prove (R x) has type U. The second rule says an application (app M N) has type T if there exists a U such that M has type (arrow U T) and N has type U.

You may wonder if our encoding of the evaluation and typing rules is faithful to the original specification. This property is known as adequacy and has been addressed for similar systems in the past. See, for example, this paper which shows adequacy for a deductive system encoded in a specification logic like ours. An important point to note here is that the use of lambda-tree syntax in capturing binding properties in the specification logic makes it easy to prove adequacy properties. We will stop in this walkthrough with the observation that adequacy can be proved for our encodings; we will not actually provide such proofs since our present objective is more to illuminate the capabilities Abella provides for reasoning about specifications once they have been accepted.

Reasoning

You are encouraged to follow along with this development explicitly using the Abella system. The specification is already included with Abella in the directory examples/lambda-calculus as the files eval.sig and eval.mod. If you make a mistake while following along, type "undo." to go back. If you haven't yet downloaded Abella, you can get the source or for Windows a binary package is available. Compiling the source requires an installation of OCaml.

To begin reasoning, we navigate to the directory which contains our specification and start Abella (it helps if abella is in your path). Then we use the Specification command to indicate which specification we are going to reason about. The text in bold is what you will enter.

~/abella/examples/lambda-calculus % abella
Welcome to Abella 2.0.0
Abella < Specification "eval".
Reading specification eval

Abella <

Recall our goal is to prove subjection reduction, i.e. that evaluation preserves the type of a lambda-term. We can state this in Abella as follows.

Abella < Theorem sr_eval : forall E V T,
           {eval E V} -> {of E T} -> {of V T}.

This theorem says that for all proofs of {eval E V} and all proofs of {of E T} there exists a proof of {of V T}. The curly braces are the predicate in the reasoning logic denoting specification logic provability: in particular, {A} is provable in the reasoning logic if and only if A is provable in the specification logic.

  ============================
   forall E V T, {eval E V} -> {of E T} -> {of V T}

To prove this goal, we'll use induction on the height of the derivation of {eval E V}. We tell the system to induct using the induction tactic, and, since we want to induct according to the first component of the nested implication above, we call this "induction on 1."

sr_eval < induction on 1.


  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  ============================
   forall E V T, {eval E V}@ -> {of E T} -> {of V T}

The system has created a new hypothesis called IH (for Inductive Hypothesis). The symbol * denotes that this inductive hypothesis can only be used on terms which are smaller than the original term. The symbol @ in the goal denotes that this term is equal in size to what we started with. Later, when we decompose the term {eval E V}@ we will get "smaller" hypotheses with * which can then be used with the inductive hypothesis.

The next step is to introduce the implications in the goal as new hypotheses. We can do this using the intros tactic which introduces eigenvariables to stand for the universally quantified variables and new hypotheses for the nested implications.

sr_eval < intros.

  Variables: E, V, T
  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  H1 : {eval E V}@
  H2 : {of E T}
  ============================
   {of V T}

Now we perform case analysis on {eval E V}@ using the case tactic. This will split the proof into two branches based on the two possible ways in which E can evaluate to V. Each of the different proof branches is called a subgoal. In general, only the first subgoal will be displayed in full; the other subgoals will be shown without their hypotheses. When the first subgoal is completed, the prover will move to the next subgoal.

sr_eval < case H1.
Subgoal 1:

  Variables: E, V, T, R
  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  H2 : {of (abs R) T}
  ============================
   {of (abs R) T}

Subgoal 2 is:
 {of V T}

The first subgoal corresponds to the first specification rule for eval which says that an abstraction evaluates to itself. If this was the rule used to derive {eval E V} then it must be that E and V are equal to (abs R) for some new eigenvariable R. The proof of this subgoal is now trivial. The search tactic will complete the proof by finding the goal as one of the hypotheses.

sr_eval < search.
Subgoal 2:

  Variables: E, V, T, R, N, M
  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  H2 : {of (app M N) T}
  H3 : {eval M (abs R)}*
  H4 : {eval (R N) V}*
  ============================
   {of V T}

The second subgoal corresponds to the second specification rule for eval which expresses how applications are evaluated. If this was the last rule used to derive {eval E V} then it must be that E is equal to (app M N) for new eigenvariables M and N. Looking at the body of the second specification rule for eval, we can see that it must also be the case that there exist derivations for {eval M (abs R)} and {eval (R N) V} for some new R. Thus these become new hypotheses in the proof. Since the derivations of these judgments are shorter than the original hypothesis, they have a * to signify that they are candidates for the inductive hypothesis.

Before we can apply the inductive hypothesis, we need to find relevant typing judgments. We get these by performing case analysis on {of (app M N) T}. This case analysis will result only in one subgoal since there is only one specification rule for typing applications.

sr_eval < case H2.
Subgoal 2:

  Variables: E, V, T, R, N, M, U
  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  H3 : {eval M (abs R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arrow U T)}
  H6 : {of N U}
  ============================
   {of V T}

This case analysis has given us typing judgments for both M and N. Now we can now use the apply tactic to apply the inductive hypotheses to {eval M (abs R)}* and {of M (arrow U T)} to get a typing judgment for (abs R).

sr_eval < apply IH to H3 H5.
Subgoal 2:

  Variables: E, V, T, R, N, M, U
  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  H3 : {eval M (abs R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arrow U T)}
  H6 : {of N U}
  H7 : {of (abs R) (arrow U T)}
  ============================
   {of V T}

Looking ahead, our goal is to get a typing judgment for (R N) so that we can apply the inductive hypothesis to get a typing judgment for V. We already have a typing judgment for N, so the next step is to decompose our typing judgment for (abs R) in order to get a typing judgment for R. Again, case analysis will result in only one subgoal since there is only one typing rule for abstractions.

sr_eval < case H7.
Subgoal 2:

  Variables: E, V, T, R, N, M, U
  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  H3 : {eval M (abs R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arrow U T)}
  H6 : {of N U}
  H8 : {of n1 U |- of (R n1) T}
  ============================
   {of V T}

The n1 here represents a nominal constant which we can think of as a placeholder for any term except another nominal constant (see this paper for a precise explanation of the logical nature of such constants). Now, the hypothesis {of n1 U |- of (R n1) T} roughly says that if any term n1 has type U then we can conclude (R n1) has type T. Obviously, we can instantiate n1 with N. The inst tactic acts on this property of our specification logic.

sr_eval < inst H8 with n1 = N.
Subgoal 2:

  Variables: E, V, T, R, N, M, U
  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  H3 : {eval M (abs R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arrow U T)}
  H6 : {of N U}
  H8 : {of n1 U |- of (R n1) T}
  H9 : {of N U |- of (R N) T}
  ============================
   {of V T}

We now know {of N U} and {of N U |- of (R N) T}. The next step is to combine these two judgments to get a typing judgment for (R N) which does not have any hypothetical judgments. We realize this through the cut tactic which implements the cut rule for our specification logic.

sr_eval < cut H9 with H6.
Subgoal 2:

  Variables: E, V, T, R, N, M, U
  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  H3 : {eval M (abs R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arrow U T)}
  H6 : {of N U}
  H8 : {of n1 U |- of (R n1) T}
  H9 : {of N U |- of (R N) T}
  H10 : {of (R N) T}
  ============================
   {of V T}

With our new hypothesis, we can apply the inductive hypotheses to {eval (R N) V}* and {of (R N) T} to get the proper typing judgment for V.

sr_eval < apply IH to H4 H10.
Subgoal 2:

  Variables: E, V, T, R, N, M, U
  IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
  H3 : {eval M (abs R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arrow U T)}
  H6 : {of N U}
  H8 : {of n1 U |- of (R n1) T}
  H9 : {of N U |- of (R N) T}
  H10 : {of (R N) T}
  H11 : {of V T}
  ============================
   {of V T}

Finally, the search tactic completes the proof.

sr_eval < search.

Proof completed.

Moving Forward

For those who are following this development using Abella, you are encouraged to try your own proofs. The following theorem states that evaluation is deterministic. Why don't you prove it?

Theorem eval_det : forall E V1 V2,
  {eval E V1} -> {eval E V2} -> V1 = V2.

Next try to prove that the term (λx. x x) cannot be assigned a type.

Theorem of_self_app_absurd : forall T,
  {of (abs (x\ app x x)) T} -> false.

Finally, it is also possible to prove that the term (λx. x x) (λ x. x x) does not evaluate to a value.

Theorem no_eval : forall V,
  {eval (app (abs x\ app x x) (abs x\ app x x)) V} -> false.

If you get stuck on any of these, the solutions to these problems and others related to the lambda-calculus are available in examples/lambda-calculus/eval.thm.

Once you've finished, it's time to move on to bigger and better things. In the advanced walkthrough you'll see more sophisticated reasoning which uses definitions and lemmas.