Example of Step by Step Evaluation

• predefined variables:
  • $FAC = (Y M)$
  • $M = \lambda fac.\lambda n.(IF (= n\hspace{0.25em} 0) 1 (* n (fac (- n\hspace{0.25em} 1))))$
• expression to be evaluated:
  
  

  
  $(FAC\hspace{0.25em} 1)$

• expression rewritten replacing $FAC$, a fixed point of $M$, by $(Y M)$:
  
  

  
  $((Y M) 1)$

• expression rewritten using rule 12:
  
  

  
  $((M (Y M)) 1)$

• expression rewritten substituting the 1st occurrence of $M$::
  
  

  
  $((\lambda fac.\lambda n.(IF (= n\hspace{0.25em} 0) 1 (* n (fac (- n\hspace{0.25em} 1)))) (Y M)) 1)$

• performing $_\beta$-reduction by substituting variable $fac$ in the body of the lambda abstraction by the argument $(Y\hspace{0.25em} M)$:
  
  

  
  $(\lambda n.(IF (= n\hspace{0.25em} 0) 1 (* n ((Y M) (- n\hspace{0.25em} 1)))) 1)$

• performing $_\beta$-reduction by substituting variable $n$ in the body of the lambda abstraction by the argument $\hspace{0.25em}1$:
  
  

  
  $(IF (= 1\hspace{0.25em} 0) 1 (* 1 ((Y M) (- 1\hspace{0.25em} 1))))$

• evaluating the `IF'-expression by selecting the `no'-branch and evaluating the subtraction:
  
  

  
  $(* 1 ((Y M) 0))$

• expression rewritten substituting $(Y M)$ by $(M (Y M))$ using rule 12:
  
  

  
  $(* 1 ((M (Y M)) 0))$

• expression rewritten substituting the first occurrence of the variable $M$ by its value:
  
  

  
  $(* 1 ((\lambda fac.\lambda n.(IF (= n\hspace{0.25em} 0) 1 (* n (fac (- n\hspace{0.25em} 1)))) (Y M)) 0))$

• performing $_\beta$-reduction substituting `fac' in the body of the lambda abstraction by the argument $(Y M)$:
  
  

  
  $(* 1 (\lambda n.(IF (= n\hspace{0.25em} 0) 1 (* n ((Y M) (- n\hspace{0.25em} 1))))) 0)$

• performing $_\beta$-reduction substituting $n$ in the body of the lambda abstraction by the argument $\hspace{0.25em}0$:
  
  

  
  $(* 1 ((IF (= 0\hspace{0.25em} 0) 1 (* 0 ((Y M) (- 0\hspace{0.25em} 1))))))$

• evaluating `IF'-expression returning the `yes'-branch:
  
  

  
  $(* 1\hspace{0.25em} 1)$

• evaluating the multiplication:
  
  

  
  $1$