September 2003 1/30

Reasoning about proof search specifications

Dale Miller INRIA/Futurs and École polytechnique

Outline

1. A new architecture for a theorem prover.

2. Proof search, logic programming, proof theory 3. A proof theoretic approach to definitions

4. A new quantifier ∇ (nabla)

5. Example: object-level provability

6. Example: π-calculus simulation

7. Conclusions

Traditional structure of theorem provers for reasoning about computation

(1) Implement mathematics • Choose among constructive mathematics, classical logic, set theory, etc.

• Provide abstractions such as sets and/or functions.

(2) Reduce computation to mathematics • via denotational semantics and/or

• via inductively defined data types for data and inference systems. What could be wrong with this approach? Isn’t mathematics the universal language? “Intensional aspects” of specifications — bindings, names, resource accounting, etc — generally require heavy encodings.

Roles of Logic in the Specification of Computation

In the specification of computational systems, logics are generally used in one of two approaches. Computation-as-model: Computations are mathematical structures representing computations via nodes, transitions, and states (for example, Turing machines, etc). Logic is used in an external sense to make statements about those structures. E.g. Hoare triples, modal logics. Computation-as-deduction: Pieces of logic are used to model elements of computation directly. Functional programming. Programs are proofs and computation is proof normalization (λ-conversion, cut-elimination). Logic programming. Programs are theories and computation is the search for (cut-free) sequent proofs. The dynamics of computation are encoded in the changes to sequents that occur during the search for a proof. A successful domain of logic programming is operational semantics.

Operational semantics of computation systems

OS is probably the dominate form of programming language semantic specification: used for both dynamic and static semantics. Operational semantics is generally given using inference rules. Below is an example rule specifying call-by-value evaluation:

{M ⇓ (abs R)  N ⇓ U  (R U) ⇓ V \atop (app M N) ⇓ V}

Such specifications have a natural and immediate connection to proof search (logic programming). For example, it is trivial to translate the above inference rule as a logic program clause (using λProlog syntax):

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

This connection means that the recent advances in proof search can often be translated into advances in the specification of operational semantics.

Advances in the proof search paradigm

Logic programming has been extended in recent years to encompass the following two extensions.

• Higher-order abstract syntax (HOAS) is captured with higher-type quantification and logic support for λ-terms. λProlog was the first programming language that incorporated HOAS. Specification languages, such as Isabelle and Twelf, also provide it.

• Linear logic (LL) greatly increases the expressiveness of logic programming, allowing direct and modular OS specification of state, exceptions, continuations, and concurrency in programming languages.

Forum is a presentation of all of higher-order linear logic as a logic programming language. It modularly extends the logical foundations of Prolog, λProlog, and Lolli.

HOAS and LL strain traditional theorem provers

Coding HOAS and LL into traditional mathematics is often complex and can obscure meaning.

• HOAS is really an approach to syntax.

– Encoding it using functions in a rich, higher-order logic is problematic: too many functions (exotic terms), extensional equality identifies too many terms, induction is difficult, etc.

– Encoding using first-order terms is problematic: one must re-implement many complex logical concepts (substitution, alpha-conversion, etc). The logic of binders is captured only indirectly.

• Encoding linear logic via semantics is difficult. Operational encodings, via multiset rewriting, ACI unification, etc, can generally capture only some aspects linear logic (additives/multiplicatives, quantifiers, modals, cut-elimination, etc).

A new architecture for a theorem prover

One meta-logic. This is a formalized replacement for mathematical reasoning, incorporating induction, co-induction, HOAS, and intuitionistic logic. Atomic judgments will include provability within an object-level logic. A few object-logics. Here, specifications are given as proof search specifications (logic programs) using such things as Horn clauses, or higher-order linear logic (e.g., Forum). Consider, for example, the π-calculus.

1. The one step transitions P ⟶^{A} P′ for the π-calculus is given by a simple logic program in an object-level logic (Horn clauses).

2. Simulation of P and Q is a meta-level predicate defined such that forall A and P′ if it is provable that P ⟶^{A} P′ then there exists a Q′ such that Q ⟶^{A} Q′ is provable and P′ is simulated by Q′.

Thus proving properties of simulation requires reasoning about the proof search specification in the object-level language.

Structure of the meta-logic

The meta-logic features the following.

• Intuitionistic logic (no linear logic at the “mathematics level”). Could be classical as well.

• Induction and co-induction are generally needed. These will not be discussed in this talk.

• A new quantifier ∇ will be used to provide a meta-level treatment of object-level eigenvariables.

• Object-level provability is specified via logic programs.

• Case analysis of how object-level judgments can be proved. The proof theoretic notion of definitions is used to address the last two points.

The sequent calculus in brief

A single-conclusion sequent is a triple written as Σ: Δ ⟶ G where Σ: The signature of this sequent: a set of eigenvariables used in the formulas G and Δ. Δ: The antecedent or left-hand side or program. G: The succedent or right-hand side or goal.

One way to understand the context Σ in the sequent

Σ: Δ ⟶ G

is that for every substitution for the variables in Σ, the sequent

Δθ ⟶ Gθ

is provable.

A proof theoretic notion of definition

A definition is a finite set of clauses

∀x̄[p_{1}(t̄_{1}) =^{△} B_{1}] … ∀x̄[p_{n}(t̄_{n}) =^{△} B_{n}] (n ≥ 0)

For i = 1, …, n, • p_{i} is a predicate constant,

• free variables of B_{i} are also free in the list t̄_{i}, and

• all variables free in t̄_{i} are contained in the list x̄_{i}. The formula B_{i} is the body and p_{i}(t̄_{i}) is the head of the i^{th} clause. The predicate symbols p_{1}, …, p_{n} are not distinct predicates: definitions act to define predicates by mutual recursion. The symbol =^{△} is not a logical connective: it is used just to denote definitional clauses. Using =^{△} directly as logical equivalence can damage proof search. We need something more clever.

Right introduction for defined atoms

Left and right introduction rules for atomic formulas are given for a fixed definition and equality theory.

{Δ ⟶ Bθ \atop Δ ⟶ A} def R, where A = Hθ for some clause ∀x̄.[H =^{△} B].

If we think of a definition as a logic program, then this rule is backchaining. Notice that (reading from bottom up)

• matching is used to select a clause from a definition, and

• the atom is replace by some body of a matching clause.

Left introduction for defined atoms

{Bθ, Δθ ⟶ Cθ | θ ∈ csu(A, H) for some clause ∀x̄.[H =^{△} B]}

A, Δ ⟶ C def L.

The variables x̄ need to be chosen so that they are not free in any formula of the lower sequent. This rule is due to [Eriksson 91]. The set of premises can be empty, finite, or infinite since definitions and the set csu(A, H) can be infinite. In some theories, minimal CSUs are not effectively computable. While the formal theory of definitions handles this general case, we shall only use this left rule when CSUs can be replaced with MGUs (most general unifiers). Notice that (reading from bottom up)

• unification is used to select a clause from a definition, and

• the atom is replace by all bodies of unifying clauses.

September 2003 13/30

Examples: 1 + 2 = 3 and 1 + 2 ≠ 1

Define addition on a simple encoding of natural numbers.

sum z N N =^{△} ⊤.
sum (s N) M (s P) =^{△} sum N M P.

We can prove that 1 + 2 = 3

\begin{matrix}{⟶ ⊤ \atop ⟶ sum z (s (s z)) (s (s z))} & def R \\ ⟶ sum (s z) (s (s z)) (s (s (s z))) \end{matrix} ; def R

and that 1 + 2 ≠ 1.

\begin{matrix}sum z (s (s z)) z ⟶ & def L \\ sum (s z) (s (s z)) (s z) ⟶ \end{matrix} ; def L

More generally, eigenvariables can be instantiated:

{Σ, n : Γ[n/m], ⊤ ⟶ G[n/m] \atop Σ, n, m : Γ, sum z n m ⟶ G} def L

September 2003 14/30

Example: evaluation of a conditional

Consider defining some rules for a conditional (if) in a functional programming language.

⋮
(if B M N) ⇓ V =^{△} B ⇓ true ∧ M ⇓ V.
(if B M N) ⇓ V =^{△} B ⇓ false ∧ N ⇓ V.
⋮

Now consider the following fragment of a proof

B ⇓ true , M ⇓ V ⟶ M ⇓ V B ⇓ true ∧ M ⇓ V ⟶ M ⇓ V ∧L B ⇓ false, M ⇓ V ⟶ M ⇓ V B ⇓ false ∧ M ⇓ V ⟶ M ⇓ V ∧L

(if B M M) ⇓ V ⟶ M ⇓ V def L

September 2003 15/30

Roles for def R and def L

⋮ ; ⟶ A def R corresponds to backchaining. ⋮ ; A ⟶ def L corresponds to finite failure. ⋮ ; A ⟶ B def L + def R corresponds to simulation^{†}.

† McDowell, Miller, and Palamidessi. Encoding transition systems in sequent calculus. TCS, 2001.

Restrictions on definitions

In general, cut can not be eliminated which out restrictions on definitions. Consider:

p =^{△} p ⊃⊥ .

The literature contains three ways to restriction definitions so that cut-elimination can hold.

1. Do not allow the body of definitions to contain implications. This is a rather strong restriction, but corresponds to Horn clauses. [Schroeder-Heister]

2. Remove contraction, which moves us away from intuitionistic logic to linear or relevant logics. [Girard, Schroeder-Heister]

3. Give predicates and formulas a level and require definitions to be stratified [McDowell & Miller].

The collapse of eigenvariables

A cut-free proof search of

∀x∀y.P x y

first introduces two new eigenvariables c and d and then attempts to prove P c d. Eigenvariables have been used to encode names in π-calculus [Miller93], nonces in security protocols [Cervesato, et. al. 99], reference locations in imperative programming [Chirimar95], etc. Since

∀x∀y.P x y ⊃ ∀z.P z z

is provable, it follows that the provability of ∀x∀y.P x y implies the provability of

∀z.P z z.

That is, there is also a proof where the eigenvariables c and d are identified. Thus, eigenvariables are unlikely to capture the proper logic behind things like nonces, references, names, etc.

A new quantifier ∇

The problem illustrated on the previous slide is that the eigenvariables c and d should be object-level eigenvariables and not meta-level eigenvariables. To fix this problem of scope, we introduce a new meta-level quantifier, ∇x.B x, and a new context to sequents. Sequents will have one global signature (the familiar Σ) and several local signatures, used to scope object-level eigenvariables.

Σ : B_{1}, …, B_{n} ⟶ B_{0}
⇓
Σ : σ_{1} ▷ B_{1}, …, σ_{n} ▷ B_{n} ⟶ σ_{0} ▷ B_{0}

Σ is a set of eigenvariables, scoped over the sequent and σ_{i} is a list of variables, locally scoped over the formula B_{i}. The expression σ_{i} ▷ B_{i} is called a generic judgment. Equality between judgments is defined up to renaming of local variables. See: Miller and Alwen Tiu, Encoding generic judgments in LICS03.

September 2003 19/30

Intuitionistic logic with ∇

Σ : B, Γ ⟶ B init  {Σ : Δ ⟶ B  Σ : B, Γ ⟶ C \atop Σ : Δ, Γ ⟶ C} cut
{Σ : B, B, Γ ⟶ C \atop Σ : B, Γ ⟶ C} cL  {Σ : Γ ⟶ C \atop Σ : B, Γ ⟶ C} wL
Σ : σ ▷ ⊥, Γ ⟶ B ⊥L  Σ : Γ ⟶ σ ▷ ⊤ ⊤R
{Σ : σ ▷ B_{i}, Γ ⟶ D \atop Σ : σ ▷ B_{1} ∧ B_{2}, Γ ⟶ D} ∧L  {Σ : Γ ⟶ σ ▷ B_{1}  Σ : Γ ⟶ σ ▷ B_{2} \atop Σ : Γ ⟶ σ ▷ B_{1} ∧ B_{2}} ∧R
{Σ : σ ▷ B_{1}, Γ ⟶ D  Σ : σ ▷ B_{2}, Γ ⟶ D \atop Σ : σ ▷ B_{1} ∨ B_{2}, Γ ⟶ D} ∨L  {Σ : Γ ⟶ σ ▷ B_{i} \atop Σ : Γ ⟶ σ ▷ B_{1} ∨ B_{2}} ∨R
{Σ : Γ ⟶ σ ▷ B  Σ : σ ▷ C, Γ ⟶ D \atop Σ : σ ▷ B ⊃ C, Γ ⟶ D} ⊃ L  {Σ : σ ▷ B, Γ ⟶ σ ▷ C \atop Σ : Γ ⟶ σ ▷ B ⊃ C} ⊃ R

The ∇ and ∀-quantifier

The ∇-introduction rules modify the local contexts.

{Σ : (σ, y_{γ}) ▷ B[y/x], Γ ⟶ C \atop Σ : σ ▷ ∇x_{γ}.B, Γ ⟶ C} ∇L  {Σ : Γ ⟶ (σ, y_{γ}) ▷ B[y/x] \atop Σ : Γ ⟶ σ ▷ ∇x_{γ}.B} ∇R

Since these rules are the same on the left and the right, this quantifier is self-dual. Both the global and local signatures are abstractions over their respective scopes. The universal quantifier rules are changed to account for the local context. (Rules for ∃ are simple duals of these.)

{Σ, σ ⊢ t : γ  Σ : σ ▷ B[t/x], Γ ⟶ C \atop Σ : σ ▷ ∀_{γ}x.B, Γ ⟶ C} ∀L  {Σ, h : Γ ⟶ σ ▷ B[(h σ)/x] \atop Σ : Γ ⟶ σ ▷ ∀x.B} ∀R

The familiar raising technique from higher-order unification is used to manage scoping of variables: if σ is x_{1}, …, x_{n} then (h σ) is (h x_{1} ⋯ x_{n}), where h is a higher-order variable of the proper type. Unification and matching in definitions is extended to these context by identifying local signature with λ-binders.

Some results involving ∇

\begin{matrix}∇x¬Bx ≡ ¬∇xBx & ∇x(Bx ∧ Cx) ≡ ∇xBx ∧ ∇xCx \\ ∇x(Bx ∨ Cx) ≡ ∇xBx ∨ ∇xCx & ∇x(Bx ⇒ Cx) ≡ ∇xBx ⇒ ∇xCx \\ ∇x∀yBxy ≡ ∀h∇xBx(hx) & ∇x∃yBxy ≡ ∃h∇xBx(hx) \\ ∇x∀yBxy ⇒ ∀y∇xBxy & ∇x.⊤ ≡ ⊤, ∇x.⊥ ≡ ⊥ \end{matrix}

Theorem. Given a fixed stratified definition, a sequent has a proof if and only if it has a cut-free proof. Theorem. Given a noetherian definition, the following formula is provable.

∇x∇y.B x y ≡ ∇y∇x.B x y.

Theorem. If we restrict to Horn definitions (no implication and negation in the body of the definitions) then

1. ∀ and ∇ are interchangeable in definitions,

2. ⊢ ∇x.B x ⊃ ∀x.B x for noetherian definitions.

Example: reasoning with an object-logic

The formula ∀u∀v[q ⟨u, t_{1}⟩ ⟨v, t_{2}⟩ ⟨v, t_{3}⟩] follows from the assumptions

∀x∀y[q x x y] ∀x∀y[q x y x] ∀x∀y[q y x x]

only if terms t_{2} and t_{3} are equal. Clear? Or were you thinking about the domain of interpretation of u and v? We would like to prove a meta-level formula like

∀x, y, z[pv (ˆ∀ u ˆ∀ v[q ⟨u, x⟩ ⟨v, y⟩ ⟨v, z⟩]) ⊃ y = z]

Example: reasoning with an encoded object-logic (cont)

We can encode provability of a first-order logic using the following definitions.

pv (ˆ∀ G) =^{△} ∇x.pv (Gx) pv A =^{△} ∃D.prog D ∧ inst D A
pv (G & G′) =^{△} pv G ∧ pv G′
inst (q X Y Z) (q X Y Z) =^{△} ⊤  prog (ˆ∀ x ˆ∀ y q x x y) =^{△} ⊤
inst (ˆ∀ D) A =^{△} ∃t. inst (D t) A prog (ˆ∀ x ˆ∀ y q x y x) =^{△} ⊤
X = X =^{△} ⊤  prog (ˆ∀ x ˆ∀ y q y x x) =^{△} ⊤

{Ξ_{1}  Ξ_{2}  Ξ_{3} \atop x, y, z : u, v ▷ pv (q ⟨u, x⟩ ⟨v, y⟩ ⟨v, z⟩) ⟶ y = z} ; x, y, z : pv (ˆ∀ u ˆ∀ v[q ⟨u, x⟩ ⟨v, y⟩ ⟨v, z⟩]) ⟶ y = z

Ξ_{1} : λuλv⟨u, x⟩ = λuλv⟨v, y⟩. Unification failure, so sequent is proved. Ξ_{2} : λuλv⟨u, x⟩ = λuλv⟨v, z⟩. Unification failure, so sequent is proved. Ξ_{3} : λuλv⟨v, y⟩ = λuλv⟨v, z⟩. Unifier [y ↦ z] yields new trivial sequent

x, z :⟶ z = z.

Example: encoding π calculus

π-calculus is a formal model for concurrency. The main entities are processes and names. The syntax is the following:

P := 0 | τ.P | x(y).P | x̄y.P | (P | P) | (P + P) | (x)P | [x = y]P

We pick the π-calculus because it is an interesting case where the conventional approach to encoding require complicated uses of side conditions involving names. Encoding the transition system for the π-calculus into HOAS has been know for a number of years and is pretty straightforward. For example: restriction (x)P is encoded using a constant of type (nm → proc) → proc. input x(y).P is encoded using a constant of type nm → (nm → proc) → proc.

Encoding π-calculus transitions

Processes can make transitions via various actions. There are three constructors for actions: τ : act for silent actions, ↓: nm → nm → act for input actions, and ↑: nm → nm → act for output actions. Following usual conventions: ↓ xy represents the action of inputting name y on channel x, and ↑ xy represents the action of outputting name y on channel x. The abstraction ↑ x : nm → act denotes outputting of an abstracted variable, and ↓ x : nm → act denotes inputing of an abstracted variable. Bound output is responsible for sending a locally bound variable outside its scope to other processes: scope extrusion. The one-step transition relation is encoded as two different predicates:

P ⟶^{A} Q A : act
P −⇀^{↓x} M bound input action, ↓ x : nm → act, M : nm → proc
P −⇀^{↑x} M bound output action, ↑ x : nm → act, M : nm → proc

September 2003 26/30

π-calculus: one step transitions

• Operational semantics:

x̄y.P \underrightarrow{x̄y} P OUTPUT−ACT  {P \underrightarrow{α} P′ \atop [x = x]P \underrightarrow{α} P′} MATCH  {P \underrightarrow{α} P′ \atop (y)P \underrightarrow{α} (y)P′} RES, y ∉ n(α)

• Encoding restriction using ∀ is problematic.

RES :  (x)P x ⟶^{α} (x)P′x =^{△} ∀x.(P x ⟶^{α} P′x)
OUTPUT − ACT : x̄y.P ⟶^{x̄y} P =^{△} ⊤
MATCH :  [x = x]P ⟶^{α} P′ =^{△} P ⟶^{α} P′

• Consider the process (y)[x = y]x̄z.0. It cannot make any transition, since y has to be “new”; that is, it cannot be x.

• The following statement should be provable

∀x∀Q∀α.[((y)[x = y](x̄z.0) ⟶^{α} Q) ⊃ ⊥]

September 2003 27/30

If restriction is translated to the meta-level ∀, then we need to prove

{x, z, Q, α} : ∀y.([x = y](x̄z.0) ⟶^{α} Q) ⟶ ⊥

There are at least two instantiations of variables that identify x and y:

1. y ↦ w, x ↦ w, α ↦ w̄z, Q ↦ 0: (wrong scoping)

{z} : ([w = w](w̄z.0) ⟶^{w̄z} 0) ⟶ ⊥

2. y ↦ x, α ↦ x̄z, Q ↦ 0: (newness assumption on y is violated)

{z} : ([x = x](x̄z.0) ⟶^{x̄z} 0) ⟶ ⊥

Scoping and newness are captured precisely by ∇:

\begin{matrix}\{x, z, Q, α\} : w ▷ ([x = w](x̄z.0) ⟶^{α} Q) ⟶ ⊥ & def L \\ \{x, z, Q, α\} : · ▷ ∇y.([x = y](x̄z.0) ⟶^{α} Q) ⟶ ⊥ \end{matrix} ; ∇L ; \{x, z, Q, α\} : · ▷ ((y)[x = y](x̄z.0) ⟶^{α} Q) ⟶ ⊥ ; def L ; \{x, z, Q, α\} :⟶ · ▷ ((y)[x = y](x̄z.0) ⟶^{α} Q) ⊃ ⊥ ; ⊃ R

The success of def L follows the failure of unification problem λw.x = λw.w.

Encoding simulation in the (finite) π-calculus

If the premises for the one step transition systems use ∇ instead of ∀, then simulation for the (finite) π-calculus is simply the following:

sim P Q =^{△} ∀A∀P′ \begin{matrix}[(P ⟶^{A} P′) ⇒ ∃Q′.(Q ⟶^{A} Q′) \\ ∧ sim P′ Q′] ∧ \end{matrix} ∀X∀P′ \begin{matrix}[(P −⇀^{↓X} P′) ⇒ ∃Q′.(Q −⇀^{↓X} Q′) \\ ∧ ∀w.sim (P′w) (Q′w)] ∧ \end{matrix} ∀X∀P′ \begin{matrix}[(P −⇀^{↑X} P′) ⇒ ∃Q′.(Q −⇀^{↑X} Q′) \\ ∧ ∇w.sim (P′w) (Q′w)] \end{matrix}

Deduction with this formula will compute simulation. This is a direct translation of the “official definition” but where names are handled entirely using scoping mechanisms of the meta-logic. There is a “cheap” λProlog program that will emulate this deduction and do “symbolic simulation”.

Future and related work

• Induction and co-induction fit naturally with definitions: simply specify which definitions should be considered least fixed points and which greatest fixed points. Doing this in the sequent calculus takes some care. See Momigliano and Tiu in TYPES 2003.

• Pitts and Gabbay have a “new name quantifier”. It is similar in that it is also self-dual and they are targeting similar applications as HOAS. It differs in most other respects.

• Alwen Tiu is constructing a prototype theorem prover for doing experiments, based on earlier work in Jérémie Wajs’s 2002 PhD.

• Carsten Schürmann is developing a meta-logical system for reasoning about LF specifications.

• Simon Ambler, Roy Crole, and Alberto Momigliano have used their Hybrid package in Isabelle/HOL to reason using definitions and HOAS.

• Do existing theorem provers allow for this style reasoning? Should a full scale implementation be undertaken?

Conclusion

• When computation is described via provability in the proof search paradigm, HOAS and linear logic can be used for expressive advantage.

• A few pieces of a meta-logic that should allow us to reason directly on provability of specifications was illustrated: in particular, definitions and ∇.

• When reasoning about HOAS specifications, something like ∇ seems required. We have no examples of ∇ that do not involve HOAS.

• The main area of application of these ideas seem to be in the operational semantic specifications of rich, symbolic systems (programming languages, specification languages, security protocols, type systems, etc).

Names

Reprose from REasoning about PROof SEarch. Prosea from PROof SEArch, but this is taken by a maritime lobbying group. Sarah since Paulson named his prover after Huet’s daughter. LINC for lambda, induction, nabla, and co-induction (Tiu). Also stands for “LINC is not Coq”.