.. _ReductionStrategies: .. raw:: html .. |--| unicode:: U+2013 .. en dash .. |---| unicode:: U+2014 .. em dash, trimming surrounding whitespace :trim: .. This file is part of the OpenDSA eTextbook project. See .. http://algoviz.org/OpenDSA for more details. .. Copyright (c) 2012-13 by the OpenDSA Project Contributors, and .. distributed under an MIT open source license. .. avmetadata:: :author: David Furcy and Tom Naps Reduction Strategies ==================== Applicative Order ----------------- How many :math:\beta redexes are in :math:(\lambda x.m \; (\lambda x.(x \; x) \; \lambda x.(x \; x)))? You should be able to find two. Depending on which one you choose to reduce first, you may find that you end up with :math:m as your "answer" or that you end up with the same expression that you started with, that is, the beta-reduction equivalent of an infinite loop. We have seen that evaluation of expressions in the :math:\lambda calculus is essentially :math:\beta reduction, which can be defined simply in terms of substitution: :math:(\lambda p.b \; a) \equiv subst(a,p,b) But there is an additional consideration involved: :math:a and :math:b in the preceding :math:\beta redex can each contain :math:\beta redexes themselves. We then need to recursively reduce them, which raises the following questions: #. Which redex should we reduce first, the top-level redex, or a nested one? #. Does it matter which one we do first? What are the consequences of these two strategies? #. Do different reduction strategies lead to different results? A key to partially answering the second and third questions above is the **Church-Rosser Theorem**, which we will merely state and not prove. According to the Church-Rosser theorem, *if two different reduction strategies both lead to an answer, then they will lead to the same answer.* So the answers to the second and third questions are no with the following caveat: any reduction strategy that leads to an answer will give the same answer. The key here is whether or not the strategy leads to an answer, and the Church-Rosser theorem neither guarantees termination nor does it guarantee that an answer will be found if it exists. The strategy that JavaScript uses in the substitution model of computation is called **applicative order reduction**. With this strategy, to evaluate an expression of the form f(arg1,arg2,arg3,...), we: #. Evaluate each of the subexpressions from left to right, including *f* if it requires evaluation. (How could it require evaluation?) #. Apply the leftmost result, which should be a function, to the rest of the evaluated subexpressions. The applicative order strategy is characterized by evaluating the subexpressions first. That is, we only perform an application when each of the subexpressions has been reduced and there are no redexes left except the topmost application. Consider: :math:(\lambda x.((x \; y) \; (y \; x)) \; (\lambda w.(w \; w) \; z)) Applicative order evaluation will first reduce :math:(\lambda w.(w \; w) \; z), getting :math:(z \; z). This result will then be substituted in for :math:x in :math:((x \; y) \; (y \; x)), yielding :math:(((z \; z) \; y) \; (y \; (z \; z))) as the final answer. Although applicative order reduction finds its answer to the preceding problem in two reductions, when it is used for the first example we considered in this section, that is, :math:(\lambda x.m \; (\lambda x.(x \; x) \; \lambda x.(x \; x))) we end up in the infinite loop we referred to earlier. Normal Order ------------ **Normal order reduction** reduces the leftmost :math:\beta redex first before reducing the subexpressions inside of it and those that follow it. While applicative order proceeds by evaluating the subexpressions and then applying the function, normal order evaluation proceeds by applying the function first and then evaluating the subexpressions. Because normal order reduction delays its evaluation of the arguments to a function, it correctly gets :math:m when applied to the example :math:(\lambda\ x.m (:math:\lambda x.(x \; x) \; \lambda x.(x \; x))) on which applicative order looped infinitely. When applied to our other example :math:(\lambda x.((x \; y) \; (y \; x)) \; (\lambda w.(w \; w) \; z)), normal order will substitute :math:(\lambda w.(w \; w) \; z) for both of the :math:x appearing in :math:((x \; y) \; (y \; x)). It will then have to evaluate :math:(\lambda w.(w \; w) \; z) **twice** before getting the final answer :math:(((z \; z) \; y) \; (y \; (z \; z))). Beta Reduction Order (1) ------------------------ This problem focuses on the first step (i.e., :math:\beta-reduction) in the evaluation of a :math:\lambda-expression with the two evaluation strategies that we discussed. To get credit for this randomized exercise, you must solve it correctly three times in a row. .. avembed:: Exercises/PL/BetaReductionOrder1.html ka :module: ReductionStrategies :points: 1.0 :required: True :threshold: 3 :exer_opts: JXOP-debug=true&JOP-lang=en&JXOP-code=java_generic :long_name: Beta Reduction Order 1 Beta Reduction Order (2) ------------------------ In this problem, you have to study the complete evaluation of a :math:\lambda-expression with the two evaluation strategies that we discussed. To get credit for this randomized exercise, you must solve it correctly three times in a row. .. avembed:: Exercises/PL/BetaReductionOrder2.html ka :module: ReductionStrategies :points: 1.0 :required: True :threshold: 3 :exer_opts: JXOP-debug=true&JOP-lang=en&JXOP-code=java_generic :long_name: Beta Reduction Order 2 Applicative Order Proficiency Exercise -------------------------------------- In this problem, you have to perform a full evaluation of a randomly selected :math:\lambda expression, that is, perform as many :math:\beta-reductions as it takes until a :math:\beta-normal form is reached. For this problem, you must use the *applicative-order* reduction strategy. To get credit for this problem, you only need to solve one problem instance correctly. However, each problem instance contains several steps that you must perform correctly (in this case, each step is a :math:\beta-reduction). Read and follow the directions carefully. Note that the correct answer (called the *model answer*) is available. However, if you look it up, you will not get credit for the current problem instance. To get another chance for credit, start a new problem instance by clicking the *Reset* button. .. avembed:: AV/PL/applicativeOrderPRO.html pe :module: ReductionStrategies :points: 2.0 :required: True :threshold: 1.0 :exer_opts: JXOP-debug=true&JOP-lang=en&JXOP-code=java_generic :long_name: Applicative-order reduction Proficiency Exercise Normal Order Proficiency Exercise --------------------------------- In this problem, you have to perform a full evaluation of a randomly selected :math:\lambda expression, that is, perform as many :math:\beta-reductions as it takes until a :math:\beta-normal form is reached. For this problem, you must use the **normal-order** reduction strategy. To get credit for this problem, you only need to solve one problem instance correctly. However, each problem instance contains several steps that you must perform correctly (in this case, each step is a :math:\beta-reduction). Read and follow the directions carefully. Note that the correct answer (called the *model answer*) is available. However, if you look it up, you will not get credit for the current problem instance. To get another chance for credit, start a new problem instance by clicking the *Reset* button. .. avembed:: AV/PL/normalOrderPRO.html pe :module: ReductionStrategies :points: 2.0 :required: True :threshold: 1.0 :exer_opts: JXOP-debug=true&JOP-lang=en&JXOP-code=java_generic :long_name: Normal-order reduction Proficiency Exercise