Programming Language Theory Concept

Curry/Y-Combinator

Books

Journey Statusreviewing Tags

fix = λ f . (λ x . f (x x)) (λ x . f (x x))

Details
fix g→[f↦g](λx. f (x x)) (λx. f (x x))→(λx. g (x x)) (λx. g (x x))→[x→λx. g (x x)]g (x x)→g ((λx. g (x x)) (λx. g (x x)))=g (fix g)
- In a Call by value evaluation strategy, this diverges because it continues to evaluate $fix g$ .
- In a Call by name evaluation strategy, $fix g$ does not diverge because $g$ gets applied to $fix g$ .