Archive for May, 2010

Using reflection to improve automatization

Thursday, May 13th, 2010 by gallais

Last week I talked about a solver for propositional logic that uses reflection. This work is the opportunity to present how one shall develop a solver using reflection.

Reflection

The purpose of reflection is being able to manipulate terms of the language inside the language itself. It allows you to design certified solvers whereas the use of a MetaLanguage (Ltac for example) doesn’t guarantee anything.

Since AIM XI, the latest version of Agda has a couple of new features. One of them is the possibility for the user to have access to the current goal [1]. From now, you can use :

  • A datatype Term that represents the terms in Agda
  • A command quoteGoal t in e which has the typing rule: e[t := `T] : T ⊢ quote t in e : T
  • A command quote which gives you the internal representation of an identifier

A solver will be designed in three steps. Let’s say that the type MyType will represent the set of goals that you want to deal with and that MyTerm will be the representation of the inhabitants of MyType. We need to:

  • Add a proper quoting function taking a Term and outputing a MyType element (preferably a non provable one if the Term has not a good shape)
  • Design the solver taking a MyType term and outputing a MyTerm element
  • Give the semantics of our datatypes and prove the soundness of our solver

A solver for propositional logic

Proving a formula of propositional logic is the same (thanks to Curry-Howard’s isomorphism) as finding a lambda term which is an inhabitant of the corresponding type. Our work is based on the (said to be “structural” but not in Agda’s sense) deduction rules presented in a paper by Roy Dyckhoff and Sara Negri [2].

Implementation

The “MyType” datatype:

data Type : ℕ → Set where
atom : ∀ {n} → Fin n → Type n
⊥ : ∀ {n} → Type n
_∩_ _⊃_ _∪_ : ∀ {m} → Type m → Type m → Type m

The “MyTerm” datatype is more verbose but pretty straight-forward so I won’t include it here. It contains all the basic constructors for this simply-typed lambda caculus with sum and product types (var, lam, app, inj1, inj2, case, proj1, proj2, and).

The only tricky thing is the lift function that lifts all the free variables of a given term because it has to deal with modifications of the environment when going under a lambda.

Interface

The issue of partiality (the formula is maybe not provable) is solved by using dependent types: the solver requires un argument that will either have the type ⊤ if the proposition is provable (the placeholder tt is then inferred by agda) or have the same type as the goal if it is not provable.

Example of the use of the solver:


Ex : ∀ {A B C D : Set} → ((A → B) × (C → A)) → (A ⊎ C) → B × (((A → D) ⊎ D) → D)
Ex {A} {B} {C} {D} = quoteGoal t in solve 4 t (A ∷ B ∷ C ∷ D ∷ []) _

References

[1] See Agda/test/succeed/Reflection.agda and Agda/doc/release-notes/2-2-8.txt

[2] Roy Dyckhoff and Sara Negri, Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic, http://www.jstor.org/stable/2695061

You can get the source code on the following darcs repository: darcs get http://patch-tag.com/r/gallais/agda

Solving first order stream equations

Monday, May 10th, 2010 by fyb

I presented a solver for first order stream equations. Those are simple equations of the form:

 x = 2 :: head (tail x) :: head (3 :: head x :: x) :: tail (4 :: x)

The solver is parametric in the domain type. It turns out that unless the domain is empty, those equations always have solutions. Given a term representing the right hand side of an equation, it builds a template which is a finite representation of its solutions. A template is instantiated by providing an environment in which the under-constrained elements of the stream get a value.

There are two steps: first reduce the term to a normal form by eliminating redexes:

  • head (d :: s) reduces to d
  • tail (d :: s) reduces to s

Then, solve the problem for normal forms. An equation whose right hand side is in normal form looks like:

 x = d_1 :: ... :: d_n :: tail^j x

where the d_i are either constants from the domain or equal to some element x_k of the stream x.

We get n equations: x_i = d_i. We get also a condition on the rest of the stream: if j = n, then there is no constraint on the remaining elements of the solutions (after the n-th), otherwise, there will be a loop of length abs(n-j).

Solving the n conditions boils to extracting the strongly connected components of a graph whose vertices are the x_1 ... x_n and the edges are the dependencies between them. The problem is actually simpler than the general one because each vertex is target of at most one edge.

I implemented such an algorithm in Agda but chickened out from writing the proofs in Agda that the algorithm produced a template whose instances are exactly the solutions of the given equation. I wrote the proofs in English instead.