Type Theory – The Untyped Lambda Calculus

The Untyped Lambda Calculus or the pure lambda calculus forms the computational substrate for most of the type systems.

Peter Landin observed that complex programming languages can be understood as having a tiny core with all the complex features implemented in the tiny core.

Lambda Calculus can be viewed as a simple programming language or as a mathematical object about which statements can be proved.

Everything is a function.

Definition 1 Lambda Term: It refers to any term in the lambda calculus.

Definition 2 Lambda Abstraction: Lambda terms beginning with a {\lambda} are called lambda abstractions.

There are three kind of terms in the lambda calculus.

  1. A variable {x} itself is a term.
  2. The abstraction of a variable from a term written as {\lambda{x.t}} is a term called a lambda abstraction.
  3. The application of a term to another term is written as {t t}.

The grammar can be summarized as:

Syntax:

\displaystyle  {t} := \text{terms} \\ := {x} \thickspace \text{variable} \\ := \lambda {x.t} \thickspace \text{lambda abstraction} \\ := {t \thickspace t} \thickspace \text{application} \ \ \ \ \ (1)

To save writing too many parenthesis the convention is that the

  1. application associates to the left, that is, is {s t u} is {(s t) u}.
  2. abstraction extend as far to the right as possible. For example, {\lambda{x.} \lambda{y.x \thickspace y \thickspace x}} is {\lambda{x.(} \lambda{y.(x \thickspace y) \thickspace x)}}.

1. Scope

A variable is said to be bound when it occurs in the body {t} of an abstraction {\lambda{x.t}}.

A variable is said to be free if it is not bound by enclosing abstraction on {x}

An abstraction with no free variables is said to be closed or a combinator.

2. Operational Semantics

In its pure form, lambda calculus has no mechanism for computation except function application, functions are applied to arguments which are themselves functions. Each step in computation is rewriting an application by replacing the value of the bound variable of the lambda abstraction with the argument given on the right side of the application.

\displaystyle  (\lambda x.{t}_{12}){t}_2 \rightarrow [{x} \thickspace \rightarrow \thickspace {t}_2] {t}_{12} \ \ \ \ \ (2)

There can be many different evaluation strategies.

  • Full-beta Reduction: Any redex may be reduced at any time.

    \displaystyle  (\lambda x.x)((\lambda x.x)(\lambda z.(\lambda x.x) \thickspace z)) \ \ \ \ \ (3)

  • Normal Order Strategy: The outermost redex is reduced first. It is a partial function and each evaluation gives a unique term.
  • Call by Name: In addition to the outermost redex being reduced first, no evaluation is allowed inside abstractions.
  • Call by Need: A reduction relation on abstract syntax graph, instead of abstract syntax trees.
  • Call by Value:

    3. Multiple Arguments

    \displaystyle  \lambda (x \thickspace y).s = \lambda x. \thickspace \lambda y. \thickspace s \ \ \ \ \ (4)

    4. Church Booleans

    \displaystyle  {tru} \thickspace = \lambda {t.} \thickspace \lambda {f.} {t} \\ {fls} = \lambda {t.} \lambda {f.} {f} \\ {test} = \lambda {l.} \lambda {m.} \lambda {n.} {l m n} \\ {test \thickspace b \thickspace v \thickspace u} = {b \thickspace v \thickspace u} \\ {and} = \lambda {b.} \lambda {c.} {b \thickspace c \thickspace fls} \ \ \ \ \ (5)

    5. Pairs

    \displaystyle  {pair} = \lambda {f.} \lambda {s.} \lambda {b.} {b \thickspace f \thickspace s} \\ {fst} = \lambda {p.} {p \thickspace tru} \\ {snd} = \lambda {p.} {p \thickspace fls} \\ {fst \thickspace (pair \thickspace v \thickspace w)} = (\lambda {p.} {p \thickspace tru})((\lambda {f.} \lambda {s.} \lambda {b.} {b \thickspace f \thickspace s}) { v \thickspace w}) \\ = (\lambda {p.} {p \thickspace tru})((\lambda {s.} \lambda {b.} {b \thickspace v \thickspace s}) { w}) \\ = (\lambda {p.} {p \thickspace tru})(\lambda {b.} {b \thickspace v \thickspace w}) \\ = (\lambda {b.} {b v w}) { tru} \\ = ({tru \thickspace v \thickspace w}) \\ = {v} \ \ \ \ \ (6)

    6. Church Numerals

    \displaystyle  {c}_0 = \lambda {s.} \lambda {z.} {z} \\ {c}_1 = \lambda {s.} \lambda {z.} {s \thickspace z} \\ {c}_2 = \lambda {s.} \lambda {z.} {s \thickspace (s \thickspace z)} \\ {c}_3 = \lambda {s.} \lambda {z.} {s \thickspace (s \thickspace (s \thickspace z))} \\ {scc} = \lambda {n.} \lambda {s.} \lambda {z.} {s \thickspace (n \thickspace s \thickspace z)}. \ \ \ \ \ (7)

    A number n is encoded by the action of applying a function s to z n times.

    7. Recursion

    \displaystyle  {omega} = (\lambda {x.} {x \thickspace x})(\lambda {x.} {x \thickspace x}) \\ {fix} = \lambda {f.} ( \lambda {x.} {f} ( \lambda {y.} {x \thickspace x \thickspace y} ) ) ( \lambda {x.} {f} ( \lambda {y.} {x \thickspace x \thickspace y} ) ) \ \ \ \ \ (8)

    \displaystyle  {factorial} = {body \thickspace containing \thickspace factorial} \\ {g} = \lambda {fct.body \thickspace containing \thickspace fct} \\ {g} = \lambda {fct.(}\lambda {n.if \thickspace (cnd) \thickspace then \thickspace (c1) \thickspace else \thickspace (times \thickspace n \thickspace (fct \thickspace (prd \thickspace n))))} \\ {factorial} = {fix \thickspace g} \\ {h1} = \lambda {x.g(}\lambda {y.x \thickspace x \thickspace y)} \\ {fct} = \lambda {y.h1 \thickspace h1 \thickspace y} \\ {factorial c_3} = {fix \thickspace g \thickspace c}_3 \\ = {h1 \thickspace h1 \thickspace g \thickspace c_3 } \ \ \ \ \ (9)

    factorial = fix (lambda fct. body containing fct)

    8. Formalities

    Definition 3 The set of terms is the smallest set such that

    1. If {x \in \mathcal{V}}, then {x \in \mathcal{T}}.
    2. If elements {x, t \in \mathcal{T}}, then {\lambda {x.t} \in \mathcal{T}}.
    3. If {{u, v} \in \mathcal{T}}, then {{u v} \in \mathcal{T}}.

    Definition 4 The set of free variables of a term {t}, written as {FV(t)} is defined as the set

    1. {FV(x) = x}
    2. {FV(\lambda x.t) = FV(t) \textbackslash x}
    3. {FV(t_1 t_2) = FV(t_1) \cup FV(t_2)}.

    Definition 5 Substituiton:

    \displaystyle  (x \mapsto s)x = x \ \ \ \ \ (10)

    \displaystyle  (x \mapsto s)y = y y \neq x \ \ \ \ \ (11)

    \displaystyle  (x \mapsto s)(\lambda y.t) = (\lambda y.(x \mapsto s)t) y \neq x, y \notin FV(s) \ \ \ \ \ (12)

    \displaystyle  (x \mapsto s)(t_1 \thinspace t_2) = ((x \mapsto s)t_1 \thinspace (x \mapsto s)t_2) \ \ \ \ \ (13)

    Syntax:

    \displaystyle  {t} := \thickspace \text{terms} \\ := {x} \thickspace \text{variable} \\ := \lambda {x.t} \thickspace \text{lambda abstraction} \\ := {t \thickspace t} \thickspace \text{application} \\ {v} := \thickspace \text{values} \\ := \lambda{x.t} \thickspace \text{variable} \\ \ \ \ \ \ (14)

    Evaluation:

    \displaystyle  \frac{ t_1 \thickspace \rightarrow \thickspace t'_1 }{ t_1\thinspace t_2 \rightarrow t'_1\thinspace t_2 } \text{E-App1} \\ \frac{ t_2 \rightarrow t'_2 }{ v_1\thinspace t_2 \rightarrow v_1\thinspace t'_2 } \text{E-App2} \\ (\lambda x.t_1)\thinspace v_2 \rightarrow [x \mapsto v_2]t_1 \text{E-AppAbs} \ \ \ \ \ (15)

  • Type Theory – Untyped Arithmetic Expressions

    The following are present in this first language:

    • true and false.
    • conditional expressions.
    • The numeric constant 0.
    • The arithmetic operators succ and prec.
    • A testing operation iszero.

    t = true

    false

    if t then t else t

    0

    succ t

    prec t

    iszero t

    Programs

    A program in the above language is a term built up from the forms given in the grammar.

    if false then 0 else 1

    {\triangleright} 1

    1. Syntax

    The grammar above is a way to specify the syntax of the language. One other way to do so is to specify it inductively using set theory.

    Definition 1 Terms, Inductively: The set of terms is the smallest set { \mathcal{T} } such that

    1. {true, false, 0} {\subseteq \mathcal{T}}.
    2. if {t_1} {\in \mathcal{T}} then succ({t_1}), pred({t_1}), iszero({t_1}) {\subseteq \mathcal{T}}.
    3. if {t_1} {\in \mathcal{T}}, {t_2 \in \mathcal{T}} and {t_3 \in \mathcal{T}} then if {t_1} then {t_2} else {t_3 \in \mathcal{T}}.

    Definition 2 Terms, By Inference Rules: The set of terms is defined by the following rules:

    Rules set 1:

    \displaystyle  true \in \mathcal{T} \ \ \ \ \ (1)

    \displaystyle  false \in \mathcal{T} \ \ \ \ \ (2)

    \displaystyle  0 \in \mathcal{T} \ \ \ \ \ (3)

    Rules set 2:

    \displaystyle  \frac{t_1 \in \mathcal{T}}{succ(t_1) \in \mathcal{T}} \ \ \ \ \ (4)

    \displaystyle  \frac{t_1 \in \mathcal{T}}{pred(t_1) \in \mathcal{T}} \ \ \ \ \ (5)

    \displaystyle  \frac{t_1 \in \mathcal{T}}{iszero(t_1) \in \mathcal{T}} \ \ \ \ \ (6)

    Rules set 3:

    \displaystyle  \frac{ t_1 \in \mathcal{T}, \thickspace t_2 \in \mathcal{T}, \thickspace t_3 \in \mathcal{T} } {t_1 \thickspace then \thickspace t_2 \thickspace else \thickspace t_3 \in \mathcal{T}}. \ \ \ \ \ (7)

    Each rule is read “If we have established the statements in the premise of the rules above, then the we may derive the conclusions in the lines below”. The rules with no premises are called axioms.

    Definition 3 Terms, Concretely: The set of terms can also be given by constructing sets of successively bigger sizes.

    For each natural number {i} we define a set {\mathcal{S}_i} as follows:

    \displaystyle  \mathcal{S}_0 = \emptyset \\ \ \ \ \ \ (8)

    \displaystyle  \mathcal{S}_{i + 1 } = {true, false, 0\} \\ \cup \quad {succ(t_1), \thickspace pred(t_1), \thickspace iszero(t_1) \thickspace | \thickspace t_1 \thickspace \in \mathcal{S}_i} \\ \cup \quad {if \thickspace t_1 \thickspace then \thickspace t_2 \thickspace else \thickspace t_3 }\thickspace | \thickspace t_1, \thickspace t_2, \thickspace t3 \in \mathcal{S}_i}. \ \ \ \ \ (9)

    Finally, let

    \displaystyle  \mathcal{S} = \bigcup_{i=1}^n \mathcal{S}_i \ \ \ \ \ (10)

    Inference rules are just another way of writing the set theoretic definition.

    Each inference rule may imply an infinite tree of terms.

    Proposition 4 {\mathcal{T} = \mathcal{S}}.

    In definition on page we saw that a term can have one of three forms. This can be used in two ways:

    • to give inductive definitions of functions over set of terms.
    • in proving theorems about the properties of terms.

    The consts, size and depth functions can be defined using inductive definition over the set of terms. Relations between sizes and depths, the cardinality of consts and size can be proven using the definition of the set of terms.

    2. Semantic Styles

    2.1. Operational Semantics

    The behaviour of the program is described by specifying an abstract machine for it.

    The machine is abstract in the sense that the terms of the program are what form the machine code, instead of some low level language.

    The terms are represented by states of an abstract machine. The meaning of a program is represented by the output of the computation of the abstract machine whose starting state is the first term of the program, that is the value in the final state.

    It is customary to give two or more different operational semantics for a single language. One closer to the language in question and the other closer to the machine language.

    Proving that the above two operational semantics correspond in some suitable sense amounts to proving that the implementation is correct.

    2.2. Denotational Semantics

    It takes a more abstract view of meaning and instead of defining the meaning of terms in terms of a sequence of machine states, the meaning of term is defined to be some mathematical object – a function or a number.

    3. Evaluation

    Consider a language with grammar as below:

    Syntax:

    \displaystyle  t = \thickspace \text{terms} \\ = true \thickspace \text{constant true} \\ = false \thickspace \text{constant false} \\ = if \thickspace t \thickspace then \thickspace t \thickspace else \thickspace t \thickspace \text{conditional} \\ \text{v} = \thickspace \text{values} \\ = true \thickspace \text{true value} \\ = false \thickspace \text{false value} \ \ \ \ \ (11)

    Values, a subset of terms, are the possible final outcomes of evaluation.

    The evaluation relation is a binary relation on the set of terms.

    Evaluation: t {\rightarrow} t

    \displaystyle  if \thickspace true \thickspace then \thickspace t \thickspace else \thickspace u \thickspace \rightarrow \thickspace t \thickspace \text{E-IfTrue} \\ if \thickspace false \thickspace then \thickspace t \thickspace else \thickspace u \thickspace \rightarrow u \thickspace \text{E-IfFalse} \\ \frac{t \rightarrow u} { if \thickspace t \thickspace then \thickspace v \thickspace else \thickspace w \thickspace \rightarrow \thickspace if \thickspace u \thickspace then \thickspace v \thickspace else \thickspace w } \text{\textsc{E-If}} \ \ \ \ \ (12)

    Definition 5 Evaluation Strategy: The interplay between the rules determines a particular order of evaluation.

    Definition 6 Computation Rules:

    Definition 7 Congruence Rules:

    Definition 8 An instance of an inference rule is obtained by replacing the metavariables in the premises and conclusions of the rule.

    Definition 9 A rule is satisfied by a relation if each instance of the rule the conclusion is in the rule or one of the premises is not.

    Definition 10 A one-step evaluation relation {\rightarrow} is the smallest binary relation on the set of terms which satisfies all the evaluation inference rules for the set of terms.

    Definition 11 When a pair (t, t’) is in the one-step evaluation relation we say that the evaluation statement t {\rightarrow} t’ is derivable .

    Theorem 12 (Determinacy of One-Step Evaluation) If t {\rightarrow} t’ and t {\rightarrow} t”, then t’ {=} t”.

    Definition 13 A term t is in normal form if no evaluation rule applies to it, i.e.\, if there is no t’ such that t {\rightarrow} t’.

    Theorem 14 Every value is in normal form.

    Theorem 15 If t is in normal form, then t is a value.

    Definition 16 The multi-step evaluation relation {\rightarrow^{*}} is the reflexive, transitive closure of the one-step evaluation relation. If t {\rightarrow} t’ and t’ {\rightarrow} t”, then t {\rightarrow} t”.

    Consider a language with grammar as below:

    Syntax:

    \displaystyle  t = \text{terms} \\ = 0 \thickspace \text{constant 0} \\ = succ \thickspace t \thickspace \text{successor} \\ = pred \thickspace t \thickspace \text{predecessor} \\ = iszero \thickspace t \thickspace \text{zero test} \\ = true \thickspace \text{constant true} \\ = false \thickspace \text{constant false} \\ = if \thickspace t \thickspace then \thickspace t \thickspace else \thickspace t \thickspace \text{conditional} \\ \text{v} = \text{values} \\ = true \thickspace \text{true value} \\ = false \thickspace \text{false value} \\ = nv \text{numeric value} \\ \text{nv} = \text{numeric values} \\ = 0 \thickspace \text{0 value} \\ = succ \thickspace nv \thickspace \text{successor value} \ \ \ \ \ (13)

    Values, a subset of terms, are the possible final outcomes of evaluation.

    The evaluation relation is a binary relation on the set of terms.

    Evaluation: t {\rightarrow} t

    \displaystyle  if \thickspace true \thickspace then \thickspace t \thickspace else \thickspace u \thickspace \rightarrow \thickspace t \thickspace \text{E-IfTrue} \\ if \thickspace false \thickspace then \thickspace t \thickspace else \thickspace u \thickspace \rightarrow \thickspace u \thickspace \text{E-IfFalse} \\ \frac{t \thickspace \rightarrow \thickspace u}{if \thickspace t \thickspace then \thickspace v \thickspace else \thickspace w} \rightarrow if \thickspace u \thickspace then \thickspace v \thickspace else \thickspace w \text{\textsc{E-If}} \ \ \ \ \ (14)

    Type Theory – Mathematical Preliminaries

    1. Sets, Relations and Functions

    Definition 1 Countable Set: A set is countable if it can be placed in one-to-one correspondence with the set of natural numbers {\mathbb{N}}.

    Definition 2 n-place Relation: An n-place relation on a collection of sets {\mathcal{S}_1, \mathcal{S}_2, \dotsc, \mathcal{S}_n} is a set {R} of tuples {R \subseteq \mathcal{S}_1 \times \mathcal{S}_2 \times \dotsc \times \mathcal{S}_n}. We say that elements {s_1 \in \mathcal{S}_1} through {s_n \in \mathcal{S}_n} are related by {R} if {(s_1, s_2, \dotsc, s_n) \in R}.

    Definition 3 Predicates: A one place relation is also called a predicate. One-place relation on a set {\mathcal{S}} is a subset {P} of {\mathcal{S}}. It is written as {P(s)} instead of {s \in P}.

    Definition 4 Binary Relation: A two place relation on sets {\mathcal{S}} and {\mathcal{T}} is also called a binary relation on the two sets. It is written as {s} {R} {t} instead of {(s, t) \in R}.

    Three or more place relations are written using the mixfix syntax. The elements are separated by symbols. For example, {\Gamma \dashv \mathsf{s} : \mathsf{T}} stands for the triple {(\Gamma, \mathsf{s}, \mathsf{T})}.

    Definition 5 Domain: The domain of a relation is the set of elements from the first set which are present in the tuples in the relation set.

    Definition 6 Range: The domain of a relation is the set of elements from the first set which are present in the tuples in the relation set.

    Definition 7 Partial Function: A binary relation {R} is a partial function if, whenever {(s, t_1) \in R} and {(s, t_2) \in R}, then, we have {t_1 = t_2 }.

    Definition 8 Total Function: A partial function {R} is also a total function if the domain of R is the whole set.

    Definition 9 A partial function {R} is said to be defined for an element {s \in \mathcal{S}} if {(s, t) \in R} for some {t \in \mathcal{T}}. Otherwise, we write {f(x)\uparrow} or {f(x) = \uparrow} to mean “{f} is undefined on {x}”.

    2. Ordered Sets

    Definition 10 Reflexive Relation: A binary relation {R} on {\mathcal{S}} is said to be reflexive if {(s, s) \in R} for all {s \in \mathcal{S}}.

    Reflexiveness only makes sense for binary relations defined on a single set.

    Definition 11 Symmetric Relation: A binary relation {R} on {\mathcal{S}} is said to be symmetric if {(s, t) \in R \Rightarrow (t, s) \in R} for all {s, t \in \mathcal{S}}.

    Definition 12 Transitive Relation: A binary relation {R} on {\mathcal{S}} is said to be transitive if {(s, t) \text{ and } (t, u) \in R \Rightarrow (s, u) \in R} for all {s, t, u \in \mathcal{S}}.

    Definition 13 Anti-Symmetric Relation: A binary relation {R} on {\mathcal{S}} is said to be anti-symmetric if {(s, t) \in R \text{ and } (t, s) \in R \Rightarrow s = t} for all {s, t \in \mathcal{S}}.

    Definition 14 Preorder: A reflexive and transitive relation on a set is called a preorder on that set. Preorders are usually written using symbols such as {\leq} or {\sqsubseteq}.

    Definition 15 Partial Order: A preorder which is also anti-symmetric is called a partial order.

    Definition 16 Total Order: A partial order with the property that for every two elements {s, t \in \mathcal{S}} we have either {s \leq t} or {s \geq t}.

    Definition 17 Join of two elements: It is the lowest upper bound for the set of elements which are greater than given two elements with respect to the partial order.

    Definition 18 Meet of two elements: It is the greatest lower bound for the set of elements which are smaller than given two elements with respect to the partial order.

    Definition 19 Equivalence Relation: A binary relation on a set is called an equivalence relation if it is reflexive, symmetric and transitive.

    Definition 20 Reflexive Closure: A reflexive closure of a binary relation {R} on a set {\mathcal{S}} is the smallest reflexive relation {R'} which contains {R}. (Smallest in the sense that if some other reflexive relation {R''} also contains {R} then {R' \subset R''}).

    Definition 21 Transitive Closure: A transitive closure of a binary relation {R} on a set {\mathcal{S}} is the smallest transitive relation {R'} which contains {R}. (Smallest in the sense that if some other transitive relation {R''} also contains {R} then {R' \subset R''}). It is written as {R^{+}}.

    Definition 22 Sequence: A transitive closure of a binary relation {R} on a set {\mathcal{S}} is the smallest transitive relation {R'} which contains {R}. (Smallest in the sense that if some other transitive relation {R''} also contains {R} then {R' \subset R''}). It is written as {R^{+}}.

    Definition 23 Permutation: A transitive closure of a binary relation {R} on a set {\mathcal{S}} is the smallest transitive relation {R'} which contains {R}. (Smallest in the sense that if some other transitive relation {R''} also contains {R} then {R' \subset R''}). It is written as {R^{+}}.

    Definition 24 Decreasing Chain: A transitive closure of a binary relation {R} on a set {\mathcal{S}} is the smallest transitive relation {R'} which contains {R}. (Smallest in the sense that if some other transitive relation {R''} also contains {R} then {R' \subset R''}). It is written as {R^{+}}.

    Definition 25 Well Founded Preorder: A transitive closure of a binary relation {R} on a set {\mathcal{S}} is the smallest transitive relation {R'} which contains {R}. (Smallest in the sense that if some other transitive relation {R''} also contains {R} then {R' \subset R''}). It is written as {R^{+}}.

    3. Induction

    Axiom (Principle of Ordinary Induction) Suppose that {P} is a predicate defined on natural numbers. Then:

    If {P(0)}

    and, for all {i}, {P(i)} implies {P(i + 1)},

    then, {P(n)} holds for all {n \in N}.

    Sicp Exercise 3.23

    Exercise 3.23.  A deque (“double-ended queue”) is a sequence in which items can be inserted and deleted at either the front or the rear. Operations on deques are the constructor make-deque, the predicate empty-deque?, selectors front-deque and rear-deque, and mutators front-insert-deque!, rear-insert-deque!, front-delete-deque!, and rear-delete-deque!. Show how to represent deques using pairs, and give implementations of the operations.23 All operations should be accomplished in (1) steps.

     

     

    Sicp Exercise 3.50

    Exercise 3.50.  Complete the following definition, which generalizes stream-map to allow procedures that take multiple arguments, analogous to map in section 2.2.3, footnote 12.

    (define (stream-map proc . argstreams)
    (if (<??> (car argstreams))
    the-empty-stream
    (<??>
    (apply proc (map <??> argstreams))
    (apply stream-map
    (cons proc (map <??> argstreams))))))

     

     

     

    Sicp Exercise 3.35

    Exercise 3.35.  Ben Bitdiddle tells Louis that one way to avoid the trouble in exercise 3.34 is to define a squarer as a new primitive constraint. Fill in the missing portions in Ben’s outline for a procedure to implement such a constraint:

    (define (squarer a b)
    (define (process-new-value)
    (if (has-value? b)
    (if (< (get-value b) 0)
    (error "square less than 0 -- SQUARER" (get-value b))
    <alternative1>)
    <alternative2>))
    (define (process-forget-value) <body1>)
    (define (me request) <body2>)
    <rest of definition>
    me)

     

     

    Sicp Exercise 3.34

    Exercise 3.34.  Louis Reasoner wants to build a squarer, a constraint device with two terminals such that the value of connector b on the second terminal will always be the square of the value a on the first terminal. He proposes the following simple device made from a multiplier:

    (define (squarer a b)
    (multiplier a a b))

    There is a serious flaw in this idea. Explain.