# A Tutorial on Schematic Polymorphism in Abella

The newest release of Abella adds the support of schematic polymorphism without changing its theoretical underpinnings. The key ideas include the following:

• We allow terms, definitions and theorems to be parameterized by type variables. Those are called schematic terms, definitions and theorems, respectively. They represent their monomorphic counterparts under the instantiation of the parameterizing type variables with ground types. In other words, they function as schemata for generating terms, definitions and theorems in the logic of Abella under type instantiation.
• Given a schematic theorem, we restrict our attention to the construction of schematic proofs for it. Those are proof schemata parameterized by the same type variables parameterizing the theorem. By plugging in ground types for the parameterizing variables they become actual proofs for the instantiated theorem in the logic of Abella. In other words, the schematic proofs are ignorant of type information and their structures are stable under type instantiation.
• We apply the same idea to encode and reason about the specification logic and polymorphic program clauses. As a result, we are now able to prove properties of polymorphic specifications in λ-Prolog, as long as schematic proofs for these properties can be constructed.
We present a tutorial of schematic polymorphism in Abella. We assume that the reader is already familiar with the basics of Abella. If not, please consult the comprehensive Abella tutorial. In the subsequent sections, we first exhibit how the schematic terms, definitions, theorems and proofs work and then show how to reason about polymorphic programs written in λ-Prolog. In each section, we discuss the limitations of schematic polymorphism. All the discussions are driven by small examples that are (supposedly) easy to understand. The examples can be found here. For more technical details, please consult the accompanying paper and its website.

## Basics of Schematic Polymorphism

### Schematic terms

We allow type variables and type constructors that may take types as arguments in forming type expressions. The type constructor declaration now has the following form:

```Kind a   type -> ... -> type.
```
As an example, the type constructor for lists is the following which takes the type of list elements as an argument:
```Kind list   type -> type.
```
The type expression `list (list int) -> list bool` represents the type of functions from lists of lists of integers to lists of booleans.

We define constructors of terms as follows:

```Type c   T
```
It declares a schematic constant `c` whose type `T` is parameterized by the free type variables `A1,...,An` occurring in `T`. By plugging in ground types for `A1,...,An` in `T`, we get a constant `c` of the instantiated type. Note that when `T` does not contain any type variable, a normal constant `c` of type `T` is declared.

As an example, the schematic constants for constructing lists are defined as follows:

```Type nil  list A.
Type ::   A -> list A -> list A.
```
In fact, Abella has already built in the declarations of `list`, `nil` and `::`. So we do not need to explicitly declare them. As usual, `::` is used as an infix operator. As an example, the following term is a list of integers
```  1 :: 2 :: 3 :: nil
```
where the parameterizing type variable `A` of `nil` and `::` are inferred as (instantiated to) `int`.

### Schematic definitions

Given schematic terms, we construct schematic definitions parameterized by type variables. They stand for an infinite collection of definitions under the instantiation of the parameterizing type variables with ground types. As an example, the schematic definition for the append relation is as follows:

```Define append : list A -> list A -> list A -> prop by
append nil L L;
append (X :: L1) L2 (X :: L3) := append L1 L2 L3.
```
The definition is very much like that of the monomorphic append relation, except that `append` is a schematic constant whose type is parameterized by the type variable `A`. The whole definition is also parameterized by `A`. By instantiating `A` with ground types, we get the definitions of append for lists of these types. In this definition, `append` must be used at its most general type. That is, all the occurrences of `append` in the definition must have the type ```list A -> list A -> list A```. Note here the types of the constants `nil` and `::` are automatically inferred to be ```list A``` and `A -> list A -> list A` where A is the parameterizing type variable. Once `append` is defined, it can be used at any of its type instances.

### Schematic theorems

Given schematic definitions, we can state schematic theorems about them. For example, the following theorem describes that `append` is deterministic in its third argument.

```Theorem append_det[A] : forall (L1: list A) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
```
Note that the list of variables after the name of the theorem contains the type variables parameterizing the theorem. To help infer the correct type of the formula, we annotate `L1` with the type `list A`. To prove this theorem, we need to show it hold for all the type instances for `A`.

### Schematic proofs

We are only interested in constructing schematic proofs for a schematic theorem, which are parameterized by the same type variables of the theorem and, given any ground type instantiation, become actual proofs of the instantiated theorem by simply replacing the occurrences of type variables in them with the type instances given by the instantiation.

To construct schematic proofs, Abella ensures that every tactic in its successful application only employs the so-called schematic proofs rules to build up the proofs; these are proof rules whose shapes are stable under type instantiation and that coincide with the proof rules in the logic of Abella under ground type instantiation. When schematic proof rules are not applicable, the tactics that implement them will fail to apply and return an error message; the proof hence gets stuck. Most of the proof rules in the logic of Abella are immediately schematic by parameterizing them over type variables. The only non-trivial case is for the rule of case analysis, which is implemented by the `case` tactic. For this rule to be schematic, a type-generic solution to the unification problem incurred by case analysis must exist (see the paper for details). Abella finds type-generic unifiers by treating type variables as "black boxes" during case analysis (unification). It ensures that if its unification algorithm finds a solution without inspecting the structures of types for type variables, then the obtained solution is type-generic.

Continuing the example `append_det`, we observe that it can be proved by following the same proof by induction on the first assumption, no matter what type is substituted for `A`. In other words, the parameterizing type `A` is treated as a black box throughout the proof. Therefore, we guess that a schematic proof exists for `append_det`. Indeed, we can type in the following proof scripts in Abella to finish the proof for `append_det`:

```Theorem append_det[A] : forall (L1: list A) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H4. search.
```
The key to this proof is that case analyses do not inspect what type `A` could be when doing unification. We left the details of the proof for the readers to explore.

We can apply the schematic theorems at specific type instances. For example, the following special case of `append_det` at the type `o` is proved by applying `append_det`.

```Theorem oappend_det : forall (L1: list o) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
intros. apply append_det[o] to H1 H2. search.
```
Here, we explicitly provide the type instances for the parameterizing type variables of `append_det` in the `apply` tactic. The following is another example, which simply restates and proves `append_det`.
```Theorem append_det1[A] : forall (L1: list A) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
intros. apply append_det[A] to H1 H2. search.
```
When applying schematic theorems, we can omit the instances for their parameterizing type variables if they can be inferred from the context, as illustrated by the following examples.
```Theorem append_det2[A] : forall (L1: list A) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
intros. apply append_det[_] to H1 H2. search.

Theorem append_det3[A] : forall (L1: list A) L2 L3 L3',
append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
intros. apply append_det to H1 H2. search.
```

### Interplay with higher-order abstract syntax

We have seen how schematic polymorphism allows us to prove common properties of generic data structures. Another significant benefit is that it allows us to prove common properties about the structures of higher-order syntax and to apply them at arbitrary type instances. For example, given the following membership definition of lists:

```Define member : A -> list A -> prop by
member X (X :: L);
member X (Y :: L) := member X L.
```
we would like to prove that if a list does not depend on a nominal constant, then any dependency of its element on this nominal constant is vacuous. By exploiting higher-order abstract syntax, this property can be stated as the following theorem:
```Theorem member_prune[A,B] : forall M (L:list A), nabla (x:B),
member (M x) L -> exists M', M = y\M'.
```
We note that it has the same proof by induction on the only assumption which does not inspect the types for `A` and `B`. Therefore, it has a schematic proof, as follows:
```Theorem member_prune[A,B] : forall M (L:list A), nabla (x:B),
member (M x) L -> exists M', M = y\M'.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
```
Again, the key for getting a schematic proof is that case analysis (unification) treats `A` and `B` as black boxes.

We can apply `member_prune` at specific types for `A` and `B`, the following are some examples:
```Theorem olist_mem_prune : forall M (L:list o), nabla (x:o),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune[o,o] to H1. search.

Theorem member_prune1[A,B] : forall M (L:list A), nabla (x:B),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune[A,B] to H1. search.
```
Again, we can omit some or all type instances when using the `apply` tactic, as shown in the following examples:
```Theorem member_prune2[A,B] : forall M (L:list A), nabla (x:B),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune[_,B] to H1. search.

Theorem member_prune3[A,B] : forall M (L:list A), nabla (x:i),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune[_,i] to H1. search.

Theorem member_prune4[A,B] : forall M (L:list A), nabla (x:i),
member (M x) L -> exists M', M = y\M'.
intros. apply member_prune to H1. search.
```
We can use the `backchain` tactic to achieve similar effects:
```Theorem olist_mem_prune_bc : forall M (L:list o), nabla (x:o),
member (M x) L -> exists M', M = y\M'.
intros. backchain member_prune[o,o].

Theorem member_prune1_bc[A,B] : forall M (L:list A), nabla (x:B),
member (M x) L -> exists M', M = y\M'.
intros. backchain member_prune[A,B].
```

### Limitations of schematic polymorphism

It is not always possible to construct proofs schematically. For example, some schematic theorem may or may not have a proof depending on the type instances for its parameterizing type variables. As an example, given the following constant `p` and a schematic definition of equality `eq`:

```Type p   A -> o.

Define eq : A -> A -> prop by
eq M M.
```
The following proposition is not provable schematically.
```Theorem tst [A,B] : forall (X:A) (Y:B),
eq (p X) (p Y) -> false.
```
This is because its provability depends on whether `A` and `B` are instantiated to the same type:
• When `A` and `B` are different types, the two occurrences of `p` represent distinct constants. As such, the assumption is vacuously false and the proposition is indeed a theorem.
• When `A` and `B` are the same type, the two occurrences of `p` represent the same constant. As such, the assumption is true if `X = Y`. In this case, the proposition is not provable.
If we try to prove this proposition in Abella, we get stuck after applying the following tactics:
```intros. case H1.
```
in the following proof state with an error message:
```Error: Unification error during case analysis:
the generic type variable A cannot be instantiated

Variables: X Y
H1 : eq (p X) (p Y)
============================
false
```
The error message indicates that unification tries to inspect the structure of `A` which should be treated as a black box for a type-generic unifier to exist. Therefore, case analysis fails to apply schematically.

Via schematic polymorphism, we are able to encode a subset of the logic of λ-Prolog and polymorphic program clauses as a fixed-point definition in the logic of Abella. Through this encoding, we are able to reason about polymorphic programs written in λ-Prolog. This section demonstrates how it is done by walking through some examples and discusses the limitations of this approach. The technical details can be found in the accompanying paper.

Suppose we have the following λ-Prolog program which simply implements the append relation at the specification level.

```type app   list A -> list A -> list A -> o.

app nil L L.
app (X :: L1) L2 (X :: L3) :- app L1 L2 L3.
```
Here the occurrences of `app` in every clause have their most general type. Each clause represents an infinite collection of clauses obtained by instantiating the free type variables in the clause (in this example, there is only one free type variable in each clause).

We are able to prove properties about `app` just as we can for the simply typed version of it, as long as schematic proofs can be constructed. For example, the following theorem is easily proved by using `search`.

```Theorem app_search[A] : forall (X:A) L,
{app (X :: nil) L (X :: L)}.
search.
```
Here, the proof is finished by backchaining on the instances of the program clauses obtained by instantiating their only free type variable with the parameterizing variable `A`.

The following is a more complicated example which replays the deterministic theorem we discussed before for `app`:

```Theorem app_det[A] : forall (L1: list A) L2 L3 L3',
{app L1 L2 L3} -> {app L1 L2 L3'} -> L3 = L3'.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H4. search.
```
The structure of the proof is similar to `append_det`. Again, the key to this proof is how case analysis works. For case analysis of an object-level assumption to succeed, Abella requires that, for any program clause,
• either none of its type instances are unifiable with the assumption,
• or there is a unique instance of it that is unifiable with the assumption in a type-generic way and that is obtained by instantiating its free type variables with type expressions constructed using only the type variables parameterizing the theorem being proved.
The second condition implies that
• a unique instance of the program clause is used for type-generic case analysis,
• all the other instances are irrelevant,
• and no new type variables are introduced by case analysis.
From these implications, we can see that the set of parameterizing type variables are fixed and used as black boxes in case analysis. As a result, case analysis is schematic with respect to the parameterizing type variables.

To see an example when the above requirement is not satisfied, consider the following λ-Prolog program

```kind i     type.
type cst   A -> i.
type pred  i -> o.

pred (cst X).
```
In the clause for `cst` is used at its most general type. Thus, this clause has a free type variable which is also the type of `X`.

If we try to prove the following theorem using the given proof script:

```Theorem ty_not_fdet_left : forall M,
{pred M} -> false.
intros. case H1.
```
We get stuck at the following proof state with an error message:
```Error: Cannot fully infer the type of the program clause:
pred (cst X) :-

Variables: M
H1 : {pred M}
============================
false
```
The error message indicates that the type variable in ```pred (cst X)``` is not fully fixed, because when unifying `M` (which is of type `i`) with `cst X` we cannot uniquely determine the type of `X`. As a result, there are an infinite number of instances of `pred (cst X)` unifiable with `{pred M}`, violating the aforementioned requirement.

Backchaining on a program clause has a similar requirement. For example, we cannot prove the following theorem by using `search` because from the type of `M` we cannot fix the type of `X` in `pred (cst X)`.

```Theorem ty_not_fdet_right : forall M,
{pred M}.
search.
```

Last updated: