Z-combinator

Formula: $\lambda f.(\lambda x.f(\lambda v.xxv))(\lambda x.f(\lambda v.xxv))$

• Details

  $$\begin{array}{cc}\text{fix}g& \to [f\mapsto g](\lambda x.f(\lambda v.xxv))(\lambda x.f(\lambda v.xxv))\\ & \to (\lambda x.g(\lambda v.xxv))(\lambda x.g(\lambda v.xxv))\\ & \to [x\to \lambda x.g(\lambda v.xxv)]g(\lambda v.xxv)\\ & \to g(\lambda v.(\lambda x.g(\lambda v.xxv))(\lambda v.(\lambda x.g(\lambda v.xxv))v)\\ & =g(\lambda v.(\text{fix}g)v)\end{array}$$

  In Call by value, $\text{fix}g$ doesn't diverge as there a thunk wrapping around the nested $\text{fix}g$.