## Using reflection to improve automatization

May 13th, 2010 by gallaisLast 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

February 23rd, 2011 at 5:28 pm

Hi,

There is one thing that is still a bit unclear to me: in this example,

what does reflection add, as compared to just writing a plain Agda

interpreter for the target logic language?

I think I understand that using quoteGoal lessens the syntactic burden

on the programmer, but I don’t see clearly whether it also means that

there is a useful interaction between terms obtained through

reflection and the Agda type-checker, as you mention in your

introduction.

I’d be really grateful if you can enlighten me!