Lambda calculus

The lambda calculus represents a minimal core language just consisting of functions.

Functions are first-class (can appear as arguments and as return values). Think of first-class objects!

• Syntax

• Free and bound variables

• Renaming and substitution

• Evaluation via beta-reduction

• Evaluation strategies

• Expressiveness/Church Encoding

• Some Haskell implementations

Syntax

Terms (expressions/programs) in the lambda calculus are defined by the following (abstract) EBNF syntax.

 t ::= x | \x -> t | t t

where

• x refers to a variable
• \x -> t to a lambda abstraction (\x -> to a lambda binding)
• t t refers to a function application

The above EBNF is ambiguous. For example, consider expression \x -> x x. Based on the above EBNF rules there are two possible interpretations.

1. A lambda function with formal parameter x where x is applied to itself in the function body.

2. The identity function \x -> x applied to x.

The first interpretation can be explained via the following (parse tree) derivation

    t
--> \x -> t
--> \x -> t t
--> \x -> x t
--> \x -> x x

where we write --> to denote derivation steps applying one of the above grammar rules.

The second interpretation results from the following derivation

    t
--> t t
--> (\x -> t) t
--> (\x -> x) t
--> (\x -> x) x

In the above derivation, parentheses "(..)" are meta-symbols to highlight the difference among the two derivations.

In examples, we therefore may make use of parentheses to avoid ambiguities, for example (\x -> x) x.

Syntactic sugar

Function application is left associative. Hence, the term (\u -> u) z x is a short-hand for (((\u -> u) z) x).

The body of a lambda abstractions extends to the right as long as possible. Hence, the term \z -> (\u -> u) z x is a short-hand for \z -> (((\u -> u) z) x).

Lambdas in Haskell

We use here the lambda notation as found in Haskell. In the literature, you'll find also the more math-style notation using greek letters.

In terms of the semantics, here is an important difference between Haskell and the lambda calculus.

Haskell is a (implicitly) typed language whereas we consider here the untyped lambda calculus.

Free and bound variables

fv(t) computes all free variables in t, i.e. those variables which are not bound by a lambda abstraction. Any variable introduced via a lambda abstraction is a bound variable.

We can compute free variables by induction over the structure of t is as follows:

(FV1) fv(x) = { x }

(FV2) fv(\x -> t) = fv(t) - { x }

(FV3) fv(t1 t2) = fv(t1) cup fv(t2)

where we write cup to denote set union and - to denote set difference.

The computation of bound variables follows a similar structure.

(BV1) bv(x) = { }

(BV2) bv(\x -> t) = bv(t) cup { x }

(BV3) bv(t1 t2) = bv(t1) cup bv(t2)

Examples

Consider t = \x -> x y. Then, we find that fv(t) = { y }.

In more detail:

   fv(\x -> x y)

=  fv(x y) - { x }                   application of (FV2)

= (fv(x) cup fv(y)) - { x }          application of (FV3)

= ({ x } cup { y }) - { x }          application of (FV1)

= { y }

Consider t = (\x -> x) (\x -> x). Then, we find that bv(t) = { x }.

In more detail:

   bv((\x -> x) (\x -> x))

=  bv(\x -> x) cup bv(\x -> x)                   application of (BV3)

= (bv(x) cup { x }) cup (bv(x) cup { x })        application of (BV2)

= ({ } cup { x }) cup ({ } cup { x })            application of (BV1)

= { x }

Renaming and substitution

Consider t= \x -> x y where fv(t) = { y } and bv(t) = { x }.

Free variables such as y are not bound by any lambda abstraction. Hence, we wish to substitute (replace) free variables by arbitrary lambda terms. However, we must be careful to avoid name clashes.

Consider the above example. Substituting y by another free variable z yields the lambda term \x -> x z. What if we substitute y by x? This results in a name clash!

From the point of view of the substitution (replacing y by x), y and x are free variables. But x is also a bound variable. If we would simply carry out the substitution (replacing y by x), we end up with \x -> x x.

This looks wrong! The lambda term be put in place (here x) of a free variable (here y) should never refer to any bound variables. The solution is to rename bound variables before substitution. Renaming of bound variables applied to our example yields \x2 -> x2 y.

We generally assume that lambda-bindings always introduce fresh, distinct variables. By fresh, distinct we mean that variables don't appear anywhere else. This property can be guaranteed by renaming. We only show renaming here by example. This form of renaming is referred to as alpha-conversion.

Substitution can then be carried out mechanically. Very similar to the computation of free/bound variable, we apply a substitution by observing the structure of the lambda term on which the substitution is to be applied.

We write [t1/x] to denote a substitution where we wish to replace all occurrences of x by t1.

We write [t1/x] t2 to denote the result of applying substitution [t1/x] on t2.

[t1/x] t2 is computed as follows.

(S1) [ t1/x ] x = t1

(S2) [ t1/x ] y = y if y != x

(S3) [ t1/x ] t2 t3 = ([ t1 /x ] t2) ([ t1 /x ] t3)

(S4) [ t1/x ] \y -> t2 = \y -> [ t1/x ] t2 if y != x and y not an element in fv(t_1).

The side condition in (S4) is not necessary assuming lambda-bindings always fresh, distinct variables.

Examples

Consider t = \x -> x y and the substitution [(\z -> x z) / y].

We first rename bound variables in t and obtain t' = \x2. x2 y.

We apply the substitution on t' as follows.

   [(\z -> x z) / y] \x2 -> x2 y

=  \x2 -> [(\z -> x z) / y] (x2 y)                        application of (S4)

=  \x2 -> ([(\z -> x z) / y] x2) ([(\z -> x z) / y] y)    application of (S3)

=  \x2 -> x2 ([(\z -> x z) / y] y)                        application of (S2)

=  \x2 -> x2 (\z -> x z))                                 application of (S1)

Dynamic semantics

The operational semantics of the lambda calculus is defined via a single rule, commonly referred to as $\beta$-reduction.

 (\x -> t1) t2 --> [t2/x] t1

where --> denotes that the left-hand side term evaluates to the right-hand side term.

Evaluation turns all lambda-abstractions that appear in function position into a substitution where in the lambda body t1 we replace all occurrences of x by t2.

Examples

Consider t = (\x -> (\x -> x) x) y. We first apply renaming to ensure that each lambda binding introduces a fresh, distinct variable. After renaming, we find t' = (\x1 -> (\x2 -> x2) x1) y.

We exhaustively apply beta-reduction.

    (\x1 -> (\x2 -> x2) x1) y

--> [y / x1] (\x2 -> x2) x1

=   (\x2 -> x2) ~ y

--> [y / x2] x2

=   y

Evaluation strategies

There are two principles ways how to evaluate terms:

• Innermost first
• Outermost first

Innermost

• Look for a redex innermost, leftmost
• Also called Applicative Order Reduction (AOR)
• Redex = reducible expression of the form (\x-> ...) e

Call-by value (CBV) = AOR with the exception that we don't evaluate under "lambda" (i.e. inside function bodies)

Difference between CBV and AOR illustrated via an example. Instead of the plain lambda calculus we make use of Go/Haskell.

// Go version
func inc(x int) int { return x+1 }

func f(x int) int {
    return inc(1+1) + x
}

func main() {
   f(1+2)
}

// Haskell version
inc :: Int -> Int
inc x = x + 1

f :: Int -> Int
f x = inc(1+1) + x

main = f (1+2)

Under AOR, we cannot reduce f(1+2) to f(3) because there's the innermost inc(1+1) that reduces to inc(2).

Under CBV, we can only reduce f(1+2) to f(3) because inc(1+1) is inside a function body.

Hence, evaluation under CBV proceeds as follows.

      f(1+2)
 -->  f(3)
 -->  inc(1+1) + 3
 -->  inc(2) + 3
 -->  3 + 3
 -->  6

In comparison, evaluation under AOR.

      f(1+2)
=    (\lambda x. inc(1+1) + x) (1+2)
                     ^^^
               innermost redex
 -->  (\lambda x. inc(2) + x) (1+2)
 -->  (\lambda x. inc(2) + x) 3
 --> inc(2) + 3
 ...
 -->  6

The motivation for CBV is to avoid evaluation of arguments unless they are needed to make progress during evaluation.

Consider the following variant.

// Go version
func inc(x int) int { return x+1 }

func f(x int) int {
    if x == 3 {
         return 0
    }
    return inc(1+1) + x
}

func main() {
   f(1+2)
}

// Haskell version
inc :: Int -> Int
inc x = x + 1

f :: Int -> Int
f x
  | x == 3    = 0
  | otherwise = inc(1+1) + x

main = f (1+2)

For this case and the call f(1+2) reducing inc(1+1) to inc(2) is unnecessary (and therefore wasteful) as we don't reach this program text during evaluation.

Outermost

Outermost, leftmost, also called Normal Order Reduction (NOR)

Call-by name (CBN) = NOR with the exception that we don't evaluate under "lambda" (i.e. inside function bodies)

Examples

We consider evaluation of (\f -> \x -> f (f x)) ((\x -> x) (\x -> x)).

We omit the alpha-renaming step (we should actually rename bound variables but keeping the bound variables as they are is harmless for this example).

Call-by-name (CBN) versus Normal Order Reduction (NOR):

    (\f -> \x -> f (f x)) ((\x -> x) (\x -> x))

--> \x -> (\x -> x) (\x -> x) (((\x -> x) (\x -> x)) x)

Under CBN we are done as we do not evaluate under a lambda. NOR will proceed as follows.

--> \x -> (\x -> x) (((\x -> x) (\x -> x)) x)

--> \x -> (\x -> x) ((\x -> x) x)

--> \x -> (\x -> x) x

--> \x -> x

Call-by-value (CBV) versus Applicative Order Reduction (AOR):

    (\f -> \x -> f (f x)) ((\x -> x) (\x -> x))

--> (\f -> \x -> f (f x)) (\x -> x)

--> \x -> (\x -> x) ((\x -> x) x)

Under CBV we are done as we do not evaluate under a lambda. AOR will proceed as follows.

--> \x -> (\x -> x)x

--> \x -> x

(Non)Termination

There are lambda terms whose evaluation will not terminate:

    (\x -> (x x)) (\x -> (x x))

--> (\x -> (x x)) (\x -> (x x))

--> (\x -> (x x)) (\x -> (x x))

--> ...

The above evaluation steps apply to CBN and CBV.

Observation: Termination under CBN is more likely than termination under CBV.

This is a general result (for proofs please check the lambda-calculus literature).

We give an example that terminates under CBN but does not terminate under CBV. Let's abbreviate (\x -> (x x)) (\x -> (x x)) by Omega. Then, the lambda term (\x -> \y -> y) Omega terminates under CBN but not under CBV.

Consider the CBN evaluation steps.

    (\x -> \y -> y) Omega

--> \y -> y

and we are done. Notice that x does not appear in the lambda body \y -> y.

Consider the CBV evaluation steps.

    (\x -> \y -> y) Omega

--> (\x -> \y -> y) Omega

and so on.

Recall that evaluation of Omega does not terminate.

Short summary

• CBN may require fewer execution step but seems rather inefficient to implement (in a compiler)
• But has plenty of applications
  • More code reuse
  • More declarative code
  • Many useful cases of "non-terminating" structures, e.g. infinite, circular data structures, callbacks, ...
• CBN usually (more efficiently) implemented via a call-by-need scheme.

CBV:

    (\x -> x + x) (1 + 3)

--> (\x -> x + x) 4

--> 4 + 4

--> 8

CBN:

   (\x -> x + x) (1 + 3)

--> (1 + 3) + (1 + 3)

--> 4 + (1 + 3)

--> 4 + 4

--> 8

The difference to CBN is that once we evaluate 1+3 and obtain the result 4, we immediately replace all other occurrences of 1+3 by 4 without actually evaluating these other occurrences.

Further examples

Consider (\x -> x y) (\x -> x) (\x -> x).

Function application is left-associative, therefore, the meaning of the above lambda term is ((\x -> x y) (\x -> x)) (\x -> x).

Let's carry out the evaluation steps.

           ((\x -> x y) (\x -> x)) (\x -> x)

=_Renaming ((\x1 -> x1 y) (\x2 -> x2)) (\x3 -> x3)

-->        ( (\x2 -> x2) y) (\x3 -> x_3)

      because

      (\x1 -> x1 y) (\x2 -> x2) --> [(\x2 -> x2) / x1 ] (x1 y) = (\x2 -> x2) y

-->        y (\x3 -> x3)

      because

      (\x2 -> x2) y --> [y / x2] x2 = y

On the other hand, the lambda term (\x -> x y) ((\x -> x) (\x -> x)) evaluates to y. Briefly, the evaluation steps are

           (\x -> x y) ((\x -> x) (\x -> x))

=_Renaming (\x1 -> x1 y) ((\x2 -> x2) (\x3 -> x3))

-->        (\x1 -> x1 y) (\x3 -> x_3)

-->        (\x3 -> x3) y

-->        y

Expressiveness/Church Encoding

In the below, we use the math-style notation for lambda terms. There might be some viewing problems on Chrome. If this is the case, please use Firefox.

How expressive is the lambda calculus? As expressive as a Turing machine?

Yes! But how? The lambda calculus looks rather simple. There are no numbers, booleans, no conditional, looping constructs.

Indeed, but as we will show next, we can encode data types (booleans, ...), conditional expressions, recursion.

The idea of the Church encoding (named after Alonzo Church):

• Encode behavior not structure

Boolean operations

The idea:

• not x = if x then false else true

• x or y = if x then true else y

• x and y = if x then y else false

The actual encoding:

• true = $\lambda x. \lambda y.x$

• false = $\lambda x. \lambda y. y$

• if $e_1$ then $e_2$ else $e_3$ = $e_1 \ e_2 \ e_3$

which written in 'lambda notation' is

ite = $\lambda e_1. \lambda e_2. \lambda e_3. e_1 \ e_2 \ e_3$

Example: if true then $e_2$ else $e_3$ equals $(\lambda x. \lambda y. x) \ e_2 \ e_3$

$(\lambda x. \lambda y. x) \ e_2 \ e_3$

$\rightarrow e_2$

In detail:

$(\lambda x. \lambda y. x) \ e_2 \ e_3$

= $((\lambda x. \lambda y. x) \ e_2) \ e_3$

by adding parentheses (recall that function application is left associative)

$\rightarrow (\lambda y.e_2) \ e_3$

$\rightarrow e_2$

Boolean operations example

We evaluate $ite \ true \ x \ y$. The expect result is $x$. Let's see!

1. Replace short-hands by actual definitions.

$ite \ true \ x \ y = (\lambda x. \lambda y. \lambda z. x \ y \ z) \ (\lambda x. \lambda y. x) \ x \ y$

2. Rename variables such that all bound variables are distinct

$(\lambda x_1. \lambda y_1. \lambda z_1. x_1 \ y_1 \ z_1) \ (\lambda x_2. \lambda y_2. x_2) \ x \ y$

3. Introduce parentheses

$(((\lambda x_1. \lambda y_1. \lambda z_1. (x_1 \ y_1) \ z_1) \ (\lambda x_2. \lambda y_2. x_2)) \ x) \ y$

4. Carry out evaluation steps

$(((\lambda x_1. \lambda y_1. \lambda z_1. (x_1 \ y_1) \ z_1) \ (\lambda x_2. \lambda y_2. x_2)) \ x) \ y$

$\rightarrow (([(\lambda x_2. \lambda y_2. x_2) / x_1] (\lambda y_1. \lambda z_1. (x_1 \ y_1) \ z_1)) \ x) \ y$

$= (((\lambda y_1. \lambda z_1. ((\lambda x_2. \lambda y_2. x_2) \ y_1) \ z_1)) \ x) \ y$

Several redexes. We choose the outermost redex

$\rightarrow ([x / y_1] (\lambda z_1. ((\lambda x_2. \lambda y_2. x_2) \ y_1) \ z_1)) \ y$

$= (\lambda z_1. ((\lambda x_2. \lambda y_2. x_2) \ x) \ z_1) \ y$

$\rightarrow [y / z_1] (((\lambda x_2. \lambda y_2. x_2) \ x) \ z_1)$

$= ((\lambda x_2. \lambda y_2. x_2) \ x) \ y$

$\rightarrow ([x / x_2] (\lambda y_2. x_2)) \ y$

$= (\lambda y_2. x) \ y$

$\rightarrow [y / y_2] x$

$= x$

Numerals

The idea.

$0 = \lambda f. \lambda x.x$

$1 = \lambda f. \lambda x. f \ x$

$2 = \lambda f. \lambda x. f \ (f \ x)$

...

The successor function.

$succ = \lambda n. \lambda f. \lambda x. f \ (n \ f \ x)$

The addition function.

$add = \lambda m. \lambda n. \lambda f. \lambda x. m \ f \ (n \ f \ x)$

Recursion

What about recursion?

     factorial n = if n == 0 then 1
                   else n * (factorial (n-1))

Idea:

• Fixpointcombinator
  • $Y = \lambda F.(\lambda y.F \ (y \ y)) \ (\lambda x.F \ (x \ x))$
  • We find that $Y \ F = F \ (Y F)$

• $Fac = \lambda fac. \lambda n. if \ (n==0) \ \ then \ 1 \ else \ n*(fac \ (n-1))$

• $factorial = Y \ Fac$

This works!

$factorial \ 1$

$\rightarrow (def) \ (Y \ Fac) \ 1$

$\rightarrow (fix) \ (Fac \ (Y \ Fac)) \ 1$

$\rightarrow (def) \ ((\lambda fac. \lambda n. if \ (n == 0) \ then \ 1 \ else \ n*(fac (n-1)))) (Y Fac)) \ 1$

$\rightarrow \ (\lambda n. if \ (n==0) \ then \ 1 \ else \ n*((Y \ Fac) \ (n-1))) \ 1$

$\rightarrow \ 1 * ((Y \ Fac) \ 0)$

$\rightarrow (fix) \ 1 * ((Fac \ (Y \ Fac)) \ 0)$

$\rightarrow \ 1 * ((\lambda n. if \ (n == 0) \ then \ 1 \ else \ n*((Y \ Fac) \ (n-1))) \ 0)$

$\rightarrow \ 1 * 1$

$\rightarrow \ 1$

More encodings (pairs, natural numbers) are possible. See Church encoding.

Haskell stuff

Church Encoding

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}   -- required due to instances I1 and I2

-- Church encoding of Booleans.

true = \x -> \y -> x
false = \x -> \y -> y
ifThenElse x y z = x y z
notC x = ifThenElse x false true
andC x y = ifThenElse x y false
orC x y = ifThenElse x true y


-- We use here higher-order abstract syntax (HOAS).
-- How to display/show the syntax such as Haskell functions?
-- We can play a trick by overloading the show function.
instance Show (t->t1->t) where                                   -- I1
   show _ = "true"

instance Show (t->t1->t1) where                                  -- I2
   show _ = "false"

-- Examples
ex = ifThenElse true true false
ex2 = ifThenElse ex (andC false ex) false
ex2a = ifThenElse false true false


-- Church encoding of pairs.

mkPair x y = \b -> b x y
fstP p = p true
sndP p = p false


ex3 = fstP (mkPair ex ex2)

-- Church encoding of lists.
nullL = mkPair true true                        -- first element
                                               -- indicates list is empty
isNull = fstP
consL = \h -> \t -> mkPair false (mkPair h t)  -- non-empty list
                                               -- as a pair of (head,tail)
headL = \z -> fstP (sndP z)                    -- head = first element of
                                               --        the second pair
tailL = \z -> sndP (sndP z)                    -- tail = second element of
                                               --        the second pair

ex4 = consL true (consL false nullL)

ex5 = headL ex4

-- Church encoding of natural numbers.
-- n represented as n compositions of function f.

zeroN = \f -> \x -> x
succN = \n -> \f -> \x -> f (n f x)

plusN = \m -> \n -> \f -> \x -> m f (n f x)

isZeroN = \n -> n (\x -> false) true

Aside.

The above employs higher-order abstract syntax (HOAS). In the below we employ first-order abstract syntax (FOAS).

• Abstract because don't consider here a concrete source language but some abstraction where we ignore the common syntactic sugar present in a programming language.

• First-oder means that we use plain values to represent terms, e.g. numbers to represent variables etc.

• Higher-order means that we use Haskell variables to represent lambda term variables, Haskell functions to represent lambda functions etc. For more details see exercises.

Lambda calculus interpreter

-- Lambda calculus interpreter

-- Concepts used:
-- Recursive definitions
-- Structural recursion, i.e. pattern matching over the structure of some arguments
-- Guarded function clauses
-- Capturing side effects via monads


import Control.Monad.State

-- The syntax of lambda terms expressed as a data type declaration
data Term = Var String
          | App Term Term
          | Abs String Term

-- Overloading the show function, notice the recursive calls
instance Show Term where
   show (Var v) = v
   show (App t1 t2) = "(" ++ show t1 ++ " " ++ show t2 ++ ")"
   show (Abs v t) = "(" ++ "\92" ++ v ++ "." ++ show t ++ ")"



-- Difference among lists.
-- Concepts:
-- (1) Recursive definition over the structure of the first argument
-- (2) Guarded clauses
without [] ys = []
without (x:xs) ys
  | elem x ys = without xs ys
  | otherwise = x : without xs ys


-- Free variables of a term.
-- Concepts:
-- Recursive definition over the structure of the Term data type
fv :: Term -> [String]
fv (Var v) = [v]
fv (App t1 t2) = fv t1 ++ fv t2
fv (Abs v t) = fv t `without` [v]


-- Substitution of a variable (string) var by a term.
-- Note: We shall only substitute *free* variables.
substitute :: (String,Term) -> Term -> Term
substitute (var,term) (Var v)
   | var == v  = term
   | otherwise = Var v
substitute (var,term) (Abs v t)
   | var == v  = Abs v t
   | otherwise = Abs v (substitute (var,term) t)
substitute (var,term) (App t1 t2) =
   App (substitute (var,term) t1) (substitute (var,term) t2)

-- What remains is to reduce lambda terms wrt the reduction rule:
--   (\ x -> t1) t2 --> [t2/x] t1
-- That is, in the lambda body t1 we replace the lambda variable x
-- by the argument t2.
--
-- Be careful during substitution, name clashes are possible.
-- Recall the example [y (\x.x)/x] \y.(\x.x) y x
-- Our approach:
-- Before substitution, rename the body of the lambda abstraction,
-- only the apply the substitution.
-- Applied to our running example, we find:
-- Renaming yields  [y (\x.x)/x] \z.(\u.u) z x
-- Substitution yields \z.(\u.u) z (y (\x.x))

-- Renaming:
-- Requires some name supply (we need to create a 'fresh name' for a variable).


-- First attempt

renameT ::  Integer -> Term -> (Integer, Term)
renameT n (t@(Var v)) = (n, t)
renameT n (App t1 t2) =
       let (n1', t1') = renameT n t1
           (n2', t2') = renameT n1' t2
       in (n2', App t1' t2')
renameT n (Abs v t) =
       let v' = v ++ show n
           in (n+1, Abs v' (substitute (v, Var v') t))


-- Reflection:
-- renameT explicitly threads through some integer value.
-- Each time we require a fresh variable name,
--  (1) we append the integer value, and
--  (2) increment the value for future renamings
--
-- This looks rather clumsy (because of the 'extra' integer argument).
-- In some imperative/OO language, we could hide the integer argument
-- by employing some side effecting function, e.g.
-- int fresh() {
--    static n = 0;
--    n++;
--    return n;
-- }
--
-- In fact, we can do something similar in Haskell by employing monads.
-- Roughly, monads capture arbitrary computations. In our case, we
-- require a *state monad* where the current state equals the current integer value.


type RenameState = Integer

fresh = do i <- get
           put (i+1)
           return i

rename :: Term -> State RenameState Term
rename (t@(Var v)) = return t
rename (App t1 t2) = do
       t1' <- rename t1
       t2' <- rename t2
       return (App t1' t2')
rename (Abs v t) = do
       n <- fresh
       let v' = v ++ show n
       return (Abs v' (substitute (v, Var v') t))


reduce :: Term -> State RenameState Term
reduce (t@(Var v)) = return t
reduce (App t1 t2) = do
       t1' <- reduce t1
       t1'' <- rename t1'
       t2' <- reduce t2
       case t1'' of
         (Abs v t) -> return (substitute (v,t2') t)
         _         -> return (App t1'' t2')
reduce (t'@(Abs v t)) = return t'


run :: Term -> Term
run t = let (t',_) = runState (reduce t) 1
        in t'

-- examples

var v = Var v
app t1 t2 = App t1 t2
lam v t = Abs v t


-- (\x.(x y))
ex1 = lam "x" (app (var "x") (var "y"))


-- ((\x.(x y)) (\x.(x y)))
ex2 = app ex1 ex1

Notes from class

Winter semester 20/21

Reference to online tests

-- Lambda calculus question

{-

 What's the meaning of


   3 + 7 * 4

(1) 3 + (7 * 4)

   or

(2)  (3 + 7) * 4

It's (1) because we assume that * binds tighter than +!


-}


-- hla7

{-

   \x -> (\y -> y) (\y -> y) x


    Evaluate the above using the Applicative Order Reduction (AOR) strategy.

    A: \x -> (\y -> y) (\y -> y) x
    B: \x -> x
    C: \x -> (\y -> y) x


The answer is B. Here's why.

First, we apply some de-sugaring.

(R1) Function application is left associative.

(R2) The body of a lambda abstractions extends to the right as long as possible.


       \x -> (\y -> y) (\y -> y) x

=>R2   \x -> ((\y -> y) (\y -> y) x)

=>R1   \x -> (((\y -> y) (\y -> y)) x)


   \x -> (((\y -> y) (\y -> y)) x)


Next, we evaluate the above.


Let's look at some of the beta-reduction steps


     \x -> (((\y -> y) (\y -> y)) x)
             ^^^^^^^^  ^^^^^^^^^
               renaming to ensure that lambda-bound variables are distinct (apply alpha-conversion)

=>alpha

      \x -> (((\y1 -> y1) (\y2 -> y2)) x)
              ^^^^^^^^^^  ^^^^^^^^^^^
               function     argument
               (\x -> t1)    (t2)

                [(\y2 -> y2)/y1] y1 = (\y2 -> y2)

=>beta

      \x -> ((\y2 -> y2)    x      )
             ^^^^^^^^^^     ^^^^^^^^
               function     argument
               (\x -> t1)    (t2)

                [x / y2] y2  = x

=>beta

     \x -> x



Point to note.

AOR evaluates under a "lambda".
We've applied AOR for the above example.

CBV does not evaluate under a "lamba".

So, we would leave the term

   \x -> (((\y -> y) (\y -> y)) x)

as it is!



-}

CBN versus NOR evaluation

Consider again the CBN/NOR evaluation of $(\lambda f.\lambda x. f \ (f \ x)) ((\lambda x.x) (\lambda x.x))$

Here's the term using Haskell ascii notation (easier to type).

NOR = pick the outermost redex.
CBN = NOR but do not evaluate under a lambda.

I will underline the argument and the lambda abstraction

            (\ f -> \x -> f (f x)) ((\x -> x) (\x -> x))
              ^^^                       ^^^^^^^^^^^^^

Step 1
->CBN+NOR        Replace f by   (\x -> x) (\x -> x).
                   The second f, from the left, is replaced by ((\x -> x) (\x -> x)),

                  We obtain

                   \x -> (\x -> x) (\x -> x) (((\x -> x) (\x -> x)) x)

                    Recall that function application is left-associative.
                    Hence, the above reads as follows

                    \x -> ( (\x -> x) (\x -> x) ) (((\x -> x) (\x -> x)) x)
                            ^^                          ^^

                   I highlight the parentheses I added.
                   Let's get ride of these parentheses again and consider the next CBN evaluation step.

                   \x -> (\x -> x) (\x -> x) (((\x -> x) (\x -> x)) x)
                              ^^        ^^^^^^^

              Recall that I'm highlighting the outermost redex.

          Under CBN we are done. All reductions take place under a lambda.
          We continue with NOR

Step 2
->NOR       Replace x by (\x -> x).
                   We should actually rename lambda bound variables names to make them distinct,
                   but we're a bit lazy here (as we won't run into name clashes for this example).

                  We obtain

                  \x -> (\x -> x) (((\x -> x) (\x -> x)) x)
                            ^^         ^^^^^^^^^^^^^^^^^

Step 3
-> NOR          We obtain

                         \x -> ((\x -> x) (\x -> x)) x
                                     ^^        ^^^^^^^

Step 4
-> NOR            We obtain

                         \x -> (\x -> x) x
                                  ^^^       ^^^

Step 5
-> NOR            We obtain

                        \x -> x

and we are done.