Overview

• Introduction to Go (basics)
• Higher-order functions
• Lambda calculus (a bit of theory)

Hello World

package main

import "fmt"

var x int

func hi(y int) {
        fmt.Printf("hi %d\n",y)
}

func main() {
    x= 1
    hi(x)
    fmt.Printf("hello, world\n")
}

• Type declarations in ‘proper’ order
  • var varName varType
  • Variable varName of Type varType

Printf similar to printf in C, see here for brief description of the C printf variant.

Go Toolchain

• Command line:

  • go run hello.go

  • gofmt hello.go

    • “pretty printer”
    • Per Default to standard I/O
    • Or by overwriting content gofmt -w hello.go

  • Choose your editor (emacs, …)

• Check your favorite IDE for a Go plugin.

In most cases, our programs consist of a single file.

Simple form of type inference

package main

import "fmt"

func main() {
    var x int
    x = 1
    y := x + 1
    fmt.Printf("y = %d", y)

}

The type of y is inferred by the right-hand side.

Pretty convenient!

Languages like Haskell support full type inference where the types of functions can be inferred.

Control structures - for loop

The only control structure.

    for i := 0; i < 5; i++ {
        fmt.Printf("Value of i is now: %d \n", i)
    }

Infinite loop with break

    for {
        if j > 5 {
            break
        }
        fmt.Printf("Value of j is now: %d \n", j)
        j++

    }

Complete example

package main

import "fmt"

func main() {

    for i := 0; i < 5; i++ {
        fmt.Printf("Value of i is now: %d \n", i)
    }

    j := 0
    for {
        if j > 5 {
            break
        }
        fmt.Printf("Value of j is now: %d \n", j)
        j++

    }

}

Strings

Unlike in C, Go strings are not null terminated. In Go, strings are represented by a struct consisting of

1. The length of the string.

2. A pointer to the first byte.

These implementation details are hidden from the user. The user can make use of array notation to access a specific position in the string. There is a primitive len that computes the length of a string. Strings are immutable. This means they cannot be updated (but copied of course).

Next, we discuss a few examples that involve strings.

Printing a string.

    var x string = "Hello"
    y := "Hi"

    fmt.Println(x)
    fmt.Printf("%s \n", y)

Several ways to iterate over a string.

    for i := 0; i < len(x); i++ {
        fmt.Printf("%c", x[i])

    }

    for i, e := range x {
        fmt.Printf("%c", e)
        fmt.Printf("%c", x[i])

    }

// Don't care notation _
    for i, _ := range x {
        fmt.Printf("%c", x[i])

    }

    for _, e := range x {
        fmt.Printf("%c", e)

    }

Via range we obtain current position and element. The notation _ indicates that we don’t care about the value.

Arrays

Out of bounds check.

    var s1 [3]string
    s1[0] = "one"
    s1[1] = "two"
    s1[2] = "three"
    // s1[3] = "four"

Short-hand array initialization

    s2 := [3]string{"one", "two", "three"}

Iteration

    for index, elem := range s1 {
        fmt.Printf("%d %s \n", index, elem)
    }

Complete example

package main

import "fmt"

func main() {

    var s1 [3]string
    s1[0] = "one"
    s1[1] = "two"
    s1[2] = "three"

    for index, elem := range s1 {
        fmt.Printf("%d %s \n", index, elem)
    }

    s2 := [3]string{"one", "two", "three"}

    fmt.Printf("%s", s2[0])
}

Slices

More flexible arrays (length may change)

    s1 := make([]string, 3)

Short-hand

    s2 := []string{"a", "b"}

Functions on slices, e.g. append

    s2 := []string{"a", "b"}
    s3 := append(s2, "c", "d", "e")

Complete example

package main

import "fmt"

func printSlice(s []string) {
    for _, elem := range s {
        fmt.Printf("%s \n", elem)
    }

}

func main() {

    s1 := make([]string, 3)

    s1[0] = "one"
    s1[1] = "two"
    s1[2] = "three"

    printSlice(s1)

    s2 := []string{"a", "b"}

    s3 := append(s2, "c", "d", "e")

    printSlice(s3)
}

Call-by-value

Go uses call-by-value for paramter passing.

Call-by-reference can be emulated via pointers. Go supports pointers (but does not support pointer arithemtic).

Slices are internally represented via pointers.

Example

package main

import "fmt"

func inc(i int) int { return i + 1 }

func mapInc(xs []int) []int {
    for i, e := range xs {
        xs[i] = inc(e)
    }

    return xs
}

func mapInc2(xs []int) {
    for i, e := range xs {
        xs[i] = inc(e)
    }

}

func main() {

    xs := []int{1, 2, 3}
    ys := mapInc(xs)
    fmt.Printf("%d %d\n", xs[0], ys[0])
    mapInc2(ys)
    fmt.Printf("%d \n", xs[0])
}

Yields

2 2
3

Functions - Return values

• Return types in ‘proper’ order

func inc(i int) int

• Multiple return values

func myDiv2(x int, y int) (int, bool)

• Complete example

package main

import "fmt"

func inc(i int) int { return i + 1 }

// Direct reference to return values by name
// Only applies to tuple return values
func myDiv(x int, y int) (res int, status bool) {
    status = false
    if y == 0 {
        return
    }
    res = x / y
    status = true
    return
}

func myDiv2(x int, y int) (int, bool) {
    if y == 0 {
        return 0, false
    }
    return x / y, true
}

func main() {
    var res int
    var status bool
    res, status = myDiv(inc(3), 2)
    fmt.Printf("Result = %d \n", res)
    fmt.Printf("Status = %t \n", status)

    res, status = myDiv2(1, 0)
    fmt.Printf("Result = %d \n", res)
    fmt.Printf("Status = %t \n", status)
}

Strings again

We write a function to split a string into a prefix and a suffix once we see given byte.

func splitAt(x string, b byte) (string, string) {
    var r1, r2 []byte
    suffix := false

    for i, _ := range x {
        if !suffix {
            if x[i] == b {
                suffix = true
            } else {
                r1 = append(r1, x[i])
            }

        } else {
            r2 = append(r2, x[i])
        }
    }

    s1 := (string)(r1)
    s2 := (string)(r2)

    return s1, s2

}

We use slices r1 and r2 to collect the prefix and suffix. We check if we have seen the given element b yet, and then append elements in the original string to either r1 or 2. The element b is not added.

We require slices as append only operates on slices. As we wish to retrieve the result as strings, we need to include a type conversion.

Function splitAt returns two results, the prefix and the suffix. Multiple return results can be retrieved as follows.

    r1, r2 := splitAt("hel:lo", ':')

    fmt.Printf("%s %s", r1, r2)

Higher-order functions

Simple (increment) function.

func inc(i int) int { return i + 1 }

Functions can be arguments.

func apply(i int, f func(int) int) int {
    return f(i)
    }

func mapInt(f func(int) int, xs []int) []int {
    ys := make([]int, len(xs))
    for i, e := range xs {
        ys[i] = f(e)
    }

    return ys
}

func execute(f func()) {
    f()
}

Point to note:

• func apply ... declares that we define a function with name apply

• f func(int) int declares that parameter f is of function type

• func(int) int is a function type where the input is an int and the output is an int as well

Functions can be return values.

func hello()  {
    fmt.Print("Hello \n")
}

func hello2(x int) func() {
    fmt.Printf("%d ", x)
    return hello
}

Complete example

package main

import "fmt"

func inc(i int) int { return i + 1 }

func square(i int) int { return i * i }

func apply(i int, f func(int) int) int {
    return f(i)
}

func execute(f func()) {
    f()
}

func hello() {
    fmt.Print("Hello \n")
}

func hello2(x int) func() {
    fmt.Printf("%d ", x)
    return hello
}

// Create a new slice.
func mapInt(f func(int) int, xs []int) []int {
    ys := make([]int, len(xs))
    for i, e := range xs {
        ys[i] = f(e)
    }

    return ys
}

// In-place update. Result refers to xs.
func mapIntWithSideEffect(f func(int) int, xs []int) []int {
    for i, e := range xs {
        xs[i] = f(e)
    }

    return xs
}




func main() {
    execute(hello)

    execute(hello2(2))

    fmt.Printf("%d \n", apply(1, inc))

    xs := []int{1, 2, 3}
    ys := mapInt(inc, xs)
    zs := mapInt(square, xs)

    fmt.Printf("%d %d %d \n", xs[1], ys[1], zs[1])

}

Anonymous functions (lambdas)

Anonymous functions are function without a name. They originate from the lambda calculus and therefore we refer to anonymous functions also as lambda funtions.

Function definitions so far.

func inc(i int) int { return i + 1 }

Go supports anonymous functions (lambdas).

func (i int) int { return i + 1 }

Almost same syntax as for function definitions. We simply drop the function name.

How can we use lambda functions?

Instead of

ys := mapInt(inc, xs)

we can also write

ys := mapInt(func(i int) int { return i + 1 }, xs)

Advantage:

• Define and use a lambda function “in place”

• Lambda functions can be defined anywhere and may refer to local variables

Consider

func hello3(x int) func() {
    return func () { fmt.Printf("Hello %d \n", x) }
}

• func() result is a parameter-less function with not result value

• func () { fmt.Printf("Hello %d \n", x) } lambda function where we refer to the local variable x

Complete example

package main

import "fmt"

func apply(i int, f func(int) int) int {
    return f(i)
}

func execute(f func()) {
    f()
}

func hello() {
    fmt.Print("Hello \n")
}

func hello2(x int) func() {
    fmt.Printf("%d ", x)
    return hello
}

// Create a new slice.
func mapInt(f func(int) int, xs []int) []int {
    ys := make([]int, len(xs))
    for i, e := range xs {
        ys[i] = f(e)
    }

    return ys
}

func main() {
    execute(hello)

    execute(hello2(2))

    fmt.Printf("%d \n", apply(1, func(i int) int { return i + 1 }))

    xs := []int{1, 2, 3}
    ys := mapInt(func(i int) int { return i + 1 }, xs)
    zs := mapInt(func(i int) int { return i * i }, xs)

    fmt.Printf("%d %d %d \n", xs[1], ys[1], zs[1])

}

Partial function application, function types and function calls

Recall

func add(x int) func(int) int {
    return func(y int) int { return x + y }
}

Consider

    var f func(int) (func(int) int)

    f = add
    inc := f(1)
    fmt.Printf("%d", inc(3))

• f(1) yields a function of type func(int) int

• This function is effectively the increment function

Consider

    x := (f(2))(3)
    fmt.Printf("%d", x)

• The call (f(2))(3) calculates 2 + 3

• First we call f(2)

• This yields function of type func(int) int

Hence, we call this function with parameter 2

f(2) is an example of a partial function application (because we obtain another function as the result).

To avoid clutter, the convention adopted in Go (and other languages that support higher-order functions) is to allow removal of parentheses by assuming that

• function application is left-associative

• function types are right-associative

Compare

    var f func(int) (func(int) int)

    f = add
    x := (f(2))(3)

versus

    var f func(int) func(int) int


    f = add
    x := f(2)(3)

Both are the same!

func(int) func(int) int     =    func(int) (func(int) int)

    because function types are right-associative


f(2)(3)   =   (f(2))(3)

    because function application is left-associative

Complete example

package main

import "fmt"

func add(x int) func(int) int {
    return func(y int) int { return x + y }
}

func main() {
    var f func(int) (func(int) int)

    f = add
    inc := f(1)
    fmt.Printf("\n %d", inc(3))

    x := (f(2))(3)
    fmt.Printf("\n %d", x)

    var g func(int) func(int) int

    g = add
    y := g(2)(3)

    fmt.Printf("\n %d", y)
}

Currying versus uncurrying

Consider

func plus(x int, y int) int {
    return x+y
}

The arguments to plus must be both present.

In Go, it’s possible to ‘incrementally’ supply addition with its arguments.

func add(x int) func(int) int {
    return func(y int) int { return x + y }
}

Function add expects an integer argument (left operand) and yields a function. This function expects another integer argument (right operand) and then yields the expected result.

How to transform one function into the other? See below curry and uncurry functions.

“Curried style”

• Arguments can be supplied incrementally

• Allows for a more flexible use of functions

“Uncurried style”

• All arguments must be present

• Generally less run-time overhead

Complete example

package main

import "fmt"

func plus(x int, y int) int {
    return x + y
}

func add(x int) func(int) int {
    return func(y int) int {
        return x + y
    }
}

func curry(f func(int, int) int) func(int) func(int) int {
    return func(x int) func(int) int {
        return func(y int) int {
            return f(x, y)
        }
    }

}

func uncurry(g func(int) func(int) int) func(int, int) int {
    return func(x int, y int) int {
        return (g(x))(y)
    }
}

func main() {

    x1 := plus(1, 2)
    x2 := (add(1))(2)
    p := uncurry(add)
    x3 := p(1, 2)
    p2 := curry(plus)
    x4 := (p2(1))(2)

    fmt.Printf("%d %d %d %d", x1, x2, x3, x4)

}

Function closures

What’s the output of the following program?

package main

import "fmt"

type Type0 func()

func main() {
    var fn Type0
    var x int = 2

    fn = func() { fmt.Printf("%d \n", x) }

    fn()

    x = 3
    fn()
}

For each call to fn there is a different result!

Unlike pure functional programming languages, the Go language is impure. Pure means that for each function call and the same input arguments, we obtain the same output. This is also referred to as referential transparency.

Type definitions and structs (named types)

Type definitions

type myint int

Introduces a new type named myint. Values of type int and myint cannot be mixed.

The type myint is structurally isomorphic to int, so we can (type) convert one into the other.

Here is the complete example.

package main

import "fmt"

type myint int

func main() {
    var i int
    var j myint

    j = 1

    i = (int)(j)
    // i = j
        // yields a type error

    j = (myint)(i)

    fmt.Printf("%d", i)
}

Structs

type rectangle struct {
    length int
    width  int
}

Defines a named type rectangle that is structurally isomorphic to a struct of two ints where both ints can be accessed via field labels.

Construction of values.

    var r1 rectangle = rectangle{1, 2}
    var r2 rectangle = rectangle{width: 2, length: 1}
    r3 := rectangle{width: 2, length: 1}

Either by position or by field reference.

Intermediate Summary

• Control structures

• Arrays, slices

• Functions

  • Higher-order (functions can be anywhere)
  • Anonymous functions (“lambdas”)
  • Multiple return values

func add(x int) func(int) int {
    return func(y int) int { return x + y }
}

// func add ...            Function declaration, I'm a function with name add
// func(int) int           Function type, from int to int
// func(y int) int { ...}  Anonymous function, lambda binder and body

Function application is left-associative.

(add(1))(2)   versus    add(1)(2)

Functions types are right-associative.

func(int) (func(int) int)    versus     f func(int) func(int) int

Connection to OO. In Go functions are first-class (that is, they can appear anywhere). This is similar to OO where objects are first-class.

For example, in an OO language, we can call a method m1 on some object o1. The result is an object on which we call another method m2.

o1.m1().m2()

• Structs
  • OO style programming

Some (simple) exercises

Play with the examples provided.

any, map, filter, …

Implement the following functions. Sample solutions below.

// Yields the first element which satisfies the predicate.
// Otherwise, we return a dummy element.
// The first component of the resulting tuple indicates
// if any element has satisfied the predicate.
func any(p func(int) bool,xs []int) (bool,int)


// Map f over a list of integer values which then yields
// a list of booleans
func map(f func(int) bool,xs []int) []bool


// Filter out all elements which satisfy the predicate.
func filter(p func(int) bool,xs []int) []int

Sample solution

package main

import "fmt"

// Yields the first element which satisfies the predicate.
// Otherwise, we return a dummy element.
// The first component of the resulting tuple indicates
// if any element has satisfied the predicate.
func any(p func(int) bool, xs []int) (bool, int) {
    for _, x := range xs {
        if p(x) {
            return true, x
        }
    }
    return false, -1
}

// Map f over a list of integer values which then yields
// a list of booleans
// 'map' predefined so use mapMy
func mapMy(f func(int) bool, xs []int) []bool {
    var ys []bool

    for _, x := range xs {
        ys = append(ys, f(x))

    }
    return ys
}

// Filter out all elements which satisfy the predicate.
func filter(p func(int) bool, xs []int) []int {
    var ys []int

    for _, x := range xs {
        if p(x) {
            ys = append(ys, x)
        }
    }
    return ys
}

func main() {
    b, x := any(func(x int) bool { return x > 1 }, []int{0, 1, 2, 3})

    fmt.Printf("%b %d \n", b, x)

    xs := filter(func(x int) bool { return x > 1 }, []int{0, 1, 2, 3})

    for _, x := range xs {
        fmt.Printf("%d \n", x)
    }

}

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!

Lambda calculus: Syntax and semantics

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

$$t \ \ ::= \ \ x \ \ \mid \ \ \lambda x.t \ \ \mid \ \ t \ t$$

where

• $x$ refers to a variable
• $\lambda x.t$ to a lambda abstraction
• $t \ t$ refers to a function application

The above EBNF is ambiguous. For example, consider expression $\lambda 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 $\lambda x.x$ applied to $x$.

The first interpretation can be explained via the following (parse tree) derivation $$t \rightarrow \lambda x.t \rightarrow \lambda x. t \ t \rightarrow \lambda x. x \ t \rightarrow \lambda x.x \ x$$

whereas for the second derivation we find $$t \rightarrow t \ t \rightarrow (\lambda x. t) \ t \rightarrow (\lambda x.x) \ t \rightarrow (\lambda 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 $(\lambda x.x) \ x$.

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

$$(\lambda x. t_1) \ t_2 \rightarrow [t_2/x]t_1$$

In $[t_2/x]t_1$, we apply the substitution $[t_2/x]$: In the body $t_1$, replace each occurrence of the formal parameter $x$ by the argument $t_2$.

Commonly, we refer to $\lambda x.e$ as a lambda-abstraction and to $\lambda x$ as the lambda-binding.

For example, $(\lambda x. (\lambda y. y)) \ z$ reduces to $\lambda y.y$.

As it is common in programming languages, we can reuse the same variable names and apply the common rule that each use of a variable name refers to the closest binding site. For example, consider $\lambda x. (\lambda x. x)$ where the innermost occurrence of $x$ refers to the inner lambda-binding.

Via some simply renaming we can always guarantee that variables are distinct. For example, $\lambda x. (\lambda x. x)$ can be renamed to $\lambda x. (\lambda y. y)$.

We generally assume that lambda-bindings always introduce fresh, distinct variables.

Details

Syntactic sugar

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

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

Free variables

$fv(t)$ computes all free variables in $t$, i.e. those variables which are not bound by a lambda abstraction.

The definition by induction over the structure of $t$ is as follows:

• $fv(x) = \{ x \}$
• $fv(\lambda x.t) = fv(t) - \{ x \}$
• $fv(t_1 \ t_2) = fv(t_1) \cup fv(t_2)$

In case of name clashes we must rename bound variables. Consider $[y \ (\lambda x.x)/x] \lambda y.(\lambda x.x) \ y \ x$:

1. Renaming yields: $[y \ (\lambda v.v)/x] \lambda z. (\lambda u.u) \ z \ x$
2. Substitution without name clashes yields: $\lambda z. (\lambda u.u) \ z(y \ (\lambda v.v))$

Substitution

Examples (where $e$ refers to a term/expression)

• $[ e_1/x ] x = e_1$
• $[ e_1/x ] y = y$ if $y$ != $x$
• $[ e_1 / x ] e_2 \ e_3 = ([ e_1 /x ] e_2) \ ([ e_1 /x ] e_3)$
• $[ e_1 / x ] \lambda y.e_2 = \lambda y. [ e_1 /x ] e_2$ if $y$ != $x$ and $y\not\in fv(e_1)$

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.

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

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

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

Under AOR, we can reduce f(1+2) to f(3) and inc(1+1) 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.

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)
}

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 $(\lambda f.\lambda x. f \ (f \ x)) ((\lambda x.x) (\lambda x.x))$ where $\rightarrow$ denotes an evaluation step.

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)

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

$\rightarrow \lambda x.(\lambda x.x)(\lambda x.x)(((\lambda x.x)(\lambda x.x)) x)$

$\rightarrow \lambda x.(\lambda x.x)(((\lambda x.x)(\lambda x.x)) x)$

$\rightarrow \lambda x.(\lambda x.x)((\lambda x.x)x)$

$\rightarrow \lambda x.(\lambda x.x)x$

$\rightarrow \lambda x.x$

Call-by-value (CBV):

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

$\rightarrow (\lambda f.\lambda x. f \ (f \ x)) (\lambda x.x)$

$\rightarrow \lambda x.(\lambda x.x) ((\lambda x.x) x)$

$\rightarrow \lambda x.(\lambda x.x)x$

$\rightarrow \lambda x.x$

(Non)Termination

There are lambda terms whose evaluation will not terminate:

$(\lambda x. (x \ x)) (\lambda x. (x \ x))$

$\rightarrow (\lambda x. (x \ x)) (\lambda x. (x \ x))$

$\rightarrow (\lambda x. (x \ x)) (\lambda x. (x \ x))$

$\rightarrow ...$

Termination under CBN is more likely than termination under CBV.

Let’s abbreviate $(\lambda x. (x \ x)) (\lambda x. (x \ x))$ by $\Omega$. Then, the lambda term $(\lambda x. \lambda y. x) \Omega$ terminates under CBN but not under CBV.

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:

$(\lambda x. x + x) \ (1 + 3)$

$\rightarrow (\lambda x. x + x) \ 4$

$\rightarrow 4 + 4$

$\rightarrow 8$

CBN:

$(\lambda x. x + x) \ (1 + 3)$

$\rightarrow (1+3) + (1+3)$

$\rightarrow 4 + (1+3)$

$\rightarrow 4 + 4$

$\rightarrow 8$

call-by-need:

$(\lambda x. x + x) \ (1 + 3)$

$\rightarrow (1+3) + (1+3)$

$\rightarrow 4 + 4$

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.

$\rightarrow 8$

Further examples

Consider $(\lambda x. x \ y) \ (\lambda x. x) \ (\lambda x. x)$.

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

Let’s carry out the evaluation steps.

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

$=_{Renaming} \ \ ((\lambda x_1. x_1 \ y) \ (\lambda x_2. x_2)) \ (\lambda x_3. x_3)$

$\rightarrow \ \ ( (\lambda x_2. x_2) \ y) (\lambda x_3. x_3)$ because $(\lambda x_1. x_1 \ y) \ (\lambda x_2. x_2) \ \rightarrow \ [(\lambda x_2. x_2) / x_1 ] (x_1 \ y) \ = \ (\lambda x_2. x_2) \ y$

$\rightarrow \ \ y \ (\lambda x_3. x_3)$ because $(\lambda x_2. x_2) \ y \ \rightarrow \ [y / x_2] x_2 \ = \ y$

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

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

$-_{Renaming} \ (\lambda x_1. x_1 \ y) \ ((\lambda x_2. x_2) \ (\lambda x_3. x_3))$

$\rightarrow \ (\lambda x_1. x_1 \ y) \ (\lambda x_3. x_3)$

$\rightarrow \ (\lambda x_3. x_3) \ y$

$\rightarrow \ y$

Expressiveness/Church Encoding

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.