[dwohnitmok]

For (b) isn't this the appeal of normal-order evaluation (or its related sibling lazy evaluation)? If there is a terminating reduction sequence lazy evaluation will find it, whereas eager evaluation will fail to find it.

Moreover the lambda calculus is confluent, so if you find the terminating reduction sequence, you're guaranteed all other terminating sequences end up with the same result.

So as long as your PL uses normal-form evaluation or lazy evaluation you can entirely realize any equivalences in the lambda calculus.