3 ms·
It's true that some constructions that work under normal/CBN order will go into an infinite loop under CBV order, but this is easy to work around, typically you
by vilhelm_s 7y ago
It's true that some constructions that work under normal/CBN order will go into an infinite loop under CBV order, but this is easy to work around, typically you just need to add an extra lambda to prevent it from evaluating too eagerly. For example, instead of translating
if b then e1 else e2
as
b e1 e2
you can translate it to
(b (λx. e1) (λx. e2)) tt
where tt is any value (it doesn't matter what).
Similarly, you can make a CBV-version of the Y combinator by eta-expanding some subexpressions to prevent it from evaluating it too eagerly [0].
The exact details of the encoding don't matter too much, because when you actually write programs you want to use some syntactic sugar like "if then else" or "let rec", so you just care that it can be translated into lambda calculus in some way which preserves the operational semantics.
[0] https://en.wikipedia.org/wiki/Fixed-point_combinator#Strict_fixed_point_combinator https://en.wikipedia.org/wiki/Fixed-point_combinator#Strict_...