Functions

Type formation rule

{a : type, b : type \over a → b : type}

The → ought to be read as “assuming a is proven, then b is proven”.

Construction

{Γ, x : a ⊢ y : b \over Γ ⊢ λx. y : a → b}

Whenever the function is constructed, x : a becomes a new variable available for constructing the b. The ⊢ describes changes to the scope.

Elimination

{f : a → b, x : a \over f x : b}

Convertibility rules

\def\arraystrech{1.1} \begin{array}{cccc} f & \backsim & λx.f x & eta\ conversion \\ (λx.y) z & \backsim & y\{x:=z\} & beta\ conversion \end{array}

Use of eta-conversion rule requires that f does not contain the variable x.

The braces in beta conversion stand for substitution.

Function composition

f : c → b, g : a → b \over f.g : a → c

Function composition is associative

f . (g . h) = (f . g) . h = f . g . h

Scope

The Γ is a comma separated list of variables associated with types.

The variables in the scope are available for building the term that is enclosed to the scope. We can do this a bit more explicit with De-Bruijn indexing.

{\over Γ, x : a ⊢ x : a} 0 \quad {Γ ⊢ y : b \over Γ, x : a ⊢ y : b} \text{---} +1

The De-Bruijn indexing prevents potential confusion with variable names that can occur when terms are copied around.

λx.λy.λz. x (y z)

The indexing removes the variable names entirely and makes it explicit what the variable refers to. To not confuse the scope variables with ordinary numbers, they are marked with a check over them. This expression is equivalent with the above expression.

λλλ\check{2}\ (\check{1}\ \check{0})

Substitution

To illustrate what the substitution is doing, lets look at the scope in the elimination rule.

{Γ ⊢ f : a → b,\quad Γ ⊢ x : a \over Γ ⊢ f\ x : b}

The type for f reveals that it’s a function, therefore we can use the eta-conversion rule to it.

{{ Γ, y : a ⊢ f y : b \over Γ ⊢ (λy. f y) : a → b},\quad Γ ⊢ x : a \over Γ ⊢ f\ x : b}

It reveals that we can remove the lambda around the expression and put it up into the scope into the place of that variable.

When we move up the variable in the proof, we have to verify that manipulations you do to the structure preserves the scope.

Γ, (Γ ⊢ x:a) ⊢ ...

If you pass over a function being constructed. It introduces a variable, but note how the substitution keeps refering to the context where it was retrieved from.

Γ, (Γ ⊢ x:a), y:b ⊢ ...

You can consider how each De-bruijn index should be replaced.

Γ, (Γ ⊢ x:a), y:b ⊢ \check{0} \\ Γ, (Γ ⊢ x:a), y:b ⊢ \check{1} \\ Γ, (Γ ⊢ x:a), y:b ⊢ \check{2}

The resulting scope should appear like this:

Γ, y:b ⊢ ...

1. Indices ending up below substitution can stay same.
2. Indices intersecting the substitution need to be replaced by the x:a, but the scope (Γ ⊢ x:a) must be first converted to (Γ, y:b ⊢ x:a).
3. Indices skipping the substituted variable should decrement by one.

Exercises (2)

 1. Function composition can be implemented with construction and elimination rules. To implement composition, complete this program:

composition : ∀a.∀b.∀c. (b → c) → (a → b) → (a → c)
composition = λf.λg.λx. _

Context on the hole:

  ∀a.∀b.∀c.
  f : b → c,
  g : a → b,
  x : a
⊢ _ : c

If you need to know what ∀ are, peek up on the next chapter.

 2. See if you can prove that composition is associative. Here’s the composition rule opened up, replace the compose here with your program and apply convertibility rules.

compose f (compose g h) = compose (compose f g) h