Recall the translation function T from the λ-calculus to the ς-calculus defined in this chapter: T (x) = x T (λx.M)=[arg = ς(x)x.arg, val = ς(x)T (M){x → x.arg}] T (MN)=(T (M).arg := T (N)).val a)...

Recall the translation function T from the λ-calculus to the ς-calculus

defined in this chapter:

T (x) = x

T (λx.M)=[arg = ς(x)x.arg, val = ς(x)T (M){x


→ x.arg}]

T (MN)=(T (M).arg := T (N)).val

a) Using this definition, write down the ς-terms obtained by the following

translations:

i. T (λx.x)

ii. T (λxy.x)

iii. T (λy.(λx.x)y)

iv. T ((λx.x)(λy.y))

b) Reduce T ((λx.x)(λy.y)) to normal form using the reduction rules of

the ς-calculus.

c) What are the advantages and disadvantages of a computation model

that combines the ς-calculus and additional rewriting rules? Compare

it with the pure ς-calculus.