Shallow versus Deep Embeddings

Question

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.

Answer 1

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.

Answer 2

Roughly speaking, with a deep embedding of a logic, you (1) define a datatype representing the syntax for your logic, and (2) give a model of the syntax, and (3) prove that axioms about your syntax are sound with respect to the model. With a shallow embedding, you skip steps (1) and (2), and just start with a model, and prove entailments between formulas. This means shallow embeddings are usually less work to get off the ground, since they represent work you'd typically end up doing anyway with a deep embedding.

However, if have a deep embedding, it is usually easier to write reflective decision procedures, since you are working with formulas which actually have syntax you can recurse over. Also, if your model is strange or complicated, then you usually don't want to work directly with the semantics. (For example, if you use biorthogonality to force admissible closure, or use Kripke-style models to force frame properties in separation logics, or similar games.) However, deep embeddings will almost certainly force you to think a lot about variable binding and substitutions, which will fill your heart with rage, since this is (a) trivial, and (b) a never-ending source of annoyance.

The correct sequence you should take is: (1) try to get by with a shallow embedding. (2) When that runs out of steam, try using tactics and quotation to run the decision procedures you want to run. (3) If that also runs out of steam, give up and use a dependently-typed syntax for your deep embedding.

• Plan to take a couple of months on (3) if this is your first time out. You will need to get familiar with the fancy features of your proof assistant to stay sane. (But this is an investment which will pay off in general.)
• If your proof assistant doesn't have dependent types, stay at level 2.
• If your object language is itself dependently typed, stay at level 2.

Also, do not try to go gradually up the ladder. When you decide to go up the complexity ladder, take a full step at a time. If you do things bit-by-bit, then you will get lots of theorems which are weird and unusable (eg, you'll get multiple half-assed syntaxes, and theorems which mix syntax and semantics in strange ways), which you will eventually have to throw out.

EDIT: Here's a comment explaining why going up the ladder gradually is so tempting, and why it leads (in general) to suffering.

Concretely, suppose you have a shallow embedding of separation logic, with the connectives $A \star B$ and unit $I$. Then, you'll prove theorems like $A \star B \iff B \star A$ and $(A \star B) \star C \iff A \star (B \star C)$ and so on. Now, when you try to actually use the logic to prove a program correct, you'll end up having something like $(I \star A) \star (B \star C)$ and you'll actually want something like $A \star (B \star (C \star I))$.

At this point, you'll get annoyed with having to manually reassociate formulas, and you'll think, "I know! I'll interpret a datatype of lists as a list of separated formulas. That way, I can interpret $\star$ as concatenation of these lists, and then those formulas above will be definitionally equal!"

This is true, and works! However, note that conjunction is also ACUI, and so is disjunction. So you'll go through the same process in other proofs, with different list datatypes, and then you'll have three syntaxes for different fragments of separation logic, and you'll have metatheorems for each of them, which will inevitably be different, and you'll find yourself wanting a metatheorem you proved for separating conjunction for disjunction, and then you'll want to mix syntaxes, and then you'll go insane.

It's better to target the biggest fragment you can handle with a reasonable effort, and just do it.

Answer 3

It is important to understand that there is a spectrum from deep to shallow. You model the parts of your language deeply that should somehow participate in some inductive argument about the construction of it, the remainder is better left in the shallow see of direct semantics of the substrate of the logic.

For example, when you want to reason about Hoare Logic, you can model the expression language in a shallow manner, but the outline of the assign-if-while language should be a concrete datatype. You don't need to enter the structure of x + y or a < b, but you need to work with while etc.

In the other answers there were allusions to dependent types. This reminds of the ancient problem to represent languages with binders in a sane way, such that they are as shallow as possible, but still admit some inductive arguments. My impression is that the jury is still out judging about all the different approaches and papers that have emerged in the past 10-20 years on that subject. The "POPLmark challenge" for the different proof assistant communities was also about that to some extent.

Oddly, in classic HOL without dependent types, the HOL-Nominal approach by C. Urban worked quite well for shallow binding, although it did not catch up with the cultural shifts in these communities of programming-language formalization.