Graph-based proof counting and enumeration, with applications for

program fragment synthesis

Boris Yakobowski ENS Lyon

Joe Wells ULTRA Group Heriot-Watt University, Edinburgh

Goal: Term enumeration

▶ Given a type environment Σ = {x_{1} : A_{1}, ..., x_{n} : A_{n}} and a type A, is it possible to create a term of type A using the x_{i}, and combination methods such as function application

▶ If so, we want to enumerate all the different ways of getting this term

Setting: To be used by language of the ML family, but should be usable with any strongly-typed language.

We consider λ-calculus with pairs and injections.

Use

▶ [Haack+others ] AxML (Another Extended ML) Automatic generation of functions which satisfy semantic constraints

▶ [Di Cosmo+others ] Automatic composition of modules

Example

Type environment:

is = int stack
empty: is
push: (int * is) -> is
fold: ((int * is) -> is) -> is -> is -> is

Desired result type:

(is * is) -> is

Possible solutions:

function   -> empty
function ( , s) -> s
function (s, s') -> fold push s s'

Generalization

We would like to find the same solutions using the following (more general) type environment:

Type environment:

empty: 'a stack
push: ('a * ('a stack)) -> 'a stack
fold: (('a * 'b) -> 'b) -> 'b -> 'a stack -> 'b

Desired result:

(('a stack) * ('a stack)) -> 'a stack

Unfortunately, we do not reach (yet) this goal.

Possible approaches

Use of the Curry-Howard correspondence (propositions-as-types, proofs-as-programs): ▶ Existing results in type inhabitation ▶ Techniques from proof search

Type inhabitation

An algorithm exists: [Ben-Yelles , 1979].

But:

▶ For pure λ-calculus only.

▶ The algorithm is extracted from a proof, and is quite inefficient.

Type inhabitation is mainly concerned with deciding whether or not a type is inhabited (i.e. a type is inhabited if it is a true proposition), not really with finding its inhabitants.

Choosing the logic for proof search

▶ Natural deduction (NJ) ▷ Proofs hard to find automatically (bad) ▷ Bijection between normal proofs and terms in

normal form (good)

▶ Sequent calculus (LJ)

▷ Search is directed by the syntax of the

propositions (good) ▷ The association between normal proofs and

λ-terms in normal form is many-to-one (bad)

Best of both worlds

[Herbelin , 1995]: LJT

▶ Sequent calculus

▶ Proofs in bijection with simply typed λ-terms in normal form

Uses a stoup (containing either a formula or nothing) to focus the proof.

If the stoup is full, proof search can only work on its content.

Presentation of LJT

Propositional language: A := X | A → A | A ∨ A | A ∧ A

Rules: \overline{Γ; X ⊢ X} ^{Ax}  \frac{Γ, A; A ⊢ B}{Γ, A;_{•} ⊢ B} ^{Cont (A)} \frac{Γ;_{•} ⊢ A  Γ; B ⊢ C}{Γ; A→B ⊢ C} ^{ImpL}  \frac{Γ, A;_{•} ⊢ B}{Γ;_{•} ⊢ A→B} ^{ImpR}

4 other rules, for conjunctions and disjunctions, on the left and on the right.

Graphical representation of possible proofs

▶ s ∈ Sequents (triples of assumptions, stoup, goal)

▶ RA(s): rules applicable to s.

▶ VP = {(s, r) | s ∈ Sequents, r ∈ RA(s)} (“valid pairs”).

To help manage the search space, we use a graph G, with two kind of nodes. One of them is labelled by Sequents, the other by VP.

All possible proof trees are embedded in G.

G(s) is the smallest subgraph of G containing all the nodes accessible from s. Similarly, all possible proof trees for s are embedded in G(s).

Different versions of the calculus

We use two different versions of LJT:

1. LJT_{Set}, simplified version: environments are represented as sets of formulas

2. LJT_{MSet},“full” version: environments are represented as multisets of formulas

Everything previously seen is defined on both versions of the calculus.

We use the symbols Set and MSet as subscripts to indicate which version we’re using; 𝒮 ranges over Set and MSet.

Example: G_{𝒮}(s_{0}) for s_{0} = (X →X, X;_{•} ⊢ X)

[figure: Cont (X→X); s_{1} = (X→X, X; X→X ⊢ X); s_{0} = (X→X, X;_{•} ⊢ X); ImpL; 1; 2; Cont (X); s_{2} = (X→X, X; X ⊢ X); Ax]

\frac{\overline{X→X, X; X ⊢ X} ^{Ax}}{X→X, X;_{•} ⊢ X}_{Cont (X)}

\frac{\overline{X→X, X; X ⊢ X} ^{Ax}}{X→X, X;_{•} ⊢ X}_{Cont (X)}  \overline{X→X, X; X ⊢ X} ^{Ax}

X→X, X; X→X ⊢ X

ImpL

X→X, X;_{•} ⊢ X

Cont (X→X)

Proof search

▶ Breadth-first traversal of the graph, which is always possible.

▶ Proofs can be found in some connected subgraphs.

Problem: if the graph is infinite or cyclic, we can forever traverse subgraphs which contain no proof.

Infinite example

A subgraph of G_{MSet}(A;_{•} ⊢ Y) with A = (X →Y)→Y

[figure: A;_{•} ⊢ Y; Cont (A); A; A ⊢ Y; ImpL; 2; 1; A; Y ⊢ Y; ImpR; A;_{•} ⊢ X →Y; …; Ax; A, X;_{•} ⊢ Y; Cont (A); A, X; A ⊢ Y; ImpL; 2; 1; A, X; Y ⊢ Y; …; ImpR; A, X;_{•} ⊢ X →Y; …; Ax; A, X, X;_{•} ⊢ Y; …]

Optimizing breadth-first traversal

Before blindly searching for a proof, we find how many of them possibly exist (0, a finite number, an infinity).

Contribution:

▶ It is always possible to do so. The problem in the MSet case is quite hard, so we use the Set calculus as an oracle.

Mathematical approach:

C_{𝒮}(s), the number of proofs of s, verify simple polynomial equations. We solve the resulting system (obtained by walking G_{𝒮})

Example 1

[figure: Cont (X→X); s_{1} = (X→X, X; X→X ⊢ X); s_{0} = (X→X, X;_{•} ⊢ X); ImpL; 1; 2; Cont (X); s_{2} = (X→X, X; X ⊢ X); Ax] C_{𝒮}(s_{0}) = C_{𝒮}(s_{1}) + C_{𝒮}(s_{2}) C_{𝒮}(s_{2}) = 1 C_{𝒮}(s_{1}) = C_{𝒮}(s_{0}) × C_{𝒮}(s_{2}) C_{𝒮}(s_{1}) = C_{𝒮}(s_{1}) + 1

Mathematical solution: in ℕ ∪ {∞}, the only acceptable solution is {C_{𝒮}(s_{0}) = C_{𝒮}(s_{1}) = ∞, C_{𝒮}(s_{2}) = 1}.

Example 2

[figure: Cont (X→X); s_{4} = (X→X; X→X ⊢ X); s_{3} = (X→X;_{•} ⊢ X); ImpL; 1; 2; s_{5} = (X→X; X ⊢ X); Ax]

C_{𝒮}(s_{3}) = C_{𝒮}(s_{4}) C_{𝒮}(s_{5}) = 1 C_{𝒮}(s_{4}) = C_{𝒮}(s_{3}) × C_{𝒮}(s_{5})

C_{𝒮}(s_{3}) = C_{𝒮}(s_{3})

Mathematical solution:

{C_{𝒮}(s_{3}) = C_{𝒮}(s_{4}) = k, C_{𝒮}(s_{5}) = 1}, k ∈ ℕ ∪ {∞}

Solution using logical reasoning: all the proofs of s_{3} need another proof of s_{3}, so {C_{𝒮}(s_{3}) = C_{𝒮}(s_{4}) = 0, C_{𝒮}(s_{5}) = 1} (least solution).

Potential problem

The system of polynomials can be infinite if G_{𝒮}(s) is infinite.

But G_{Set}(s) is always finite (thanks to the subformula property). Also :

▶ C_{Set}(s) = 0 ⇔ C_{MSet}(s) = 0

▶ C_{Set}(s) = ∞ ⇔ C_{MSet}(s) = ∞

If C_{Set}(s) is finite and different from 0, the number of “useful” equations in the system of polynomials for C_{MSet}(s) is finite, and we can solve it normally.

Conclusion

▶ Efficient method for proof enumeration ▶ Full implementation, including for term

enumeration ▶ General method, which can be applied to other

calculi than LJT

Remaining to be explored: ▶ Polymorphism. ▶ Ruling out inefficient terms ▶ Recursivity

Adding polymorphism to the calculus

Goal: better support for the ML-like languages. Good news: there are already some rules in LJT

\frac{Γ; A[a/α] ⊢ B}{Γ; ∀α.A ⊢ B} ^{ForAll L}  \frac{Γ;_{•} ⊢ A}{Γ;_{•} ⊢ ∀α.A} ^{ForAll R}

But the rules are no longer syntax-directed (what should be put in place of α in ForAll L)?

Inefficient terms

We would like to avoid ML-terms such as:

1. Useless decomposition:

let f x y = match x with C1   -> y | C2   -> y

2. Decomposition previously done:

let f x = match x with
| C1 e1 -> (
    match x with
    | C1 e3 -> e3
    | C2 e2 -> e1)
| C2 e2 -> e2

Adding recursivity to the calculus

We need recursive types. It then becomes possible to model ML datatypes : μX. Y ∨ (int ∧ X) for int list, with one inhabitant for Y

▶ We really need to remove useless decompositions of disjunctions

▶ We must avoid non-terminating functions

▶ Better with polymorphism (′a list)