Is there a valid application where variables are not distinct and occur free in operand

33 Views Asked by At

Consider

$$ (\lambda V_1..V_n. E)E_1..E_n $$

Is there a case where application of this form is valid if not all $V_i$ are distinct and some $V_i$ occur free in $E_i$?

Here's an example where it is not valid.

$$ (\lambda xx. \underline{sum} \ xx)(\lambda z.x)(\underline{3}) = (\lambda x. \underline{sum} \ (\lambda z.x) \ x) \ \underline{3} $$

Free variable $x$ in $(\lambda z.x)$ becomes bound in $\underline{sum}$ so this is invalid.

Now I can't find a case where it is valid? Can you give me an example where it is?

Thanks a bunch!

1

There are 1 best solutions below

0
On

@Spukgespenst from #math libera mentioned

$$ (\lambda xx.x)xx $$

is valid. Thanks!