The newest release of Abella adds the support of schematic polymorphism without changing its theoretical underpinnings. The key ideas include the following:
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 TIt 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 :: nilwhere the parameterizing type variable
A of
nil and :: are inferred as (instantiated to)
int.
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.
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.
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.
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].
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:
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.
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.
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) ============================ falseThe 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,
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.