In this walkthrough you will learn...

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

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.

Typing judgments on lambda-terms are defined as follows.

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.

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.

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 %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.abellaWelcome to Abella 2.0.0 Abella <Specification "eval".Reading specification eval Abella <

Abella <This theorem says that for all proofs ofTheorem sr_eval : forall E V T, {eval E V} -> {of E T} -> {of V T}.

`{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 <The system has created a new hypothesis calledinduction 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}

`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 <Now we perform case analysis onintros.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}

`{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 sr_eval <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 derivecase 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}

`{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 <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 derivesearch.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}

`{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 <This case analysis has given us typing judgments for bothcase 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}

`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 <Looking ahead, our goal is to get a typing judgment forapply 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}

```
(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 <Thecase 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}

`n1`

here represents a `{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 <We now knowinst 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}

`{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 <With our new hypothesis, we can apply the inductive hypotheses tocut 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}

`{eval (R N) V}*`

and `{of (R N) T}`

to get the
proper typing judgment for `V`

.
sr_eval <Finally, the search tactic completes the proof.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}

sr_eval <search.Proof completed.

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.