From c6c218b409fd108359dcfcdda70dbdc3ef19df7f Mon Sep 17 00:00:00 2001 From: Peter Thiemann Date: Fri, 9 Feb 2024 14:07:44 +0100 Subject: [PATCH 1/2] paragraph on normal order reduction in Untyped chapter --- src/plfa/part2/Untyped.lagda.md | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md index 6b9142285..5dabbbb6d 100644 --- a/src/plfa/part2/Untyped.lagda.md +++ b/src/plfa/part2/Untyped.lagda.md @@ -540,6 +540,35 @@ which matches only if both pattern `P` and pattern `Q` match. Character required around it. In this case, the pattern ensures that `L` is an application. +We already observed that reduction in the untyped lambda calculus is +non-deterministic. However, the `progress` function is deterministic and +thus it picks one particular reduction sequence out of many possible ones. +In other words, `progress` implements a _reduction strategy_ that searches +for the next redex in a top-down traversal of the term, visiting any subterms +from left to right. It reduces the first redex that it encounters on this +traversal. We can see that as follows in the definition of `progress`: + +* There is no choice in the variable case. +* At a lambda abstraction, `progress` continues the search in the body. +* At an application, there are several subcases. + + If the application is a beta redex, it gets reduced without looking + further into the subterms. + + Otherwise, the subterms are processed from left to right. + +What other choices do we have? +* At any application, we might choose to reduce the right, argument subterm. + But doing so introduces a chance of nontermination because the beta reduction + may ignore its argument. +* At a beta redex, we might choose to reduce the body of the lambda. + But we will have more opportunities reducing the body right after the beta + reduction. + +The strategy implemented by `progress` is known as _normal order reduction_ +or _leftmost outermost reduction_. It has the pleasing property that +if any reduction sequence terminates in a normal form, then +normal order reduction terminates in the same normal form. + + ## Evaluation As previously, progress immediately yields an evaluator. From 4e021f23a60ac60203c30b675c8c61044cc479e6 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Fri, 9 Feb 2024 13:11:42 +0000 Subject: [PATCH 2/2] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- src/plfa/part2/Untyped.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md index 5dabbbb6d..1e1e33b2d 100644 --- a/src/plfa/part2/Untyped.lagda.md +++ b/src/plfa/part2/Untyped.lagda.md @@ -565,7 +565,7 @@ What other choices do we have? The strategy implemented by `progress` is known as _normal order reduction_ or _leftmost outermost reduction_. It has the pleasing property that -if any reduction sequence terminates in a normal form, then +if any reduction sequence terminates in a normal form, then normal order reduction terminates in the same normal form.