Logical relations are cool (hence the incredibly witty title). I studied them last year while writing this paper. One of the goals of the paper was to introduce logical relations to people with some familiarity with proof assistants (e.g. graduate students studying programming languages). The paper was rejected, but the feedback we got was really helpful! I’m not really sure when or if I’ll next get the chance to refine the paper and resubmit it somewhere, but I still do want to try to write some stuff down before I forget everything. So here is a blog post!

I’ll be writing this blog post as if it were geared at someone who has started to study programming language foundations. If you’re pretty familiar with syntax and semantics but want to learn more about logical relations, feel free to skip some sections. Some basic familiarity with Agda (e.g. you’ve read a fair amount of Part 1 of PLFA) would be helpful, though I’ve tried to make most of this digestible to someone who is familiar with Haskell and/or logical foundations.

variable x y : String

data Term : Set where
  true false : Term

  -- variables, e.g. var "x"
  var : String → Term

  -- abstraction, e.g. λ[ "x" ⇒ t ]
  λ[_⇒_] : String → Term → Term

  -- application, e.g. r · s
  _·_ : Term → Term → Term

  -- conditional branching, e.g. if s then t₁ else t₂
  if_then_else_ : Term → Term → Term → Term

variable r s t t₁ t₂ : Term

_ : Term
_ = λ[ "x" ⇒ var "x" ] · true

data Type : Set where
  -- boolean type
  bool : Type

  -- function type e.g. S ⇒ T
  _⇒_ : Type → Type → Type

variable S T : Type

data Map (K : Set) (V : Set) : Set where
  -- empty map
  • : Map K V

  -- extending a map, e.g. m , k ↦ v
  _,_↦_ : Map K V → K → V → Map K V

Ctx = Map String Type

variable Γ : Ctx

-- lookup, e.g. k ↦ v ∈ m
data _↦_∈_ {K : Set} {V : Set} : K → V → Map K V → Set where
  -- the key/value pair is at the head of the context
  here : ∀ {k : K} {v : V} {m : Map K V}
         ------------------
       → k ↦ v ∈ m , k ↦ v

  -- the key/value pair is not at the head of the context
  there : ∀ {k k′ : K} {v v′ : V} {m : Map K V}
        → k ↦ v ∈ m
        → ¬ (k ≡ k′)
          --------------------
        → k ↦ v ∈ m , k′ ↦ v′

-- extending a context, e.g. Γ , x ∷ T
_,_∷_ : Ctx → String → Type → Ctx
_,_∷_ = _,_↦_

-- variable lookup in a context, e.g. x ∷ T ∈ Γ
_∷_∈_ : String → Type → Ctx → Set
_∷_∈_ = _↦_∈_

Here are the (standard) typing rules for terms in the lambda calculus that are well typed (i.e. the terms that make up our STLC).

-- typing judgement, e.g. Γ ⊢ t ∷ T
data _⊢_∷_ : Ctx → Term → Type → Set where

  ⊢true : ---------------
          Γ ⊢ true ∷ bool

  ⊢false : ----------------
           Γ ⊢ false ∷ bool

  ⊢var : x ∷ T ∈ Γ
         -------------
       → Γ ⊢ var x ∷ T

  ⊢abs : Γ , x ∷ S ⊢ t ∷ T
         ----------------------
       → Γ ⊢ λ[ x ⇒ t ] ∷ S ⇒ T

  ⊢app : Γ ⊢ r ∷ S ⇒ T
       → Γ ⊢ s ∷ S
         -------------
       → Γ ⊢ r · s ∷ T

  ⊢if :          Γ ⊢ s ∷ bool
      → Γ ⊢ t₁ ∷ T   →   Γ ⊢ t₂ ∷ T
        ----------------------------
      → Γ ⊢ if s then t₁ else t₂ ∷ T

What is a logical relation?

Logical relations are a powerful technique for proving program properties. Let’s say we want to prove that a program t and its compiled program ⟦ t ⟧ have the same behavior (e.g. t ≈ ⟦ t ⟧), as long as t is well typed. It’s often the case that we can’t prove this directly by induction on the typing derivation for t (e.g. Γ ⊢ t : T). Instead, we may need to strengthen our inductive hypothesis. Logical relations are, among many things, an instance of this.

Their name can be a little arcane, but essentially they represent the logical interpretation that we would ascribe a program that satisfies the property we want to prove. Instead of showing that if t is well typed then t ≈ ⟦ t ⟧, we may instead craft a relation between t and ⟦ t ⟧ that is more descriptive of the behavior we would logically expect to be true if it were the case that t ≈ ⟦ t ⟧.

And that’s really the main idea behind logical relations! There’s more details I’m skipping over, but I’ll touch on them as we go through the example of type soundness.

Type soundness

A classic property that we prove about the simply-typed lambda calculus is that the evaluation of any term is well defined (sometimes called type soundness or type safety). This is relevant in the sense that in the untyped lambda calculus, we can have a term like true true (i.e. try to apply true to true). There is no well-defined evaluation for true true, in other words if we try to “run” this program it would “fail.”

With that said, true true is an ill-typed term – so it is ruled out in the simply-typed lambda calculus. In other words, proving type soundness gives meaning to our type system: we have shown that with it we are now only considering terms that will not “fail” when they are “run.” This has a practical benefit: if we’re designing a programming language and prove type soundness, then we can give programmers a guarantee that if their code type checks, it will not “fail.”

We can prove type soundness through the use of a logical relation. Specifically, we can use a logical predicate: a unary logical relation (that is, a relation over a single term).

Semantics

Before we can even formulate what type soundness is, we need to describe computation of STLC (i.e., the semantics). We will be using a call-by-value semantics. A term t is evaluated in an environment γ to a value a (i.e. γ ⊢ t ⇓ a). An environment γ maps variables to values. The values that STLC terms evaluate to are either true, false, or a closure [λx. t] γ.

A closure “closes” a term t in an abstraction λx. t with an environment γ mapping every variable in t except for x to a value. Intuitively, [λx. t] γ is “waiting” for a value for x to continue evaluating t with the environment γ extended with the value for x. The metavariables γ, δ will range over environments; a, b, and f will range over values.

mutual
  -- values that terms evaluate to
  data Value : Set where
    true false : Value

    -- closure, e.g. [λ x ⇒ t ] γ
    [λ_⇒_]_ : String → Term → Env → Value

  -- environment that terms are evaluated in
  Env = Map String Value

variable γ δ : Env

variable f a b : Value

-- semantics, e.g. γ ⊢ t ⇓ a
data _⊢_⇓_ : Env → Term → Value → Set where

  evalTrue : ---------------
             γ ⊢ true ⇓ true

  evalFalse : ----------------
              γ ⊢ false ⇓ false

  evalVar : x ↦ a ∈ γ
            ---------------
          → γ ⊢ var x ⇓ a

  evalAbs : -----------------------------
            γ ⊢ λ[ x ⇒ t ] ⇓ [λ x ⇒ t ] γ

  evalApp : γ ⊢ r ⇓ [λ x ⇒ t ] δ     →       γ ⊢ s ⇓ a
          →              δ , x ↦ a ⊢ t ⇓ b
            ------------------------------------------
          → γ ⊢ r · s ⇓ b

  evalIfTrue : γ ⊢ s ⇓ true  →   γ ⊢ t₁ ⇓ a
               ----------------------------
             → γ ⊢ if s then t₁ else t₂ ⇓ a

  evalIfFalse : γ ⊢ s ⇓ false  →  γ ⊢ t₂ ⇓ b
                ----------------------------
              → γ ⊢ if s then t₁ else t₂ ⇓ b

This is what is known as a natural semantics. This semantics is nice because it looks a lot like an interpreter that you might write in a functional programming language. I haven’t actually written the semantics out as a function because we’re in Agda, where every program has to be terminating.

Agda wouldn’t be able to tell that such a function would terminate; and in fact, it wouldn’t, as the semantics is over untyped terms. Untyped lambda calculus terms can evaluate forever (e.g. (λx.x x) (λx.x x)). This is another practical reason why we want to prove type soundness of STLC: it tells us that the evaluation of a well-typed term will in fact terminate.

Either way, we can now state type soundness! We say that our type system is sound if any term that can be assigned a type can be evaluated to a value. For clarity and simplicity, it is common to restrict this property to a closed term of a base type such as bool. The restricted version is: a closed term that can be assigned the type bool evaluates to either true or false.

postulate
  -- type soundness
  _ : • ⊢ t ∷ bool
      ----------------------------
    → • ⊢ t ⇓ true ⊎ • ⊢ t ⇓ false

Here, I’m using Agda’s sum type (_⊎_ : Set → Set → Set).

Why a logical relation?

So, what’s the problem? This seems like a pretty standard property to prove. Sure, it’s restricted to the empty context and base types, so proving it by induction on the typing derivation doesn’t make sense, but we can probably generalize it a little:

postulate
  -- generalized type soundness
  _ : Γ ⊢ t ∷ T
      -----------------------
    → ∃[ γ ] ∃[ a ] γ ⊢ t ⇓ a

Here, I’m using Agda’s “exists” syntax, e.g. ∃[ x ] P x, where P is some property dependent on x.

Nice! This seems to be more of a general enough property to prove by induction on the typing derivation Γ ⊢ t : T, right? Well, sadly, no. Not nice. We can’t prove this property directly by induction on the typing derivation, either. This is the case even if we play around with the definition a little – as you might be tempted to do, but don’t! There is a better way. A… logical way.

If we were to try to prove this property directly by induction on the typing derivation the problem would be in the application case (r s). The induction hypothesis tells me that the evaluation of r is well defined, as well as that the evaluation of s is well defined. We can even take some extra steps to determine that r evaluates to some closure [λx. t] δ.

Unfortunately, it’s at this point that you usually get stuck. Let’s say that s evaluates to some value a. To prove that the evaluation of r s is well defined, we’d also want to know that the evaluation of the body of the closure [λx. t] δ is well defined when its environment δ is extended with x ↦ a. But, we’re all out of induction hypotheses!

So, how does a logical relation help here? Well, we talked about a logical relation being the logical interpretation we would give a term t if it is the case that it satisfies this property. Logically, we would expect it to be the case that if r is a well-typed term that evaluates to a closure, then the evaluation of the body of the closure should also be well defined when extended with some value.

I can encode this logical interpretation as a logical relation (or in this case, a logical predicate), such that satisfying the logical relation implies the desired property. Then, instead of proving that the evaluation of a well-typed term is well defined, we can prove that a well-typed term satisfies the logical predicate. This strengthens our induction hypothesis, because we have now (hopefully) described all of the properties we would logically expect to hold of a term whose evaluation is well defined.

Defining a logical relation

There is one missing piece to the structure of a logical relation that is unfortunately not present in the name: a logical relation is usually defined inductively on types. The properties we wish to prove are in relation to our type system, so types should be our guiding force. If we have a well-typed term r, its type is what feeds our expectations. For example, if its type were bool ⇒ bool, we’d expect r to evaluate to a closure.

The logical predicate we’ll be using will be defined mutually in two parts, though this is mostly for clarity. Both of these definitions can be thought of as making up one predicate (and we could combine them into one if we wanted to, though this would be a little annoying with the way I’ve set everything up so far).

The first part of the predicate is ⟦ T ⟧, which is the logical interpretation we would have for a value of type T. For bool, we expect a value to be either true or false. For S ⇒ T, our expectation is that the value is a closure [λx. t] δ and that when the closure is given a value a such that a ∈ ⟦ S ⟧, the body of the closure itself evaluates to a value b such that b ∈ ⟦ T ⟧. Which brings us to the second part of the predicate, ℰ⟦ T ⟧, which is mostly syntactic sugar for “this term evaluates to some value a such that a ∈ ⟦ T ⟧”.

In set notation, we could write this out as:

⟦ bool ⟧ = { true , false }
⟦ S ⇒ T ⟧ = { [λx. t] δ | ∀ a ∈ ⟦ S ⟧, ((δ , x ↦ a) , t) ∈ ℰ⟦ T ⟧

ℰ⟦ T ⟧ = { (γ , t) | ∃ a ∈ ⟦ T ⟧, γ ⊢ t ⇓ a }

In Agda, the definition does not change much:

mutual
  -- logical predicate for values, e.g. a ∈ ⟦ T ⟧
  ⟦_⟧ : Type → Value → Set
  ⟦ bool ⟧ true = ⊤
  ⟦ bool ⟧ false = ⊤
  ⟦ S ⇒ T ⟧ ([λ x ⇒ t ] δ) = ∀ {a} →
     a ∈ ⟦ S ⟧
    → ((δ , x ↦ a) , t) ∈ ℰ⟦ T ⟧
  ⟦ _ ⟧ _ = ⊥

  -- logical predicate for environment/term, e.g. (γ , t) ∈ ℰ⟦ T ⟧
  ℰ⟦_⟧ : Type → Env × Term → Set
  ℰ⟦ T ⟧ (γ , t) = ∃[ a ] γ ⊢ t ⇓ a × a ∈ ⟦ T ⟧

Here, I’m making use of Agda’s membership syntax (_∈_ : A → (A → Set) → Set) for readability. I’m also using Agda’s product type (_×_ : Set → Set → Set) and constructor (_,_ : A → B → A × B). Finally, I’m using Agda’s unit (⊤) and empty (⊥) types to represent a condition that always holds and a condition that never holds, respectively.

Our goal now is to use this predicate to prove type soundness. To do so, we usually first show that if a term is well-typed, then it satisfies the logical predicate. We can try to write that out:

postulate
  _ : Γ ⊢ t ∷ T → ∀ γ → (γ , t) ∈ ℰ⟦ T ⟧

Unfortunately, however, we are still unable to prove this property. The reason is that γ is unrestricted. To understand why this is problematic, consider the variable case. We want to show that a variable evaluates to a value a such that a ∈ ⟦ T ⟧, but the variable evaluates to whatever is supplied by the environment, for which we have no guarantees. Changing the forall to an exists doesn’t solve the problem either, because we wouldn’t know what to use as our environment γ.

The problem is that the environment γ is unrestricted, so how about we restrict it? If we let ourselves be guided by the variable case, we probably want it to be the case that for every variable x such that x ∷ T ∈ Γ, it should be the case that there is some value a such that x ↦ a ∈ γ and a ∈ ⟦ T ⟧. We refer to this as γ being “semantically typed by the context Γ”, or Γ ⊨ γ.

-- semantic typing for environments, e.g. Γ ⊨ γ
_⊨_ : Ctx → Env → Set
Γ ⊨ γ = ∀ {x} {T}
        → x ∷ T ∈ Γ
        → ∃[ a ] a ∈ ⟦ T ⟧ × x ↦ a ∈ γ

Now, we can prove a different property that might finally work, known as semantic typing. We say that a term t has the semantic type T in the context Γ (notated Γ ⊨ t ∷ T) if for any environment γ that is semantically typed by the context Γ (e.g. Γ ⊨ γ), it is the case that (γ , t) ∈ ℰ⟦ T ⟧. It’s common to refer to ℰ⟦ T ⟧ as a semantic “model” of the type T, hence why we refer to this property as semantic typing.

_⊨_∷_ : Ctx → Term → Type → Set
Γ ⊨ t ∷ T =
  ∀ {γ} → Γ ⊨ γ → (γ , t) ∈ ℰ⟦ T ⟧

Fundamental lemma of logical relations

Proving that if a term is syntactically typed then it is semantically typed, is known as the fundamental lemma of logical relations.

fundamental-lemma : Γ ⊢ t ∷ T → Γ ⊨ t ∷ T

Before diving into the proof of the fundamental lemma, I will first start with a smaller lemma, ⊨-ext. If I have an environment γ such that Γ ⊨ γ and a value a such that a ∈ ⟦ T ⟧, then the extended environment γ , x ↦ a is also semantically typed by the context Γ , x ∷ T.

⊨-ext : Γ ⊨ γ → a ∈ ⟦ T ⟧ → Γ , x ∷ T ⊨ γ , x ↦ a
⊨-ext {a = a} ⊨γ a∈⟦T⟧ y∷S∈Γ
  with y∷S∈Γ
... | here            =
  a , a∈⟦T⟧ , here
... | there y∷S∈Γ y≢x =
  let (b , b∈⟦S⟧ , y↦b∈γ) = ⊨γ y∷S∈Γ in
  b , b∈⟦S⟧ , there y↦b∈γ y≢x

With this lemma, we prove the fundamental lemma by induction on the syntactic typing derivation. I’ll go into more detail for all of the other cases below, but let’s focus on the application case for now. With our logical predicate, we now have the inductive hypothesis we need. The closure [λx. t] δ that r evaluates to satisfies the logical predicate, so we have that t evaluates to a value b when δ is extended with the value a that s evaluates to.

fundamental-lemma ⊢true ⊨γ = true , evalTrue , tt
fundamental-lemma ⊢false ⊨γ = false , evalFalse , tt

fundamental-lemma (⊢var x∷T∈Γ) ⊨γ =
  let (a , a∈⟦T⟧ , x↦a∈γ) = ⊨γ x∷T∈Γ in
  a , evalVar x↦a∈γ , a∈⟦T⟧

fundamental-lemma {t = λ[ x ⇒ t ]} (⊢abs ⊢t) {γ} ⊨γ =
  [λ x ⇒ t ] γ , evalAbs ,
  λ a∈⟦S⟧ →
    let (b , t⇓ , b∈⟦T⟧) = fundamental-lemma ⊢t (⊨-ext ⊨γ a∈⟦S⟧) in
    b , t⇓ , b∈⟦T⟧

fundamental-lemma (⊢app ⊢r ⊢s) ⊨γ
  with fundamental-lemma ⊢r ⊨γ
...  | f @ ([λ x ⇒ t ] δ) , r⇓ , f∈⟦S⇒T⟧  =
  let (a , s⇓ , a∈⟦S⟧) = fundamental-lemma ⊢s ⊨γ in
  let (b , f⇓ , b∈⟦T⟧) = f∈⟦S⇒T⟧ a∈⟦S⟧ in
  b , evalApp r⇓ s⇓ f⇓ , b∈⟦T⟧

fundamental-lemma (⊢if ⊢s ⊢t₁ ⊢t₂) ⊨γ
  with fundamental-lemma ⊢s ⊨γ
... | true , s⇓ , tt  =
  let (a , t₁⇓ , a∈⟦S⟧) = fundamental-lemma ⊢t₁ ⊨γ in
  a , evalIfTrue s⇓ t₁⇓ , a∈⟦S⟧

... | false , s⇓ , tt =
  let (b , t₂⇓ , sb) = fundamental-lemma ⊢t₂ ⊨γ in
  b , evalIfFalse s⇓ t₂⇓ , sb

Putting it all together

Now that we’ve proven the fundamental lemma of logical relations, we can prove type soundness of STLC. The proof follows directly from the fundamental lemma: if a term t has type bool then the value that it evaluates to satisfies the logical predicate for ⟦ bool ⟧. There are only two such values: true and false.

soundness : • ⊢ t ∷ bool → • ⊢ t ⇓ true ⊎ • ⊢ t ⇓ false
soundness ⊢t
  with fundamental-lemma ⊢t (λ ())
... | true , t⇓ , _ = inj₁ t⇓
... | false , t⇓ , _ = inj₂ t⇓

And that’s it! You’ve now been shown a logical relation and how to use it! Congratulations!

Of course, we’ve proven a property that can be proven by other methods. (And you may have even done so already!) That said, there’s a ton of other properties that can be proven by logical relations. Many of these actually are concerned with two different terms, which entails defining a binary logical relation instead of a unary one as I’ve done here.

Further reading

Now that you’ve seen this example, you can try to look at some more complicated ones. A nice followup is to see how strong normalization (which is closely related to type soundness) is proven with a logical relation. I found these lecture notes to be really helpful.

Another nice followup is to see how you can extend logical relations to prove properties about languages with more complex features, like recursive types. For that, I would recommend these notes based on Amal Ahmed’s lectures at OPLSS 2015.

Neither of those resources include a mechanized component, as I have tried to do in this blog post. “POPLmark Reloaded” by Abel et al. goes over a logical relation for proving strong normalization as well, and has several accompanying mechanizations. More recently, Timany et al. wrote “A Logical Approach to Type Soundness,” which has a very nice tutorial on proving type soundness with a logical relation for richer languages than STLC, as well as a true relational property that requires a binary logical relation. They use a Coq framework known as Iris, which is very helpful for mechanizing more complicated logical relations.

(λx. t) s ⟶ t[s/x]