index.md (2009B)
1 +++ 2 title = "Strategies" 3 +++ 4 5 # Strategies 6 **strategy:** how to reduce a term 7 8 **normalising strategy:** gives a reduction sequence to a normal form. leftmost outermost. 9 10 e.g. given: (λy.z)(Ω) 11 12  13 14 - Outermost: not contained in another redex 15 - Innermost: does not contain another redex 16 - Leftmost: the one most on the left obviously 17 18 ## Call by need 19 reduce in every step the leftmost outermost redex. if it finds a loop, no normal form. 20 21 e.g. in above: (λy.z)(Ω) ➝ β z 22 23 another e.g.: (λx.fxx)((λx.x) 3) ➝ β f ((λx.x) 3) ((λx.x) 3) ➝ β f 3 3 24 25 pros: 26 - normalising 27 - all steps contribute to normal form 28 cons: 29 - redexes may be copied 30 - difficult to implement 31 32 ## Call by value 33 Reduce in every step the leftmost innermost redex. 34 35 e.g. in above: (λy.z)(Ω) ➝ β (λ.z)(Ω) ➝ β (λy.z)(Ω) ➝ β … 36 37 e.g.: (λx.fxx) ((λx.x)3) ➝ β (λx.fxx) 3 ➝ β f 3 3 38 39 pros: 40 - redexes not copied 41 - easy to implement 42 cons: 43 - not normalising 44 - reduction to normal form may reduce redexes that don’t contribute to normal form 45 46 ### Rightmost-outermost: not normalizing! 47 Rightmost outermost is not normalising. For example, take the term ((λx.x)(λx.y))(Ω). 48 49 Leftmost outermost: 50 51 <pre> 52 ((λx.x)(λx.y))(Ω) => (λx.y)(Ω) [reduces the λx.x] 53 => y 54 </pre> 55 56 Rightmost outermost: 57 58 <pre> 59 ((λx.x)(λx.y))(Ω) => ((λx.x)(λx.y))(Ω) 60 = ((λx.x)(λx.y))((λx.xx)(λx.xx)) [reduces the application in Ω] 61 => ((λx.x)(λx.y))(Ω) 62 => ((λx.x)(λx.y))(Ω) 63 => etc. 64 </pre> 65 66 It's easier to see this if you draw the tree. An application with an application on the left side can't be a redex. The leftmost outermost redex is the λx.x, whereas the rightmost outermost strategy reduces the application inside the Ω. 67 68 Leftmost outermost gives a result, while rightmost outermost goes into a loop. Therefore, rightmost outermost is not a normalizing strategy.