Walkthrough: subject reduction
In this walkthrough you will learn how to express specifications, state theorems, and conduct proofs. The example is the simply-typed lambda-calculus, and the theorem is subject reduction: evaluation preserves typing.
Introduction
Abella is designed for reasoning about the metatheory of programming languages and other logical systems that manipulate objects with binding. The simplest example of a programming language is the lambda-calculus, so we encode the semantics of evaluation and the typing rules for lambda-terms, and then show that the type of a term is not changed by evaluation.
Evaluation is defined by the following rules.
The first rule says that abstractions evaluate to themselves. The second rule says that an application is evaluated by evaluating the function component to an abstraction, substituting the argument component into the abstraction, and evaluating the result. The second rule assumes a notion of capture-avoiding substitution.
Typing judgments on lambda-terms are defined as follows.
These typing rules use a typing context that stores the binding for variables.
The first rule says that a variable x has type T if such a binding is in
the typing context. The second rule finds 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 implies that we must occasionally rename the bound
variable before applying the rule. The last rule types an application by
requiring the function component to have an arrow type and the argument
component to have the input type of that arrow.
The structure of Abella
Abella takes a two-level logic approach.
- The specification logic expresses inference rules such as those for evaluation and type assignment. Specifications in this logic have an executable interpretation, and execution traces correspond to derivations based on the rules.
- The reasoning logic expresses and proves properties about atomic predicates defined by the specification. Proofs naturally follow the execution traces in the specification logic.
When using Abella, distinguish between the logical system you want to specify and the properties you want to prove about it, and use the two logics accordingly. Both logics support a lambda-calculus representation of binding.
The executable specification
Abella's specification and reasoning logics are simply typed. Before
specifying evaluation and typing, introduce the types and terms used to
construct the objects and judgments. The following signature is saved in
eval.sig.
sig eval.
kind tm, ty type.
type app tm -> tm -> tm.
type abs (tm -> tm) -> tm.
type arrow ty -> ty -> ty.
type of tm -> ty -> o.
type eval, step, nstep tm -> tm -> o.
This signature declares two types, tm and ty, for terms and types. It
declares constructors such as app and abs.
The abs constructor takes an abstraction in the specification logic, so no
explicit constructor for variables is needed. For example,
abs (x\ abs (y\ app x y)) represents the term lambda x. lambda y. x y.
Finally, the signature declares the judgments eval, step, nstep, and
of. The type o 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 capture-avoiding substitution and implicit
renaming of bound variables. The rules for evaluation and typing are encoded
in eval.mod.
module eval.
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.
eval (abs R) (abs R).
eval (app M N) V :- eval M (abs R), eval (R N) V.
step (app (abs R) M) (R M).
step (app M N) (app M' N) :- step M M'.
nstep A A.
nstep A C :- step A B, nstep B C.
The first evaluation rule says that abstractions evaluate to themselves. The
second says that app M N evaluates to V if M evaluates to abs R and
R N evaluates to V. The term R is an abstraction at the specification
level, so bound variable names are not tracked and substitution is obtained by
applying R to N.
The typing rules use generic and hypothetical judgments. A generic judgment
introduces a new constant distinct from all other variables and constants. It
is written pi x\ G. A hypothetical judgment introduces a locally scoped
assumption, written H => G.
The abstraction rule therefore says that abs R has type arrow T U if, for
a fresh constant x assumed to have type T, the term R x has type U.
The application rule says that app M N has type T if, for some U, M
has type arrow U T and N has type U.
Reasoning
The specification is included with Abella in examples/lambda-calculus as
eval.sig and eval.mod. To follow along, work in that directory and start
Abella. The Specification command selects the specification to reason about.
$ abella
Welcome to Abella 2.1.0-dev.
Abella < Specification "eval".
Reading specification "./eval".
Abella <
The goal is subject reduction. State it as follows.
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 is a proof of {of V T}. The curly braces denote
specification-level provability in the reasoning logic: {A} is provable in
the reasoning logic exactly when A is provable in the specification logic.
============================
forall E V T, {eval E V} -> {of E T} -> {of V T}
Proceed by induction on the height of the derivation of {eval E V}. Since
this is the first component of the nested implication, use
induction on 1.
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 creates a new hypothesis IH, the inductive hypothesis. The
symbol * marks terms that are smaller than the original term, while @
marks a term equal in size to the one we started with. Decomposing
{eval E V}@ produces hypotheses marked with *, which can be used with the
inductive hypothesis.
Introduce the implications as hypotheses with intros. This also introduces
eigenvariables for the universally quantified variables.
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 perform case analysis on {eval E V}@ using case. This splits the proof
into two branches based on the two ways in which E can evaluate to V.
Each branch is a subgoal. Only the first subgoal is displayed in full.
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 rule that an abstraction evaluates to
itself. If this was the rule used, then E and V are both abs R for a new
eigenvariable R. The subgoal is trivial: search finds the goal among the
hypotheses.
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 application rule. If this was the last
rule used, then E is app M N for new eigenvariables M and N, and there
are derivations of {eval M (abs R)} and {eval (R N) V}. Those derivations
are shorter than the original hypothesis, so they are marked with * and are
candidates for the inductive hypothesis.
Before applying the inductive hypothesis, find the relevant typing judgments.
Case analysis on {of (app M N) T} produces only one subgoal, because there is
one typing rule for applications.
case H2.
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 gives typing judgments for both M and N. Apply the inductive
hypothesis to {eval M (abs R)}* and {of M (arrow U T)} to get a typing
judgment for abs R.
apply IH to H3 H5.
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}
The goal is now to obtain a typing judgment for R N, so that the inductive
hypothesis can be applied to get a typing judgment for V. A typing judgment
for N is already available, so decompose the typing judgment for abs R to
get a typing judgment for R. Case analysis again produces one subgoal.
case H7.
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 is a nominal constant: a fresh name introduced by a generic
judgment and distinct from every other name. The hypothesis
{of n1 U |- of (R n1) T} says that if n1 has type U, then R n1 has
type T. We can instantiate n1 with N. The inst tactic uses this
substitution property of the specification logic.
inst H8 with n1 = N.
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}. Combine them to get a
typing judgment for R N with no hypothetical assumptions. The cut tactic
implements the cut rule for the specification logic.
cut H9 with H6.
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 the new hypothesis, apply the inductive hypothesis to
{eval (R N) V}* and {of (R N) T}.
apply IH to H4 H10.
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, search completes the proof.
search.
Proof completed.
Moving forward
Try your own proofs. The following theorem states that evaluation is deterministic.
Theorem eval_det : forall E V1 V2,
{eval E V1} -> {eval E V2} -> V1 = V2.
Next, try to prove that the term abs (x\ app x x) cannot be assigned a
type.
Theorem of_self_app_absurd : forall T,
{of (abs (x\ app x x)) T} -> false.
Finally, prove that the self-application
app (abs x\ app x x) (abs x\ app 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.
Solutions to these problems, and the rest of the development, are in
examples/lambda-calculus/eval.thm in the Abella sources.
Once you have finished, continue with the advanced walkthrough, which uses definitions and lemmas.