6
$\begingroup$

I'm unclear on the terms "deep embedding" and "shallow embedding". I understand they are concerned with using one logic inside another, e.g. using Metamath/set.mm proofs in Lean or building Coq inside Coq. I also get the impression that deep embeddings involve some sort of re-implementation, whereas shallow embeddings do not.

I'm looking for the following:

$\endgroup$

1 Answer 1

12
$\begingroup$

The terms "deep" and "shallow" embedding are somewhat informal and have many variations. I will explain the essentials only.

An embedding from a source language $S$ to a target language $T$ is shallow if the constituent parts of $S$ are translated (mostly) directly to the corresponding parts of $T$. This is useful when we want to use $S$ but all we have is $T$. For example, if $S$ is a domain-specific logic and $T$ is a full-fledged proof assistant, we encode $S$ using the logic of $T$ and then use $T$'s theorem proving abilities to prove $S$-theorems. Even more specifically, suppose $S$ is the classical propositional calculus and $T$ is a proof assistant based on constructive type theory, equipped with a tactic for proving intuitionistic propositions. We can shallowly translate $S$ into $T$ using the double-negation translation and use $T$'s tactic to prove classical $S$-statements.

An embedding is deep if in $T$ we define (inductive) types that describe the syntax and inference rules of $S$. This is useful when we want to use $T$ to study $S$ as a formal system. For example, if $S$ is a programming language and $T$ is a full-fledged proof assistant, we can define in $T$ types that represent the syntax, the typing rules, and the operational semantics of $S$. This allows us to prove theorems about $S$, such as type safety. (In fact, this was one of successful early applications of proof assistant technology.)

Example: simply-typed $\lambda$-calculus

Suppose $S$ is the simply typed $\lambda$-calculus with the following parts:

  • the types of natural numbers nat
  • function types, written a ⇒ b
  • constructors zero and succ
  • $\lambda$-abstraction $\lambda (x{:}A),\, e$ and application $e_1 \, e_2$.

There are also typing contexts and typing rules which I am not going to write here, as they are quite standard (and also formalized below as a deep embedding in Agda).

Shallow embedding

The following is a shallow embedding of the calculus in Agda. It is mostly just a collection of abbreviations, so that we can write nat instead of Agda's , and A ⇒ B instead of Agda's A → B, etc.

(Note: the embedding shown below is not as shallow as it could be, because we map the typing contexts of λ-calulus to types in Agda. An even shallower embedding would map contexts to contexts, but that would be a bit confusing to beginners because most of the embedding would become invisible.)

module Shallow where

  open import Data.Nat
  open import Data.Product
  open import Data.Unit

  -- The types of the λ-calculus are Agda's types.
  type = Set

  -- The typing contexts are sets.
  context = Set

  -- The empty context is the unit type
  ∙ : context
  ∙ = ⊤

  -- Extending a context with type is Agda's cartesian product
  infixl 5 _⨟_
  _⨟_ : context → type → context
  Γ ⨟ A = Γ × A

  -- The λ-calculus type nat is Agda's type ℕ
  nat : type
  nat = ℕ

  -- The λ-calculus function type is Agda's function type
  infixr 7 _⇒_
  _⇒_ : type → type → type
  A ⇒ B = A → B

  -- The λ-calculus typing judgement x : nat, f : nat ⇒ nat, y : nat ⊢ succ (succ x) : nat
  example-1 : (∙ ⨟ nat ⨟ nat ⇒ nat ⨟ nat) → nat
  example-1 (((_ , x) , f) , y) = suc (suc x)

  -- The λ-calculus typing judgement ∙ ⊢ (λ (x y : nat) succ x) (succ (succ 0))
  example-2 : ∙ → nat ⇒ nat
  example-2 tt = (λ (x y : nat) → suc x) (suc (suc 0))

  -- The λ-calculus typing judgement f : A ⇒ A ⊢ λ (x : A) f (f x) : A ⇒ A
  example-3 : {A : type} → (∙ ⨟ A ⇒ A) → (A ⇒ A)
  example-3 {A} (_ , f) = λ (x : A) → f (f x)

With the shallow embedding it is very easy to compute in λ-calculus, just use Agda's normalization abilities to compute their normal forms. This is possible because our embedding makes sure that the λ-calculus normalization and Agda's normalization coincide.

Deep embedding

Here is the corresponding deep embedding.


module Deep where

  -- The λ-calculus simple types
  infixr 7 _⇒_
  data type : Set where
    nat : type
    _⇒_ : type → type → type

  -- The λ-calculus typing context, we use de Bruijn indices
  infixl 5 _⨟_
  data context : Set where
    ∙ : context
    _⨟_ : context → type → context

  -- A ∈ Γ is the type of those de Bruijn indices whose type in Γ is A
  infix 3 _∈_
  data _∈_ : type → context → Set where
    z : ∀ {A : type} {Γ : context} → A ∈ Γ ⨟ A
    s : ∀ {A B : type} {Γ : context} → B ∈ Γ → B ∈ Γ ⨟ A

  -- term Γ A is the type of λ-calculus terms of type A in context Γ
  data term : context → type → Set where
    zero : ∀ {Γ} → term Γ nat
    succ : ∀ {Γ} → term Γ nat → term Γ nat
    var : ∀ {Γ A} → A ∈ Γ → term Γ A
    lam : ∀ {Γ} A {B} → term (Γ ⨟ A) B → term Γ (A ⇒ B)
    app : ∀ {Γ A B} → term Γ (A ⇒ B) → term Γ A → term Γ B

  -- The λ-calculus typing judgement x : nat ⨟ f : nat ⇒ nat⨟ y : nat ⊢ succ (succ x) : nat
  example-1 : term (∙ ⨟ nat ⨟ nat ⇒ nat ⨟ nat) nat
  example-1 = succ (succ (var (s (s z))))

  -- The λ-calculus typing judgement ∙ ⊢ (λ (x y : nat) succ x) (succ (succ 0)) : nat ⇒ nat
  example-2 : term ∙ (nat ⇒ nat)
  example-2 = app (lam nat (lam nat (succ (var (s z))))) (succ (succ zero) )

  -- The λ-calculus typing judgement f : A ⇒ A ⊢ λ (x : A) f (f x) : A ⇒ A
  example-3 : {A : type} → term (∙ ⨟ A ⇒ A) (A ⇒ A)
  example-3 {A} = lam A (app (var (s z)) (app (var (s z)) (var z)))

In the deep embedding the terms of the λ-calculus are elements of the inductive type term. We cannot use Agda's normalization algorithm to compute with these, they're all in normal form already.

However, with the deep embedding we can reason about λ-calculus. For example, we can define a model of the λ-calculus:

module Semantics where

  -- The set-theoretic model of λ-calculus

  open import Data.Nat
  open import Data.Unit
  open import Data.Product

  open Deep

  -- Types are interpreted as sets
  ⟦_⟧ᵗ : type → Set
  ⟦ nat ⟧ᵗ = ℕ
  ⟦ A ⇒ B ⟧ᵗ = ⟦ A ⟧ᵗ → ⟦ B ⟧ᵗ

  -- Contexts are interpreted as sets
  ⟦_⟧ᶜ : context → Set
  ⟦ ∙ ⟧ᶜ = ⊤
  ⟦ Γ ⨟ A ⟧ᶜ =  ⟦ Γ ⟧ᶜ × ⟦ A ⟧ᵗ

  -- Auxiliary map, for looking up values of variables
  lookup : ∀ {Γ A} → A ∈ Γ → ⟦ Γ ⟧ᶜ → ⟦ A ⟧ᵗ
  lookup z (_ , a) = a
  lookup (s x) (η , _) = lookup x η

  -- A typing judgement Γ ⊢ e : A is interpreted as a map ⟦ e ⟧ : ⟦ Γ ⟧ᶜ → ⟦ A ⟧ᵗ
  ⟦_⟧ : ∀ {Γ A} → term Γ A → ⟦ Γ ⟧ᶜ → ⟦ A ⟧ᵗ
  ⟦ zero ⟧ η = 0
  ⟦ succ e ⟧ η = suc (⟦ e ⟧ η)
  ⟦ var x ⟧ η = lookup x η
  ⟦ lam A e ⟧ η = λ a → ⟦ e ⟧ (η , a)
  ⟦ app e₁ e₂ ⟧ η = ⟦ e₁ ⟧ η (⟦ e₂ ⟧ η)

  -- The interpretation of ∙ ⊢ (λ (x : nat) . succ (succ x)) (succ zero) : nat
  cow : ⟦ ∙ ⟧ᶜ → ⟦ nat ⟧ᵗ
  cow tt = ⟦ app (lam nat (succ (succ (var z)))) (succ zero) ⟧ tt
  -- Agda normalizes cow tt to the numeral 3

Yes, the model is also an interpreter for λ-calculus. Welcome to constructive mathematics.

The laundry list

I am not familiar with all the embeddings you listed in the question. Hopefully other will provide answers for the missing ones:

  • “Coq in Coq” is deep. They want to prove things about Coq. A shallow embedding would be the identity map.
  • Dedukti is a logical framework, which makes it a bit special. Its purpose is formalization of formal systems. One defines the syntax and typing rules of the embedded system (deep embedding), but in such a way that Dedukti's contexts, variables, type-checking, normalization and rewriting abilities can be reused by the embedded system (shallow embedding).
  • “Coq is a Lean Typechecker“ is shallow. The web page even says: “The basic idea is to translate Lean Prop to Coq SProp, inductives to inductives, etc.“
  • “Towards self-verification of HOL Light” has a section called “Formalized syntax” so I will guess it is deep without reading the entire paper.
  • “Lean4Lean“ is about implementing Lean in Lean, a self-interpreter. This is a deep embedding because it will involve parsing syntax and interpreting it into machine code. A shallow embedding of Lean in Lean is just the identity transformation.
  • “MathPort” is a shallow embedding, because they tried as hard as possible to make it the identity transformation.
  • “Encoding the HOL Light logic in Coq” is shallow.

Supplemental: What about set theories?

An interesting question is whether emeddings of set theory into type theory are shallow or deep. Let us just focus on material set theory such as ZFC (although the story is much the same for structural set thoeries).

A material set theory is typically a single-sorted first-order theory. In type theory we commonly find something like this:

open import Level
open import Data.Empty
open import Data.Product
open Σ

module SetTheory (ℓ : Level) where

  -- The type of well-founded trees with branching type from universe level ℓ
  data V : Set (suc ℓ) where
    set : ∀ {I : Set ℓ} → (I → V) → V

  mutual
    -- Membership relation
    infix 5 _∈_
    data _∈_ : V → V → Set ℓ where
      ∈-set : ∀ {I} {t} {u : I → V} → (Σ[ i ∈ I ] t ≈ u i) → t ∈ set u

    -- Subset relation
    infix 5 _⊆_
    _⊆_ : V → V → Set ℓ
    set x ⊆ t = ∀ i → x i ∈ t

    -- Equality of well-founded trees as sets
    infix 5 _≈_
    data _≈_ : V → V → Set ℓ where
      ≈-set : ∀ {t u : V} → t ⊆ u → u ⊆ t  → u ≈ t

  -- We check that (V, ∈, ≈) satisfies the set-theoretic axioms.
  -- For illustration we only provide extensionality and empty set.
  -- (Note that we cannot validate the powerset axiom, Agda is too predicative.)

  data empty-type : Set ℓ where

  ∅ : V
  ∅ = set {I = empty-type} λ {()}

  axiom-empty-set : Σ[ x ∈ V ] ∀ (y : V) → y ∈ x → ⊥
  axiom-empty-set = ∅ , λ {y (∈-set ())}

  axiom-extensionality : ∀ {x y : V} → x ⊆ y → y ⊆ x → x ≈ y
  axiom-extensionality x⊆y y⊆x = ≈-set y⊆x x⊆y

  -- and so on

I would call this a model of set theory in type theory. It is not an "embedding" in the sense of having a syntactic translation from one formal system to another.

This situation is completely analogous to other situations involving first-order theories, which is what a material set theory usually is. Take the theory of a group, for example. If we define a single group, say $\mathbb{Z}_7$, then that is like defining a single model V of set theory, as above. We might define the structure of all groups

structure Group : Type where
  carrier : Type
  mul : carrier → carrier → carrier
  inv : carrier → carrier
  assoc : ...
  unit-left : ...
  unit-right : ...
  inv-left : ...
  inv-right : ...

but that would still just be semantics, as we're now just defining (the object part of) the category of all groups. We could to the same for set theories and define the category of all models of set theory, so not an embedding.

If you insist, you may call the above a shallow something-or-other of set theory into type theory (because we are using type-theoretic logic to validate set-theoretic axioms), but I hesitate to call it an "embedding" because it does not faithfully reflect provability of set-theoretic statements. That is, type theory might prove some set-theoretic statements about V which set theory does not prove (this is not an easily answered question, and it depends on the exact set-theoretic axioms and the exact type-theoretic rules).

A deep embedding of set theory into type theory would begin with inductive types representing the first-order formulas and terms. But that's a different kind of animal that we would use if we wanted to prove meta-theorems about the first-order theory known as "set theory".

$\endgroup$
3
  • $\begingroup$ Wow, this is a really good answer! You have really cleared it up for me (and hopefully others with the same question)! $\endgroup$
    – Jason Rute
    Oct 13, 2023 at 22:59
  • $\begingroup$ I wonder now if Lean's Mathlib's ZFC set theory (based on Flypitch) and category theory libraries are a mixture of deep and shallow embeddings. On the deep side, there are inductive definitions, resp., for a ZFC model and a category. On the shallow side, the canonical models of sets ($\mathbf{V}$ in ZFC and $\mathbf{Set}$ in category theory) are defined in terms of Type u. The shallow embedding is further supported by the notation and typeclasses. For example, the Yoneda embedding has signature def yoneda {C : Type u₁} [category.{v₁} C] : C ⥤ (Cᵒᵖ ⥤ Type v₁). $\endgroup$
    – Jason Rute
    Oct 13, 2023 at 23:48
  • $\begingroup$ I also commented on set theory embedding. $\endgroup$ Oct 14, 2023 at 10:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.