FLOLAC-STLC.lagda.md

Intrinsically-typed de Bruijn representation of simply typed lambda calculus

open import Data.Nat
open import Data.Empty
  hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
  hiding ([_])

Fixity declartion

infix  3 _⊢_ _=β_

infixr 7 _→̇_

infixr 5 ƛ_
infixl 7 _·_
infixl 8 _[_] _⟪_⟫
infixr 9 ᵒ_ `_ #_

Types

We only deal with function types and a ground type ⋆.

data Type : Set where
  ⋆   : Type
  _→̇_ : Type → Type → Type

Context

infixl 7 _⧺_
infixl 6 _,_
infix  4 _∋_

data Context : Set where
  ∅   :                  Context
  _,_ : Context → Type → Context

For convenience, we use symbols

• A, B, C for types
• Γ, Δ, and Ξ for contexts

In Agda this convention can be achieved by the keyword variable as follows.

variable
  Γ Δ Ξ : Context
  A B C : Type

Membership

Γ ∋ A means that A is a member of Γ.

There are two ways of estabilishing the judgement Γ ∋ A.

1. Γ , A ∋ A for any Γ and A, as we know that A is in the 0-th position.

2. If x : Γ ∋ A is a proof that A is in Γ, then Γ , B ∋ A holds.

How should we name these inference rules? Note that if we interpret the proof of Γ ∋ A as the position of A in Γ, then 1. should be Z (for zero) and 2. should be S (for successor).

data _∋_ : Context → Type → Set where
  Z   ---------
    : Γ , A ∋ A

  S_ : Γ     ∋ A
       ---------
     → Γ , B ∋ A

variable
  x     : Γ ∋ A

For example, S Z : ∅ , A , B ∋ A means A is in the first position. That is,

_ : ∅ , A , B ∋ A
_ = S Z 

Lookup is just _‼_ in Haskell. Agda is a total language, but lookup can only be partial with this type. We work around this problem by postulating ⊥, as we only use lookup for examples.

⊥-elim : ∀ {T : Set} → ⊥ → T
⊥-elim ()

lookup : Context → ℕ → Type
lookup (Γ , A) zero     =  A
lookup (Γ , B) (suc n)  =  lookup Γ n
lookup ∅       _        =  ⊥-elim impossible
  where postulate impossible : ⊥

If lookup Γ n finds the element in the n-th position, then the memberhsip proof can be produced algorithmatically. Hence we can transform a natural number to a membership proof.

count : (n : ℕ) → Γ ∋ lookup Γ n
count {Γ = Γ , _} zero     =  Z
count {Γ = Γ , _} (suc n)  =  S (count n)
count {Γ = ∅    }  _        =  ⊥-elim impossible
  where postulate impossible : ⊥

Examples

_ :  ∅ , A , B ∋ A
_ = count 1

_ : ∅ , B , A ∋ A
_ = count 0

Shifting

  (Aₙ , ... , A₁, A₀) 
    |    |     |   |
    ↓    ↓     ↓   ↓  
↦ (Aₙ , ... , A₁, A₀, B)

   n+1         2   1  0

ext
  : (∀ {A}   →     Γ ∋ A →     Δ ∋ A)
    ---------------------------------
  → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
ext ρ Z      =  Z
ext ρ (S x)  =  S (ρ x)

Concatenation

_⧺_ : Context → Context → Context
Γ ⧺ ∅       = Γ
Γ ⧺ (Δ , x) = Γ ⧺ Δ , x

Terms = typing rules

First off, since the typing rules for simply typed lambda calculus are syntax-directed, we combine the term formation rules with the typing rules.

Therefore, the typing judgement consists of only a context Γ and a Type with inference rules as term constructs. The collection of terms in simply typed lambda calculus is defined as an inducitve family indexed by a (given) context and a type.

data _⊢_ (Γ : Context) : Type → Set where

In our formal development we will use the position of λ to which the bound variable refer for the name of a variable. For example,

λ x. λ y. y

will be represented by

λ λ 0

This representation is called de Bruijn representation and the nubmer is a de Bruijn index. It also makes α-equivalence an equality on λ-terms.

Note that we have

Γ ∋ (x : A) 
-----------
Γ ⊢ x : A

in our informal development where x is now merely a number pointing to the position of A in Γ. We introduce a term x for a free variable in Γ just by giving its position in the context. Given Γ ⊢ M : A, the context Γ is the set of possibly free variables in M.

  `_ : Γ ∋ A
       -----
     → Γ ⊢ A

The definition of application is straightforward.

  _·_ : Γ ⊢ A →̇ B
      → Γ ⊢ A
        -----
      → Γ ⊢ B

In the informal development it takes a variable x and a term M to form λ x. M. Since the name of a variable does not matter at all in our formal development λ now takes a term M only.

Moreover, the position of a variable in the context Γ , A now refers to the innermost λ. Hence our definition

  ƛ_
    : Γ , A ⊢ B
      ---------
    → Γ ⊢ A →̇ B

For example, Z : (∅ , A) ⊢ A is a variable of type A under the context (∅ , A). After abstraction, ƛ Z : ∅ ⊢ A →̇ A is an abstraction under the empty context whose body is only a variable refering to the variable bound by λ.

As you may have observed, this inductive family Γ ⊢ A is just a variant of the natural deduction for propositional logic where inference rules are viewed as term constructs.

For convenience, the following symbols denote a term.

variable
  M N L M′ N′ L′ : Γ ⊢ A

Also for convenience, we compute the proof of Γ ∋ A by giving its position n (as a natural). In short, define # n as ` (count n)

#_ : (n : ℕ) → Γ ⊢ lookup Γ n
# n  =  ` count n

Examples

nat : Type → Type
nat A = (A →̇ A) →̇ A →̇ A

Recall that the Church numberal c₀ for 0 is

λ f x. x

In the de Bruijn representation, λ f x. x becomes

λ λ 0

c₀ : ∀ {A} → ∅ ⊢ nat A
c₀ = ƛ ƛ # 0

Similarly, c₁ ≡ λ f x. f x becomes

λ λ 1 0 

c₁ : ∀ {A} → ∅ ⊢ nat A
c₁ = ƛ ƛ # 1 · # 0

The addition of two Church numerals defined as

λ n. λ m. λ f. λ x. n f (m f x)

becomes

λ λ λ λ 3 1 (2 1 0)

add : ∀ {A} → ∅ ⊢ nat A →̇ nat A →̇ nat A
add = ƛ ƛ ƛ ƛ # 3 · # 1 · (# 2 · # 1 · # 0)

Exercise

Translate the following terms in the informal development to de Bruijn representation.

1. (id)   λ x. x
2. (fst)  λ x y. x
3. (if)   λ b x y. b x y
4. (succ) λ n. λ f x. f (n f x)

id : ∅ ⊢ A →̇ A
id = ƛ ` Z

fst : ∅ ⊢ A →̇ B →̇ A
fst = ƛ ƛ ` (S Z)

bool : Type → Type
bool A = A →̇ A →̇ A

if : ∅ ⊢ bool A →̇ A →̇ A →̇ A
if = ƛ ` Z

succ : ∅ ⊢ nat A →̇ nat A
succ = ƛ ` Z

Parallel Substitution

To define substitution, it is actually easier to define substitution for all free variable at once instead of one.

Rename : Context → Context → Set
Rename Γ Δ = ∀ {A} → Γ ∋ A → Δ ∋ A

Subst : Context → Context → Set
Subst Γ Δ = ∀ {A} → Γ ∋ A → Δ ⊢ A

As the de Bruijn index points to the position of a λ abstraction starting from the innermost λ, we need to increment/decrement the number when visiting/leaving λ.

For example, substituting M for x in the following term

x : A → A ⊢ x (λ y. y) 

becomes

0 (λ 0) [ M / 0 ] ≡ M (λ [ M ↑ / 1 ])

where M ↑ indicates that the de Bruijn index of a free variable which is incremented.

Therefore, a renaming function ρ : ∀ {A} → Γ ∋ A → Δ ∋ A becomes ext ρ : ∀ {A B} → Γ , B ∋ A → Δ , B ∋ A where B is the type of argument when visiting an abstraction λ.

rename : Rename Γ Δ
  → (Γ ⊢ A)
  → (Δ ⊢ A)
rename ρ (` x)   = ` ρ x
rename ρ (M · N) = rename ρ M · rename ρ N
rename ρ (ƛ M)   = ƛ rename (ext ρ) M

Similarly, we proceed with a substitution σ : ∀ {A} → Γ ∋ A → Δ ⊢ A. Note that

rename S_ : ∀ {A} → Γ ∋ A → Γ , B ∋ A

merely enlarges the context and increments the de Bruijn index for every Γ ∋ A.

exts : Subst Γ Δ → Subst (Γ , A) (Δ , A)
exts σ Z     = ` Z
exts σ (S p) = rename S_ (σ p)

_⟪_⟫
  : Γ ⊢ A 
  → Subst Γ Δ
  → Δ ⊢ A
(` x)   ⟪ σ ⟫ = σ x
(M · N) ⟪ σ ⟫ = M ⟪ σ ⟫ · N ⟪ σ ⟫
(ƛ M)   ⟪ σ ⟫ = ƛ M ⟪ exts σ ⟫

Singleton Substitution

Note that we only need to substitute the free variable corresponding to the outermost λ, i.e.

(λ x. M) N -→ M [ N / x ] 

where the free occurrence of x in M points to the outermost λ. Thus it suffices to define singleton subsitution for the non-empty context

Γ , x : A

which appears in the typing rule

Γ , x : A ⊢ M : B 
----------------------
Γ ⊢ λ x : A. M : A → B

It follows that the singleton substitution is a special case of parallel substitution given by

σN : ∀ {A} → Γ , B ∋ A → Γ ⊢ A 

for some N : Γ ⊢ B so that _⟪ σN ⟫ : Γ , B ⊢ A → Γ ⊢ A.

subst-zero : {B : Type}
  → Γ ⊢ B
  → Subst (Γ , B) Γ
subst-zero N Z     =  N
subst-zero _ (S x) =  ` x

_[_] : Γ , B ⊢ A
     → Γ ⊢ B
       ---------
     → Γ ⊢ A
_[_] N M =  N ⟪ subst-zero M ⟫

Single-step reduction

In our informal development -→β is defined only for beta-redex followed by one-step full β-reduction. These two rules can be combined altogether.

infix 3 _-→_
data _-→_ {Γ} : (M N : Γ ⊢ A) → Set where
  β-ƛ·
    : (ƛ M) · N -→ M [ N ]

  ξ-ƛ
    :   M -→ M′
    → ƛ M -→ ƛ M′    
  ξ-·ₗ
    :     L -→ L′
      ---------------
    → L · M -→ L′ · M
  ξ-·ᵣ
    :     M -→ M′
      ---------------
    → L · M -→ L · M′

Reduction sequence of -→

The reduction sequence M -↠ N from M to N is just a list of reductions such that the RHS of a head reduction must be the LHS of the tail of reductions.

data _-↠_ {Γ A} : (M N : Γ ⊢ A) → Set where
  _∎ : (M : Γ ⊢ A)
    → M -↠ M       -- empty list
    
  _-→⟨_⟩_
    : ∀ L          -- this can usually be inferred by the following reduction 
    → L -→ M       -- the head of a list 
    → M -↠ N       -- the tail
      -------
    → L -↠ N

infix  2 _-↠_ 
infixr 2 _-→⟨_⟩_
infix 3 _∎

The relation -↠ is also transitive in the sense that

if L -↠ M and M -↠ N then L -↠ N

the proof itself is in fact the concatenation of two lists.

_-↠⟨_⟩_ : ∀ L
  → L -↠ M → M -↠ N
  -----------------
  → L -↠ N
M -↠⟨ L-↠M ⟩ M-↠N = {!!}

infixr 2 _-↠⟨_⟩_

Exercise

Show that -↠ is a congruence. That is, show the following lemmas.

ƛ-↠ : M -↠ M′
      -----------
    → ƛ M -↠ ƛ M′
ƛ-↠ M-↠M′       = {!!}
  
·-↠ : M -↠ M′
    → N -↠ N′
    → M · N -↠ M′ · N′
·-↠ M-↠M′ N-↠N′ = {!!}

Computational equality

In (untyped) lambda calculus, we say that two terms M and N are computationally equal denoted by M =β N if either

1. M -→ N

2. M =β M

3. M =β N
   ------
   N =β M

4. L =β M    M =β N
   ----------------
       L =β N

Correspondingly, we introduce an inductive type family where each case is a constrctor of that type family:

data _=β_ {Γ : Context} : Γ ⊢ A → Γ ⊢ A → Set where
  =β-beta
    : M -→ N → M =β N

  =β-refl
    : M =β M

  =β-sym
    : N =β M → M =β N

  =β-trans
    : L =β M → M =β N
    → L =β N

Homework Solution in Agda

Show that if M -↠ N and M is in normal form then M ≡ N (every two α-equivalent terms are exactly equal in de Bruijn representation).

HW2 : M -↠ N → (∀ N → ¬ (M -→ N)) → M ≡ N
HW2 M-↠N M↛ = {!!}

Normal form

Recall that a term M is in normal form if M --̸→ N for any N. This property can be characterised completely by its syntax. The characterisation is given as follows:

λ x₁ x₂ ⋯ xₙ. x N₁ N₂ ⋯ ⋯ ⋯ Nₘ  
│             ╰── Neutral ──╯│  
╰────────── Normal ──────────╯  

where x is a (free or bound) variable, Nᵢ's are all in normal form, and n and m can be zero. The syntax is devided into two categories:

• neutral terms: the neutral part indicates a spine of normal terms starting from a variable

• normal terms: a sequence of abstractions λ followed by neutral terms

Neutral terms are those normal terms which do not create any further β-redexs during substitution. This characterisation is defined as two mutually-defiend inductive families.

data Neutral : Γ ⊢ A → Set 
data Normal  : Γ ⊢ A → Set 

data Neutral where
  `_  : (x : Γ ∋ A)
    → Neutral (` x)
  _·_ : Neutral L
    → Normal M
    → Neutral (L · M)

data Normal where
  ᵒ_  : Neutral M → Normal M
  ƛ_  : Normal M  → Normal (ƛ M)

The soundness of characterisation is proved by induction on the derivation of Normal M (resp. Neutral M) and if necessary on M -→ M.

The completeness is proved by induction on the derivation of M (or Γ ⊢ M : A) and by contradiction using ⊥-elim : ⊥ → A. so that we can deduce any property we need once we derive a contradication ⊥.

Proofs are left as exercises.

Exercise

normal-soundness  : Normal M  → ¬ (M -→ N)
neutral-soundness : Neutral M → ¬ (M -→ M′)

normal-soundness  M = {!!}
neutral-soundness M = {!!}

normal-completeness
  : (M : Γ ⊢ A) → (∀ N → ¬ (M -→ N))
  → Normal M 
normal-completeness M = {!!}

Preservation

Preservation theorem is trivial in this formal development, since

M -→ N

is an inductive family indexed by two terms of the same type.

Progress

Progress theorem state that every well-typed term M is either

1. in normal form or
2. reducible

so we introduce a predicate Progress over well-typed terms M for this statement.

data Progress (M : Γ ⊢ A) : Set where
  step
    : M -→ N
      ----------
    → Progress M

  done : Normal M
    → Progress M

Progress theorm is proved by induction on the derviation of Γ ⊢ M : A in the informal and formal developments.

progress : (M : Γ ⊢ A)
  → Progress M
progress M = {!!}

Progress Theorem can be proved without Normal. Then, why bother? Despite of being logically equivalent, the proof becomes really ugly! Try the following exericse at your own risk.

data Progress′ (M : Γ ⊢ A) : Set where
  step
    : (r : M -→ N)
      ----------
    → Progress′ M

  done : (M↓ : (N : Γ ⊢ A) → M -→ N → ⊥)
    → Progress′ M

progress′ : (M : Γ ⊢ A) → Progress′ M
progress′ M = {!!}

如果你使用 Emacs 編輯 Agda 檔案，請將下列加入你的 Emacs 設定檔 .emacs讓 Emacs 可以辨認 Literate Agda in Markdown 格式

(setq auto-mode-alist
   (append
     '(("\\.agda\\'" . agda2-mode)
       ("\\.lagda.md\\'" . agda2-mode))
     auto-mode-alist))