by *gallais* on **May 13, 2010**.

Tagged as: Lunches.

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.

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

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].

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.

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 ∷ []) _`

[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

comments powered by Disqus