Using reflection to improve automatization

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

One Response to “Using reflection to improve automatization”

  1. David Says:

    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!

Leave a Reply