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 :
Term that represents the terms in AgdaquoteGoal t in e which has the typing rule: e[t := `T] : T ⊢ quote t in e : Tquote which gives you the internal representation of an identifierA 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:
Term and outputing a MyType element (preferably a non provable one if the Term has not a good shape)MyType term and outputing a MyTerm elementProving 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