Consider the model of computation defined as the restriction of the λcalculus to the set of linear terms. Linear terms are inductively defined as
follows:
– A variable is a linear term.
– If x occurs free in a linear term M, then λx.M is a linear term.
– If M and N are linear terms and the sets of free variables of M and N
are disjoint, then (M N) is a linear term.
In λx.M, the variable x is bound; terms are defined modulo α-equivalence
as usual.
a) Show that λx.λy.xy is a linear term according to the definition above,
and give an example of a non-linear term.
b) The computation rule in the linear λ-calculus is the standard βreduction rule. Indicate whether each of the following statements is
true or false and why.
i. In the linear λ-calculus, we can ignore α-equivalence when we apply
the β-reduction rule.
ii. If we β-reduce a linear term, we obtain another linear term.
iii. The linear λ-calculus is confluent.
iv. Every sequence of reductions in the linear λ-calculus is finite (in
other words, the linear λ-calculus is terminating).
v. The linear λ-calculus is a Turing-complete model of computation.