Shallow versus Deep Embeddings When encoding a logic into a proof assistant such as Coq or Isabelle, a choice needs to be made between using a shallow and a deep embedding. In a shallow embedding logical formulas are written directly in the logic of the theorem prover, whereas in a deep embedding logical formulas are represented as a datatype. 


What are the advantages and
limitations of the various
approaches?
Are there any guidelines available for determining which to use? 
Is it possible to switch between the two representations in any systematic fashion?


As motivation, I would like to encode various security related logics into Coq and am wondering what the pros and cons of the different approaches are.
What are the advantages and limitations of the various approaches?



Pros of deep embeddings : You can prove and define things by induction on formulas' structure. Examples of interests are the size of a formula. 
Cons of deep embeddings: You have do deal explicitly with binding of variables. That's usually very laborious. 



  Are there any guidelines available for determining which to use ?


Shallow embeddings are very useful to import result proved in the object logic. For instance, if you have prove something in a small logic (e.g. separation logic) shallow
embeddings can be a tool of choice to import your result in Coq.

On the other side, deep embedding are almost mandatory when you want to prove 
meta-theorems about the object logic (like cut-elimination for instance).    


  Is it possible to switch between the two representations in any systematic fashion?


The idea behind the shallow embedding is really to work directly in a model of the object formulas. Usually people will maps an object formula P directly (using notations or by doing the translation by hand) to an inhabitant of Prop. Of course, there are inhabitants of Prop which cannot be obtained by embedding a formula of the object logic. Therefore you lose some kind of completeness. 

So it is possible to send every result obtained in a deep embedding setting through an interpretation function. 

Here is a little coq example: 


Inductive formula : Set :=
    Ftrue : formula
  | Ffalse : formula
  | Fand : formula -> formula -> formula 
  | For : formula -> formula -> formula.

Fixpoint interpret (F : formula) : Prop := match F with 
    Ftrue => True
  | Ffalse => False
  | Fand a b => (interpret a) /\ (interpret b)
  | For a b => (interpret a) \/ (interpret b)
 end.

Inductive derivable : formula -> Prop := 
    deep_axiom : derivable Ftrue
  | deep_and : forall a b, derivable a -> derivable b -> derivable (Fand a b)
  | deep_or1 : forall a b, derivable a -> derivable (For a b)
  | deep_or2 : forall a b, derivable b -> derivable (For a b).

Inductive sderivable : Prop -> Prop := 
    shallow_axiom : sderivable True 
  | shallow_and : forall a b, sderivable a -> sderivable b -> sderivable (a /\ b)
  | shallow_or1 : forall a b, sderivable a -> sderivable (a \/ b)
  | shallow_or2 : forall a b, sderivable b -> sderivable (a \/ b).

(* You can prove the following lemma: *)
Lemma shallow_deep : 
   forall F, derivable F -> sderivable (interpret F).

(* You can NOT prove the following lemma :*)
Lemma t : 
   forall P, sderivable P -> exists F, interpret F = P.