Lambda calculus

Operational semantics

• Specifies behaviour of a language by specifying a simple abstract machine for it.
• This machine uses the terms of the language as instructions.
  • Simple language ⇒ state of machine is a term and transition function performs a simplification to proceed to next state.
  • Meaning of the term is the final state of the machine (when the term was the input).
• Sometimes useful to have multiple operational semantics for the same language. Some closer to the way machines see it and some closer to the way that humans see it. Then we can sort of chain proofs and prove correctness of the language. (I suppose this is how CompCert did it).

Denotational semantics

• Meaning of a term is taken as a mathematical object (like a number or function).
• Denotational semantics means finding semantic domains and defining an interpreter function mapping the terms of the language to elements in these domains.
• Highlights the essential properties of the language.
• Domain theory is a field that came out of the search for appropriate semantic domains for modeling various language features.
• Thoughtful selection of domains can let us derive powerful properties for reasoning about programs.
• Can't handle non-determinism and concurrency??

Axiomatic semantics

• Instead of assigning behaviour and then deriving laws and properties them, define the laws themselves first and then derive the behaviour.
• The laws themselves are the definition. Behaviour is whatever we can get from those laws.
• Meaning of a term is what can be proved about it.
• Focuses on the process of reasoning about programs.
• Procedures can't be handled properly??

Small step style

• Evaluation may be done in multiple steps.
• Computation progresses through individual steps guided by the evaluation relation till the term becomes a value.

Big step style

• aka Natural semantics
• Do everything in one step.
• Directly specifies that 'this term evaluates to this value'.
• t ⇓ v means that the term t evaluates to the value v.

Stuck term

• A term for which there is no further step in the evaluation relation but is still not a value.
• ie, the term is in normal form but is not a value.

Terms with free variables

ie, open terms.

We don't know how far is the binder (ie, λ) for a free variable. We need a naming context.

For example, in λx. y x, we know that x is 0 but are not sure about y.

Use a naming context (which is basically an assignation of de-Bruijn indices to the free variables) and use this assignment consistently.

Consider a naming context like

Γ = x ↦ 4
  | y ↦ 3
  | z ↦ 2
  | a ↦ 1
  | b ↦ 0

Then the terms could be 'translated' to:

| Named     | Nameless |
|-----------+----------|
| x (y z)   | 4 (3 2)  |
| λw. y w   | 4 0      |
| λw. λa. x | 6        |

for each binder, we got to increment the de-Bruijn index of the free variables.

Free variables

But can't have free variables in this notation? Though that isn't much of a problem as any term with a free variable can be made into a closed term.

Like: λx. x y being made into λy. (λ.x x y).

Church-Turing hypothesis

Lambda calculus with β-reduction is as powerful as a Turing machine.

It can express any computable function.

Syntax

term = x      -- variable
     | λx. t  -- abstraction
     | t₁ t₂  -- application

Substitution operation

We use an auxiliary operation called shifting for help in doing substitution.

The name of the bound variables are irrelevant as long as the naming is consistent.

For example, λx. x and λw. w are both same. The change in name doesn't make them different. Both are simply different forms of the identity function.

[1 ↦ s](λ.2)

shift(d, c) k       = k,     if k < c
                    | k + d, if k ≥ c

shift(d, c) (λ.t)   = λ. shift(d, c+1) t
shift(d, c) (t₁ t₂) = (shift(d, c) t₁) (shift(d, c) t₂)

-- if c is not mentioned, it is assumed to be 0

-- Exercise: 6.2.2
-- Part 1
shift(2) (λ.λ. 1 (0 2))
= λ. shift(2, 1) (λ. 1 (0 2))
= λ. λ. shift(2, 2) (1 (0 2))
= λ. λ. 1 (0 4)

-- Part 2
shift(2) (λ. 0 1 (λ. 0 1 2))
= λ. shift(2,1) (0 1 (λ. 0 1 2))
= λ. 0 3 (λ. shift(2,2) (0 1 2))
= λ. 0 3 (λ. 0 1 4)

Free variables

FV(x)     = {x}              -- variable
FV(λx.t)  = FV(t) - {x}      -- abstraction
FV(t₁ t₂) = FV(t₁) ∪ FV(t₂)  -- application

Fixpoint

Effectively just recursion.

fix =
λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

Strictness

• strict
• lazy

Redex

A term of the form (λx. t₁) t.

• Reducible expression.
• Term coined by Alonzo Church.
• β-reduction is the process of rewriting a redex as per evaluation rules.

Types of β-reduction

Full β-reduction

• Any redex can be reduced at any time.
• Each step picks a redex anywhere inside the term being evaluated and reduces it.

Normal order

• Left-most, outer-most redex is reduced first.

id(id(λz. id z))
----------------
 ↓

id(λz. id z)
------------
 ↓

λz. id z
    ----
 ↓
λz. z

Call by name

• Similar to normal order but no reductions inside abstractions. (names preserved??)
• A lazy strategy. Evaluation happens only if the term is actually used.
• Haskell uses call by need, an optimized form of call by name form of β-reduction.

id(id(λz. id z))
----------------
 ↓

id(λz. id z)
------------
 ↓

λz. id z

Call by value

• Only outermost redexes are reduced (TODO: what does that mean??)
• Redex is reduces only when its right side has been reduced to a value.
• A strict strategy. Evaluation happens anyway, even if it not needed and the term is not being used.
• Used by most languages.

id(id(λz. id z))
  --------------
 ↓

id(λz. id z)
------------
 ↓

λz. id z

DONE Full β reduction

Any redux can be reduced at any time.

Eg:

id (id (λz. id z))
    --------------

id (λz. id z)
        -----

id (λz. z)
----------

λz. z

Reduction stops.


Another possiblity:


id (id (λz. id z))
            ----  

id (id (λz. z))
---------------

id (λz. z)
----------

λz. z

Reduction stops.

Call by need

• Lazy. Arguments evaluated only when needed
• Used by Haskell (via rewrites)

DONE Call by name

• No reduction done inside an abstraction.
• Reduction stops if a lambda is encountered.
• Lazy. Arguments evaluated only when needed

Eg:

id (id (λz. id z))
------------------

id (λz. id z)
-------------

(λz. id z)

Reduction stops.
Even though the 'id z' inside the last abstraction could also be reduced.

DONE Call by value (??)

• Redex reduced only when the right operand is already in normal form (ie, a value)
• Only outermost redexes reduced.
• 'Functions are called only on values' ²
• Strict. Arguments always evaluated. Whether needed or not.
• Used by most languages

Eg:

id (id (λz. id z))
   ---------------

id (λz. id z)
-------------

(λz. id z)

Reduction stops.
Even though the 'id z' inside the last abstraction could also be reduced.

DONE Normal order

• leftmost, outermost redex is reduced first
• redexes inside abstractions also reduced

Eg:

id (id (λz. id z))
------------------

id (λz. id z)
-------------

λz. id z
    ----

(λz. z)

Reduction stops.

Examples

-- assumptions: types of available functions
nil : ∀X. List X
cons : ∀X. X -> List X
isnil : ∀X. List X -> Bool
head : ∀X. List X -> X
tail : ∀X. List X -> List X  (* everything except first element)

-- map function
λX. λY. λf:(X -> Y).
  (fix (λm: (List X) -> (List Y).  -- recursive function
    λl: List X.                    -- input list
      if isnil [X] l               -- from where did 'if' come from??
        then nil [Y]
      else
        cons [Y] (f (head [X] l))
    (m (tail [X] l))))

append: ∀X. (List X) -> (List X) -> (List X)
append =
λX. (fix (λm: (List X) -> (List X) -> (List X).
  λa: (List X). λb: (List X).
  if isnil [X] a
  then b
  else
    cons [X] (head [X] a) (m (tail [X] a) y)))

reverse: ∀X. (List X) -> (List X)
reverse = 
λX. (fix λm: (List X) -> (List X).
  λa: (List  X).
  if isnil [X] a
  then nil [X]
  else
    append [X] (m (tail [X] a)) (head [X] a))

Normalization

Evaluation of a well-typed term is guaranteed to halt in a finite number of steps. ie, every well-typed term is normalizable. (src: tapl)

• TODO: Strong normalization

Impredicativity

A definition (of a set/type etc) is impredicative if it involves a quantifier whose domain includes the very thing being defined. (src: tapl C23)

Monotypes

Type variables that range only over quantifier-free types. (src: tapl C23)

Polytype or Type scheme

Quantified types.

Subtypes

• aka second order lambda calculus (via an analogy with second-order intuitionalistic logic)
  • Quantification over types (analogous to predicates) possible.
  • In addition to quantification over terms
• A form of polymorphism (subtype polymorphism).
• Discovered in 1972 by Jean-Yves Girard
• A single term is given many types. (using rule of subsumption?)
• sml doesn't have subtyping.

Type preservation

• Meaning is not lost.
• t → t' means t reduces to t'

 Γ ⊢ t : T         t → t'
==========================
    Γ ⊢ t' : T

Progress

• Related to normalizability.
• For every term in the language:the term is either in normalized form (cannot be reduced further. Is already a value), or there is a typing rule (t → t') that takes it a step closer to normalized form.