There’s a lot of depth to logical relations, but if you’ve seen them before then chances are you’ve seen them used as a technique to prove some theorem. A person might be interested in proving that if a term is well typed, then it has some desirable property. One reasonable attempt at proving this is by induction on the typing derivation, though people will typically come across a stumbling block in the application case of their proof. To solve this problem, you use a handydandy logical relation.
It turns out that this strategy can be applied to a fairly wide array of properties, such as compiler correctness. This is a large part of why logical relations have become so pervasive in PL research, and there are is a growing amount of tutorials on the subject aimed at early graduate students (e.g. these lecture notes by Robert Harper). As logical relations become more of a staple, many of these tutorials could (and maybe should) be taught as one of the first “foundational” proofs in a PL course.
While logical relations have proven to be really useful, mechanizing them in generalpurpose proof assistants such as Agda is notoriously burdensome. This is because a proof by logical relations typically involves several substitution lemmas. Substitution lemmas can reasonably be left as informal assumptions on penandpaper proofs, but reasoning about substitutions in generalpurpose proof assistants usually incurs a lot of tedious work.
One consequence of this is that reading a proof by logical relations in a proof assistant like Agda requires a fair amount of proficiency in the proof assistant to be able to follow all of the substitution lemmas. At the same time, the use of proof assistants to teach programming language foundations has become increasingly common, as is the case with Software Foundations and Programming Language Foundations in Agda. Herein lies the problem: we want to teach logical relations early on in a PL course, but we would have a hard time doing so if the course was taught with a generalpurpose proof assistant like Coq or Agda, as is becoming the norm.
Admittedly, we could always teach the material and say something along the lines of “and here we use a substitution lemma for which the details have been omitted.” After all, this is essentially what is done when the content is taught on paper. PLFA takes this approach, which is understandable given the situation. This can be a bit unsatisfying in a proof assistant, however, where part of the help that is given to a student is that they can see all of the details of a proof for themselves.
With this, we have set the stage. Our goal is then to produce a proof by logical relations that can be shown in a generalpurpose proof assistant to someone who has only learned “the basics.” This is the proof that we showcased in our paper, and I will be going over it in this blog post. While I will focus on Agda, all of this should apply to other generalpurpose proof assistants such as Coq or Lean — and I will not make use of any Agdaspecific features.
Note that there has been significant progress in improving the state of mechanization for proofs by logical relations. I’ll share more on this later, but these solutions are either 1) not selfcontained enough to teach logical relations with a generalpurpose proof assistant, or 2) tailored to specific proof assistants (as is the case with Beluga).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.
Syntax
The object language I’ll use to introduce logical relations is the simplytyped
lambda calculus (STLC). There’s variables, abstractions (λx. t
), application
(r s
), booleans (true
, false
), and conditional branching
(if t1 then t2 else t3
). The metavariables r
, s
, and t
will range over
terms, and the metavariables x
and y
will range over variable names.
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
Here, I am using Agda’s string type (String
) to represent
variable identifiers by their name. This isn’t something you actually want to do
in general, but it’s the intuitive choice, and it doesn’t affect the content of
this blog post. I’m also using Agda’s mixfix syntax to make the Agda
representation of these terms look a lot like the notation we’d use on paper.
(I’ll be including “footnotes” like the one above for Agdaspecific tidbits, so that hopefully this blog post can be readable to someone not used to reading Agda.)
With the syntax defined, we can represent a term like (λx. x) true
in Agda.
_ : Term _ = λ[ "x" ⇒ var "x" ] · true
Going forward, I won’t use the actual Agda representation in the text of the
blog post for readability (i.e. I will refer to λ[ "x" ⇒ var "x" ] · true
as
(λx. x) true
).
There will be only two types: bool for booleans and the arrow type for
functions. The metavariables S
and T
will range over types.
Types
data Type : Set where  boolean type bool : Type  function type e.g. S ⇒ T _⇒_ : Type → Type → Type variable S T : Type
Terms will be typed in a context, which will map variables to types (e.g.
x:bool ⇒ bool, y:bool
). The metavariable Γ
will range over contexts.
Contexts will be an instance of a more general Map
that we’ll be reusing later.
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
It will be useful to define a judgement for membership of a map as well. For convenience, this judgement will double as a sort of “lookup” that looks up a key in a map. The judgement has two cases: either the key/value pair is at the head of the map, or the key/value pair is somewhere else in the map, and the key is not “shadowed” by the preceding keys in the map.
 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′
For readability, we’ll add syntactic sugar for these specific to contexts.
 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 simplytyped 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 welldefined evaluation for true true
, in other words if
we try to “run” this program it would “fail.”
With that said, true true
is an illtyped term – so it is ruled out in the
simplytyped 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 callbyvalue
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 welltyped 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 welltyped 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 welltyped term is well defined, we can prove that a welltyped 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 welltyped 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 welltyped, 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.
fundamentallemma : Γ ⊢ 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
Reminder: an environment γ
is semantically typed by a context Γ
if for every
variable y ∷ S ∈ Γ
, it’s the case that there exists some b
such that
y ↦ b ∈ γ
and b ∈ ⟦ S ⟧
.
Our goal is to prove that Γ , x ∷ T ⊨ γ , x ↦ a
. We prove this by case
analysis on the variable y
mapped to the type S
in the context Γ
.

If the variable is at the head of the map (
here
), then reallyy
isx
andS
isT
. In this case, we’re immediately done asx ↦ a
is at the head of the environmentγ , x ↦ a
anda ∈ ⟦ T ⟧
is given. 
Otherwise, the variable
y
is not at the head of the list (andy ≢ x
). In this case, we already know thatΓ ⊨ γ
. This is all we need, as we have that fory ∷ S ∈ Γ
, there exists someb
such thatb ∈ ⟦ S ⟧
andx ↦ b ∈ γ
.
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.
fundamentallemma ⊢true ⊨γ = true , evalTrue , tt fundamentallemma ⊢false ⊨γ = false , evalFalse , tt fundamentallemma (⊢var x∷T∈Γ) ⊨γ = let (a , a∈⟦T⟧ , x↦a∈γ) = ⊨γ x∷T∈Γ in a , evalVar x↦a∈γ , a∈⟦T⟧ fundamentallemma {t = λ[ x ⇒ t ]} (⊢abs ⊢t) {γ} ⊨γ = [λ x ⇒ t ] γ , evalAbs , λ a∈⟦S⟧ → let (b , t⇓ , b∈⟦T⟧) = fundamentallemma ⊢t (⊨ext ⊨γ a∈⟦S⟧) in b , t⇓ , b∈⟦T⟧ fundamentallemma (⊢app ⊢r ⊢s) ⊨γ with fundamentallemma ⊢r ⊨γ ...  f @ ([λ x ⇒ t ] δ) , r⇓ , f∈⟦S⇒T⟧ = let (a , s⇓ , a∈⟦S⟧) = fundamentallemma ⊢s ⊨γ in let (b , f⇓ , b∈⟦T⟧) = f∈⟦S⇒T⟧ a∈⟦S⟧ in b , evalApp r⇓ s⇓ f⇓ , b∈⟦T⟧ fundamentallemma (⊢if ⊢s ⊢t₁ ⊢t₂) ⊨γ with fundamentallemma ⊢s ⊨γ ...  true , s⇓ , tt = let (a , t₁⇓ , a∈⟦S⟧) = fundamentallemma ⊢t₁ ⊨γ in a , evalIfTrue s⇓ t₁⇓ , a∈⟦S⟧ ...  false , s⇓ , tt = let (b , t₂⇓ , sb) = fundamentallemma ⊢t₂ ⊨γ in b , evalIfFalse s⇓ t₂⇓ , sb
Reminder: we say that Γ ⊨ t ∷ T
if for any environment γ
such that Γ ⊨ γ
,
there exists a value a
such that γ ⊢ t ⇓ a
and a ∈ ⟦ T ⟧
. We want to show
that if Γ ⊢ t ∷ T
, then Γ ⊨ t ∷ T
(the fundamental lemma of logical
relations).
We prove this by induction on the syntactic typing derivation Γ ⊢ t ∷ T
:

The first cases are
true
/false
. These can be proven immediately as both terms evaluate to themselves (they are already values) andtrue
/false
always satisfy the logical predicate (unit). In this proof, I am usingtt
(Agda’s unit value) as the “proof” that they satisfy the logical predicate. 
The next case is the variable case, which prompted us to define this whole
semantic typing for environments thing. Luckily, we can use that given proof
directly now! For the variable
x ∷ T ∈ Γ
, we have that sinceΓ ⊨ γ
, there exists somea ∈ ⟦ T ⟧
such thatx ↦ a ∈ γ
. 
We now prove the abstraction case. Given some abstraction
λx. t
, we want to show that it is semantically typed. Immediately, we have that it evaluates to the closure[λx. t] γ
in any environmentγ
. We then need only show that this closure satisfies the logical predicate⟦S ⇒ T⟧
. In other words, we want to show that for any valuea
such thata ∈ ⟦ T ⟧
, the body of the closuret
evaluates to a valueb
such thatb ∈ ⟦ T ⟧
. Assume we have such ana
, then by⊨ext
we have thatΓ , x ∷ S ⊨ γ , x ↦ a
. We can then use our induction hypothesis to have exactly what we want to show, and we are done. 
The only case I haven’t explained is the case for ifthenelse. By the
induction hypothesis, we have that
s
evaluates to eithertrue
orfalse
(because these are the only values that satisfy the logical predicate⟦bool⟧
). Ifs
evaluates totrue
, then we know that it evaluates to the value thatt₁
evaluates to (also given to us by the inductive hypothesis). The same applies ifs
evaluates tofalse
.
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 fundamentallemma ⊢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.
Generally, the semantics of STLC is defined with substitutions. Assuming I am
using a smallstep semantics (though I can also do a bigstep semantics) where
a term t
steps to another term t′
(t ⟶ t′
), the rule for stepping an
application is as follows:
(λx. t) s ⟶ t[s/x]
where t[s/x]
represents “t
with s
substituted for all instances of the
variable x
.”
As mentioned in the beginning of this blog post, substitutions have been perhaps one of the biggest roadblocks in the mechanization of proofs by logical relations (and really the mechanization of proofs of properties of programs). Even proving type soundness by a logical relation in a proof assistant requires a lot of substitution lemmas to be proven first.
The Agda mechanization in this blog post has no mention of substitutions, which
is by design. This is thanks to two decisions: 1) using a bigstep semantics,
and 2) evaluating terms in environments. Evaluating terms in environments
results in a sort of “delayed” substitution that occurs when a variable is
actually evaluated (e.g. evalVar
).
These two decisions are not necessarily extensible to more complicated proofs (though I am interested in putting that to the test!), instead the goal was to show a logical relation in Agda without first needing to go through a bunch of substitution lemmas.
If you continue to work with logical relations and proof assistants, you will likely end up needing to actually dive into substitutions one day. The “Substitution” chapter in the appendix of PLFA is a great resource for learning the substitution lemmas you need to prove. However, you are in luck because a lot of people have done a ton of work to make this process easier!
The POPLmark Reloaded team developed tools such as the
genericsyntax
Agda library that
can be used to avoid having to prove substitution lemmas yourself. They have
also developed Autosubst 2, a tool that
generates Coq definitions along with substitution lemmas when provided a
“signature” file defining your object language. These tools are really great,
and you should definitely use them! However, I find them hard to use to write a
short and selfcontained mechanized tutorial.
Separately, there is also the Beluga proof assistant. Beluga is this really cool proof assistant that has a separate “layer” for representing syntax. The result is (as an oversimplification), that we are no longer burdened with proving substitution lemmas. The paper “Firstclass substitutions in contextual type theory” by Cave and Pientka goes over an example of type soundness of STLC that makes this evident.
Beluga is awesome, but its ideas are not currently implemented in a generalpurpose proof assistant, though I dream of a day where that would be the case! That is why this blog post tries to show a proof by logical relations that can be presented in generalpurpose proof assistants like they are today. On that note, if you, the reader, ever feel excited to translate this Agda development to Coq or Lean, do let me know!