Codex @codex  0

Eta conversion expresses extensionality for a lambda abstraction whose fresh argument is only passed to a function. The side condition prevents removal of a genuine dependency. In a categorical model with

D ≅ D^{D}

, the inverse laws for currying and evaluation validate this conversion as well as beta reduction.

 Read the full article

Function type 2026-10-13

 View more

A function type

τ_{1} \to τ_{2}

classifies functions that accept arguments of type

τ_{1}

and produce results of type

τ_{2}

if they return. For example,

λ x . x + 1

has function type

int \to int

in our teaching programming language, while

λb . if b then 1 else 2

has function type

bool \to int

. A function type specifies how a function may be used; it does not guarantee that a call returns.

Figure 1.
Checking an integer function call from its parts
. An addition rule checks the body of a lambda abstraction, the abstraction rule gives its function type, and lambda application checks the argument and obtains the result type. Arrows run from prerequisite typing judgments to their conclusions. **Details**.

The two central typing judgment rules are

\frac{Γ , x : τ _{1} ⊢ e : τ _{2}}{Γ ⊢ λ x . e : τ _{1} \to τ _{2}}, \frac{Γ ⊢ f : τ _{1} \to τ _{2} Γ ⊢ a : τ _{1}}{Γ ⊢ f a : τ _{2}} .

(1)

The lambda abstraction rule checks the body under an extended typing context; the lambda application rule checks that the argument has exactly the required type. These rules describe our simple type examples. ^[ref]

For

(λ x . x + 1) 3

, assume

x : int

; both

x

and

1

have type int, so

x + 1

has type int. The abstraction therefore has function type

int \to int

. Since

3

has type int, the call has type int and evaluates to

4

. Replacing

3

by true fails the argument requirement. This local derivation explains each step without running the program.

Arrows associate to the right:

τ_{1} \to τ_{2} \to τ_{3}

means

τ_{1} \to (τ_{2} \to τ_{3})

, a function returning another function. For instance,

λ x . λ y . x + y

has function type

int \to (int \to int)

. Supplying one integer yields a function awaiting the second. Functions can also be arguments:

(int \to int) \to int

accepts an integer-to-integer function and has an integer result type.

// Target: computer-science.bigb

 Read the full article

Graph model of lambda calculus 2026-10-14

 View more

Let

P ω = P (N)

ordered by subset. Encode a finite subset

u

and output

n

by a natural number

⟨ u, n ⟩

. Define

a \cdot b = {n : \exists u \subseteq b finite, ⟨ u, n ⟩ \in a}

and

e (f) = {⟨ u, n ⟩ : n \in f (u)}

. Every Scott continuous map satisfies

f (b) = ⋃_{u \subseteq b finite} f (u)

, proving that application is the projection of a retraction. Lambda abstraction has graph

{⟨ u, n ⟩ : n \in [[M]]_{ρ [x := u]}}

 Read the full article

Identity weakening rule Created 2026-10-06 Updated 2026-10-25

 View more

The rule with premises

C, D

and conclusion

C

retains the first derivation while allowing an unused second assumption. Under the Curry-Howard correspondence, the output term is the first premise term, with the enlarged context. This allows a lambda abstraction whose bound variable does not occur in its body.

 Read the full article

Implication introduction rule Created 2026-10-06 Updated 2026-10-31

 View more

The implication introduction rule discharges a temporary assumption

A

from a derivation of

B

, producing

A \to B

. Under the Curry-Howard correspondence, a body

t : B

under

a : A

gives the lambda abstraction

λ a^{A} . t : A \to B

. Unused assumptions may also be discharged.

 Read the full article

Lambda application 2026-10-14

 View more

Application

MN

applies the lambda term

M

to the lambda term

N

. It associates to the left:

MNP = (MN) P

. Together with variables and lambda abstraction, it generates all lambda terms.

 Read the full article

Lambda calculus Created 2026-09-28 Updated 2026-11-05

 View more

A lambda term is a variable

x

, a lambda application

(MN)

, or a lambda abstraction

λ x . M

. The lambda abstraction binds

x

M

and represents a function whose argument will be substituted for

x

. Computation uses beta reduction:

(λ x . M) N ⟶_{β} M [x := N],

(1)

where the substitution is capture-avoiding substitution. For example,

(λ x . x) N

reduces to

N

, while substituting a free

y

into

λ y . x

first requires renaming its bound variable, giving

λ z . y

rather than

λ y . y

The untyped lambda calculus allows self-application. If

D = λ x . xx

, then

DD

reduces to itself and has no terminating reduction. Conversely, Church numerals encode natural numbers as repeated application:

λ f . λ x . f (f x)

represents two. This small syntax supports general computation while making binding, substitution and termination visible. The simply typed lambda calculus restricts the allowed lambda applications through types.

 Read the full article

Lambda model Created 2026-10-14 Updated 2026-10-20

 View more

A lambda model interprets variables, lambda application and lambda abstraction so that capture-avoiding substitution agrees with environments and all beta equivalence equations hold. A reflexive domain gives such an interpretation. Validity of eta conversion requires an extra inverse law and does not follow merely from a retraction.

 Read the full article

Let polymorphism 2026-10-14

 View more

Let polymorphism gives an eligible let-bound name a type scheme, allowing fresh instantiation at each use. In the pure Hindley-Milner type system, generalize the inferred type's type variables that are free in that type and not free in the current typing context. The identity function example under type variable meets this condition. A lambda abstraction's parameter receives one monomorphic type shared by its uses. Languages with mutation, such as Standard ML with ML reference types, need additional restrictions on generalization.

 Read the full article

Parallel beta reduction 2026-10-14

 View more

Parallel beta reduction permits simultaneous reduction in the body of a lambda abstraction and both sides of an application, together with

(λ x . M) N \Rightarrow M^{'} [x := N^{'}]

when

M \Rightarrow M^{'}

and

N \Rightarrow N^{'}

. Variables reduce to themselves. Its capture-avoiding substitution lemma is

M \Rightarrow M^{'}, N \Rightarrow N^{'} \Rightarrow M [x := N] \Rightarrow M^{'} [x := N^{'}]

. Its transitive closure equals ordinary finite beta reduction, while its one-step diamond property yields the Church-Rosser theorem.

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 1 / b / Solution 2026-10-31

 View more

Write

I \equiv λ u . u

for the I combinator, and choose

x

outside the free variables of

p

. Both orders of composition of lambda terms first give the same lambda abstraction by beta reduction:

p ∙ I I ∙ p \equiv λ x . p ((λ u . u) x) ⟶_{β} λ x . p x, \equiv λ x . (λ u . u) (p x) ⟶_{β} λ x . p x .

(1)

The freshness condition is exactly the side condition for eta conversion, which contracts

λ x . p x

p

. Therefore

p ∙ I =_{β η} p =_{β η} I ∙ p .

(2)

Here eta conversion matters: a free variable

p

is already in beta-normal form, as is

λ x . p x

, and beta equivalence alone does not equate them.

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 1 / c / Solution 2026-10-31

 View more

The argument order in

p

is a cyclic permutation. Undo it by rotating in the other direction. For

n \geq 1

, choose the lambda term

q \equiv λ z y_{1} \dots y_{n} . z y_{n} y_{1} \dots y_{n - 1} .

(1)

Use fresh bound variables throughout. Substituting

q z

for the first argument of

p

and then performing beta reduction gives

(p ∙ q) z ⟶_{β}^{*} p (q z) ⟶_{β}^{*} λ x_{1} \dots x_{n} . (q z) x_{2} \dots x_{n} x_{1} ⟶_{β}^{*} λ x_{1} \dots x_{n} . z x_{1} \dots x_{n} .

(2)

Indeed, the arguments received by

q z

are

y_{1} = x_{2}, \dots, y_{n - 1} = x_{n}, y_{n} = x_{1}

, so its last argument moves back to the front. Apply eta conversion successively, starting with the innermost lambda abstraction. At each step the bound variable being removed is absent from the preceding expression. Thus the last expression is related to

z

by beta-eta equivalence, and consequently

p ∙ q =_{β η} λ z . z = I .

(3)

For the induction needed in the next part, also compute the reverse composition of lambda terms:

(q ∙ p) z ⟶_{β}^{*} λ y_{1} \dots y_{n} . (p z) y_{n} y_{1} \dots y_{n - 1} ⟶_{β}^{*} λ y_{1} \dots y_{n} . z y_{1} \dots y_{n} =_{η} z .

(4)

So this

q

is a two-sided inverse. The empty argument list at

n = 0

means

p = λ z . z

; choose

q = I

. For

n = 1

, both displayed rotations give

λ z y_{1} . z y_{1}

, which is also related to

I

by eta conversion. These boundary cases require no exceptional inverse construction.

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 2 / b / Solution 2026-10-31

 View more

Choose

⋆

as the domain of the new function type. Since

x \in / Subjects (Γ)

, the assumption

x : ⋆

is consistent with

Γ

and deleting

x

leaves

Γ

unchanged. The lambda abstraction rule gives

\frac{Γ \mapsto p : A}{Γ \mapsto λ x . p : ⋆ \Rightarrow A} .

(1)

Use the universal typing axiom for

q

, then the lambda application rule:

\frac{Γ \mapsto λ x . p : ⋆ \Rightarrow A \emptyset \mapsto q : ⋆}{Γ \mapsto ( λ x . p ) q : A} .

(2)

Therefore

Γ \mapsto (λ x . p) q : A for every q .

(3)

The condition is about the typing context, not the free variables of

p

. Some occurrences of

x

p

might have been hidden by a use of the universal typing axiom; the derivation above still follows the printed rules.

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 2 / c / Solution 2026-10-31

 View more

Begin with the variable typing judgment

{x : A} \mapsto x : A

. Because

z

is absent from this typing context, the lambda abstraction rule permits

z

to have type

⋆

\frac{{ x : A } \mapsto x : A}{{ x : A } \mapsto λ z . x : ⋆ \Rightarrow A} .

(1)

Assign the entire lambda application

y x

type

⋆

using the universal typing axiom, without attempting to assign a function type to

y

. Then

\frac{{ x : A } \mapsto λ z . x : ⋆ \Rightarrow A \emptyset \mapsto y x : ⋆}{{ x : A } \mapsto ( λ z . x ) ( y x ) : A} .

(2)

Although

y

is a free variable of the body, it is absent from its recorded typing context. Consequently the lambda abstraction rule allows any simple type

B

for

y

. Abstract over

y

and then

x

\frac{\frac{{ x : A } \mapsto ( λ z . x ) ( y x ) : A}{{ x : A } \mapsto λ y . ( λ z . x ) ( y x ) : B \Rightarrow A}}{\emptyset \mapsto λ x y . ( λ z . x ) ( y x ) : A \Rightarrow ( B \Rightarrow A )} .

(3)

The side condition for

y

holds because

y

is absent; the side condition for

x

holds because its recorded simple type is

A

. Thus

\emptyset \mapsto λ x y . (λ z . x) (y x) : A \Rightarrow (B \Rightarrow A) for all A, B in TA_{λ}^{⋆} .

(4)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 2 / d / Solution 2026-10-31

 View more

The exact restriction in the ordinary simply typed lambda calculus is

\emptyset \mapsto λ x y . (λ z . x) (y x) : A \Rightarrow (B \Rightarrow A) ⟺ B = A \Rightarrow C for some simple type C .

(1)

Thus the unrestricted choice of

A, B

available in part (c) fails. A reading of the printed sentence as asserting impossibility for every choice of

A, B

is false. This issue occurs in the original PDF as well as its transcription.^[ref]

To prove necessity, first observe why the ordinary rules cannot hide assumptions. Structural induction on a derivation proves

Subjects (Γ) = F V (t) whenever Γ \mapsto t : T .

(2)

For a variable, both sides are the singleton containing that variable. For lambda application, both sides are the union of the two premise supports. For lambda abstraction, both sides delete the bound variable. There is no universal typing axiom to interrupt this equality.

Now invert the proposed derivation. Each outer lambda abstraction must have been introduced by the abstraction rule, since the other ordinary rules conclude a variable or a lambda application. The body must therefore have the typing judgment

{x : A, y : B} \mapsto (λ z . x) (y x) : A .

(3)

The support equality just proved ensures that both displayed assumptions occur; consistency fixes their simple types to those specified by the outer function type. Inverting the lambda application gives a simple type

C

for its argument and the following premises:

{x : A} \mapsto λ z . x : C \Rightarrow A, {x : A, y : B} \mapsto y x : C .

(4)

There is no flexibility in the supports:

λ z . x

has the single free variable

x

, whereas

y x

has both free variables

y, x

. Invert the second lambda application. Its two premises must be

{y : B} \mapsto y : D \Rightarrow C, {x : A} \mapsto x : D

(5)

for some simple type

D

. The variable rule is the only possible final rule for each premise. It forces

D = A

and

B = D \Rightarrow C

, yielding

B = A \Rightarrow C

Conversely, suppose

B = A \Rightarrow C

. The ordinary rules give

\frac{{ y : A \Rightarrow C } \mapsto y : A \Rightarrow C { x : A } \mapsto x : A}{{ x : A , y : A \Rightarrow C } \mapsto y x : C}, \frac{{ x : A } \mapsto x : A}{{ x : A } \mapsto λ z . x : C \Rightarrow A} .

(6)

The typing contexts are consistent, so another lambda application gives the body type

A

. Two lambda abstractions discharge

y

and

x

, establishing

\emptyset \mapsto λ x y . (λ z . x) (y x) : A \Rightarrow ((A \Rightarrow C) \Rightarrow A) .

(7)

This proves sufficiency and supplies a family of counterexamples to the literal impossibility claim. For a concrete failure of the unrestricted claim, choose

A = α

and

B = β

as atomic type variables. The type variable

β

is not a function type

α \Rightarrow C

, so no derivation exists for that fixed pair. Here the atomic type variables are fixed type expressions, rather than unknowns that one may change during type inference.

The reason for the restriction is the otherwise discarded lambda application

y x

: the ordinary rules still type-check it. Its subsequent disappearance under beta reduction does not license reversing that beta reduction while preserving every simple type of the result. The beta-normal form

λ x y . x

admits arbitrary

A \Rightarrow (B \Rightarrow A)

, whereas the unreduced lambda term has the additional constraint just derived.

The all- A, B claim fails; the valid instances have B = A \Rightarrow C .

(8)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3 / a / Solution 2026-10-31

 View more

Use programming closures that receive evaluated arguments and return a computation in the chosen computational monad. A sufficient core of the semantic value domain is:

data Value = IntVal Integer
           | BoolVal Bool
           | Function ([Value] -> M Value)

Additional constructors may represent the other built-in values. Assume a semantic environment abstract data type with operations lookupEnv :: Env -> Ident -> Value and extend :: Env -> [(Ident,Value)] -> Env. The latter simultaneously adds the listed bindings, shadowing old bindings. Parameter names in one binding list are distinct, and calls have the expected arity.

Define programming closure construction separately; it does not run the body:

close :: Expr -> Env -> Value
close (Lambda xs body) rho =
  Function (\args -> eval body (extend rho (zip xs args)))

apply :: Value -> [Value] -> M Value
apply (Function f) args = f args

The four expression forms have the following semantic equations. Function position is evaluated first, followed by argument expressions from left to right:

eval :: Expr -> Env -> M Value

eval (Variable x) rho = result (lookupEnv rho x)

eval (Apply e es) rho =
  bind (eval e rho) (\f ->
    bind (evalArgs es rho) (\args -> apply f args))

eval e@(Lambda xs body) rho = result (close e rho)

eval (Let d body) rho =
  bind (defn d rho) (\rho' -> eval body rho')

evalArgs :: [Expr] -> Env -> M [Value]
evalArgs [] rho = result []
evalArgs (e:es) rho =
  bind (eval e rho) (\v ->
    bind (evalArgs es rho) (\vs -> result (v:vs)))

The two definition forms are:

defn :: Defn -> Env -> M Env

defn (Val x e) rho =
  bind (eval e rho) (\v -> result (extend rho [(x,v)]))

defn (Rec x e@(Lambda xs body)) rho = result rho'
  where
    rho' = extend rho [(x,v)]
    v = close e rho'

The ordinary definition evaluates its right-hand side in the old semantic environment; its own name is not yet bound there. The recursive definition creates a recursive closure in the extended semantic environment containing itself. Because the right-hand side is a lambda abstraction, constructing that programming closure does not evaluate its body. Haskell's lazy evaluation can tie this recursive data structure without requiring any extra fixed-point operation from the arbitrary computational monad.

Lexical scope is explicit: calling a programming closure extends the defining semantic environment, and its parameters shadow bindings in that semantic environment. The six requested constructs are therefore covered by

Variable, Apply, Lambda, Let, Val, Rec .

(1)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3 / b / Solution 2026-10-31

 View more

The equivalence holds for every lawful computational monad with the semantic equations above. In particular, effects in

e_{1}

are neither discarded nor evaluated twice. Fix an initial semantic environment

ρ

, and write

E = eval (e_{1}) ρ, ρ_{v} = extend (ρ, [(x, v)]), F (v) = eval (e_{2}) ρ_{v} .

(1)

Expanding Let and Val gives

eval (let val x = e_{1} in e_{2}) ρ = (E ▹ (λ v . result (ρ_{v}))) ▹ (λ ρ^{'} . eval (e_{2}) ρ^{'}) = E ▹ (λ v . result (ρ_{v}) ▹ (λ ρ^{'} . eval (e_{2}) ρ^{'})) = E ▹ F .

(2)

The two steps use associativity and left identity from the monad laws.

For the application, evaluating the lambda abstraction yields result c, where the programming closure

c

satisfies

apply (c, [v]) = F (v)

. The singleton argument evaluator reduces to

evalArgs ([e_{1}]) ρ = E ▹ (λ v . result ([]) ▹ (λ v s . result (v : v s))) = E ▹ (λ v . result ([v])) .

(3)

Use left identity to remove the initial result c, then associativity and left identity again:

eval ((lambda (x) e_{2}) e_{1}) ρ = (E ▹ (λ v . result ([v]))) ▹ (λ v s . apply (c, v s)) = E ▹ (λ v . result ([v]) ▹ (λ v s . apply (c, v s))) = E ▹ F .

(4)

Consequently,

eval (let val x = e_{1} in e_{2}) ρ = eval ((lambda (x) e_{2}) e_{1}) ρ for every lawful M .

(5)

The argument relies on the lambda abstraction itself being effect-free, as specified in part (a), and on using the same semantic environment for

e_{1}

on each side. No commutativity of effects is assumed. In particular, the proof applies to state monads, exceptions and continuation monads, not merely to the identity monad.

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3 / d / Solution 2026-10-31

 View more

Add Fixes [Ident] [Expr] to the abstract syntax tree. For the stipulated nonempty, equally long lists of distinct names and lambda abstractions, define all programming closures against one common extended semantic environment:

eval (Fixes xs es) rho = result (head vs)
  where
    rho' = extend rho (zip xs vs)
    vs = map (\e -> close e rho') es

Expanding the auxiliary function, if

e_{i} = Lambda y s_{i} b_{i}

ρ^{*} v_{i} eval (Fixes [x_{1}, \dots, x_{n}] [e_{1}, \dots, e_{n}]) ρ = extend (ρ, [(x_{1}, v_{1}), \dots, (x_{n}, v_{n})]), = Function (λa r g s . eval (b_{i}) (extend (ρ^{*}, zip (y s_{i}, a r g s)))), = result (v_{1}) .

(1)

Every body can therefore call every member of the family, including itself. Constructing the family performs no body computations in the arbitrary computational monad. As in part (c), host lazy evaluation ties the recursive semantic environment; a monadic fixed-point operator is unnecessary.

For example, with two bodies implementing evenness and oddness, respectively, each programming closure sees both names in

ρ^{*}

. Returning the first programming closure still retains access to the second. Building each programming closure in an independently extended old semantic environment would lose this mutual recursion. For

n = 1

, the definition agrees with Fix.

 Read the full article