Functional Programming

Question 1

Untyped lambda-calculus

Answer 1

N ::= x | λx.N | NN

Question 2

Variable capture

Answer 2

When a term with free variable x is substituted inside λx.N, by which the variable x becomes bound.

Question 3

Simple type syntax

Answer 3

τ ::= o | τ → τ

Question 4

Outermost reduction

Answer 4

• Given a redex (λx.N)M, reduces the redex before any reductions in N and M
• Guarantees to reach normal form but duplicates work as much as possible

Question 5

Innermost reduction

Answer 5

• Given a redex (λx.N)M, reduces the redex after any reductions in N and M
• Does not duplicate work but does not necessarily reach normal form

Question 6

Zip

Answer 6

zip :: [a] -> [b] -> [(a,b)]
zip _ [] = []
zip [] _ = []
zip (x:xs) (y:ys) = (x,y) : zip xs ys

Question 7

Weakly normalising term

Answer 7

• A term that has reduction to normal form
• For example, (λy.x)((λx.xx)(λx.xx))

Question 8

Strongly normalising term

Answer 8

• A term that is weakly normalising and has no infinite reduction sequence
• For example, (λy.x)(λx.xx)

Question 9

Example term that is neither weakly nor strongly normalizing

Answer 9

(λx.xx)(λx.xx)

Question 10

Fixed-point combinator

Answer 10

• A fixed-point combinator is a λ-term F that satisfies M =β F M for any M, where β is beta-equivalence
• For example: λf.(λx.f(xx))(λx.f(xx))

Question 11

Fixed-point combinator proof

Answer 11

For any lambda-term M, Y M = β M(Y M)

Y M
→ (λx.M(xx))(λx.M(xx))
→ M((λx.M(xx))(λx.M(xx)))
← M(Y M)

Question 12

Capture-avoiding substitution

Answer 12

M[y/x] = M with x renamed to y

Question 13

Examples of capture-avoiding substitution

Answer 13

1) Example: (λx.xy)[λz.z/y]
This means change y to λz.z
Therefore = λx.x(λz.z)

2) Example: (λx.xy)[λz.zx/y]
Therefore = λw.w(λz.zx)
The x changes to w to avoid capturing the free x in λz.zx

3) Example: (f(λx.yx)yx)[fy/x]
Therefore = f(λx.yx)y(fy)
The bound x in λx.yx is not substituted

4) Example: (λf.f(λx.yx)yx)[fy/x]
Therefore = λg.g(λx.yx)y(fy)
The bound f is renamed to g avoiding capturing the free f

Question 14

Church-Rosser Property

Answer 14

• M =β N if and only if there is a term P s.t. M → ∗β P and N → ∗β P
• This proves that a lambda term can’t have more than one normal form

Question 15

Confluence

Answer 15

Whenever M →∗ N1 and M →∗ N2, there is some P such that N1 →∗ P and N2 →∗ P

Question 16

Local Confluence

Answer 16

Whenever M → N1 and M → N2, there is some P such that N1 →∗ P and N2 →∗ P

Question 17

Free and bound variables

Answer 17

If the first occurrence of a variable appears when defining a lambda, then it is bound to that lambda.

For example, in λx.x, variable x is bound as it first occurs in λx

Otherwise, it is a free variable. For example, in (λx.x)(λy.yx):
- the variable x in λx.x is bound to
the first lambda
- the variable y in λy.yx is bound to
the second lambda
- the variable x in λy.yx is free

Example 3 - (λx.xy)(λy.y):

• the variable y in λx.xy is free
• the variable y in λy.y is bound to the second lambda

Question 18

Lazy evaluation

Answer 18

• A reduction strategy that uses graphs to ensure a term is evaluated at most once, if its result is needed for the overall computation, and otherwise not evaluated at all.
• When a redex (λx.M)N is reduced, instead of substituting N for every free variable x in M, each variable x functions as a pointer to N.
• Then N is evaluated at most once, and when its output is needed after that, the stored result is used
• It always reaches normal form if one exists, and is efficient since it doesn’t evaluate terms more than once

Question 19

Fixed point in the λ-calculus

Answer 19

• A λ-term M such that M = βF M
• Every term in the lambda calculus has a fixed point

Question 20

Simply typed lambda-calculus

Answer 20

M ::= x | λx^τ.M | MM

Question 21

Typing rules

Answer 21

Question 22

Referential transparency

Answer 22

• Means that the output of a function depends only on its inputs and not on other, less visible factors
• A function that always returns the same values given the same inputs
• Lazy evaluation needs referential transparency otherwise the evaluation steps do not preserve the meaning of a program

Question 23

Computational effects

Answer 23

• May give different outputs on different occasions, even with the same input
• They destroy referential transparency

Question 24

Functions that use computational effects

Answer 24

• Example 1: mutable state
• This interferes with referential transparency because the stored values in the state may have changed
• Example 2: random values
• This interferes with referential transparency because the random number generator may produce different numbers each time
• Example 3: user inputs
• This interferes with referential transparency because a user may give different input on
  each occasion

Question 25

List comprehension syntax

Answer 25

function xs = [check x | x <- xs, condition]

Question 26

Recursion syntax

Answer 26

function [] = 0
function (x:xs)
| condition x = change x + function xs
| otherwise = function xs

Question 27

Redex

Answer 27

An application in which the left-hand side is an abstraction

Question 28

Beta reduction

Answer 28

• (λx.N)M → N[M/x]
• Capture-avoiding substitution rules apply (renames bound variables)

Question 29

Alpha conversion

Answer 29

• Renaming of variables
• This fixes beta-reduction, to avoid variable capture

Question 30

Alpha-equivalence

Answer 30

Two terms differ only in the names of their bound variables

Question 31

Beta equivalence

Answer 31

The reflexive-transitive-symmetric closure of →β

Question 32

Lambda terms for booleans

Answer 32

true: λx.λy.x
false: λx.λy.y
ifthen: λb.λx.λy.bxy
and: λb1.λb2.ifthen b1 b2 false
or: λb1.λb2.ifthen b1 true b2

add: F = λa.λm.λn.ifthen (iszero n) m (succ (a m (pred n)))
add as a fixed point = YF

succ: +1 = λn.λf.λx.f(n f x)
pred: -1 = λm.λn.λf .λx.m f (n f x)

Question 33

Lambda terms for Church numerals

Answer 33

add: λm.λn.λf .λx.m f (n f x)
mul: λm.λn.λf .λx.m (n f) x

The numerals themselves:

0: λf.λx.x
1: λf.λx.fx
2: λf.λx.f(fx)
3: λf.λx.f(f(fx))

Question 34

Zero-testing

Answer 34

• Applying λx.false any non-zero number of times to any argument gives false
• Applying it zero times to true gives true
• Lambda term: λn.n (λx.false) true

Question 35

Properties of the typed lambda-calculus

Answer 35

Uniqueness of types:
For any context Γ and term M , there is at most one type τ such that Γ |- M : τ

Substitution preserves types:
If Γ , x : τ |- M : σ and Γ |- N : τ then Γ |- M[N/x] : σ

Reduction preserves types:
If Γ , x : τ |- M : σ and Γ |- N : τ then Γ |- M[N/x] : σ

Question 36

Trees

Answer 36

Defined as data Tree a = Leaf | Node a (Tree a) (Tree a)

• Tree a on LHS = initial definition
• Tree a on RHS = recursive call with child of node
• a = type, can represent anything
• Leaf = constructor to define an empty tree
• Node takes three arguments: the data to store at the node, and the two children of it

Question 37

Encoding rules for addition

Answer 37

• If it’s a recursive function, then it is weakly normalising as it can reach a normal form but it is also possible to unfold the fixpoint forever
• If it’s not recursive then it is strongly normalising and thus also weakly normalising
• If add is encoded using the Y combinator, it is neither because the fixed point can never be discarded