1
$\begingroup$

What is an example of a typed lambda term $\lambda x.\phi : A \to B$ and a term $a : A$ such that, when $\beta$-reducing the term $(\lambda x.\phi)(a)$, the argument $a$ must be repeated/recomputed several times?

$\endgroup$
3
$\begingroup$

In the simply typed $\lambda$-calculus with pairs, a simple example is

$$(\lambda x :T. (x,x))a$$

where $a$ is a term of type $T$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.