From 9411795ef23e5be8a9152421cb77631a5cf7efa6 Mon Sep 17 00:00:00 2001 From: Peter Thiemann Date: Fri, 16 Jan 2026 16:16:17 +0100 Subject: [PATCH 1/2] changed requested by @wadler --- src/plfa/part2/Untyped.lagda.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md index 73a560781..64fe1e882 100644 --- a/src/plfa/part2/Untyped.lagda.md +++ b/src/plfa/part2/Untyped.lagda.md @@ -576,6 +576,19 @@ application. # Evaluation +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. + +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. + As previously, progress immediately yields an evaluator. We relate gas to the number of steps in a reduction sequence. From 2b66cade36360b308a09b273f4c39dd87e412ca5 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Fri, 16 Jan 2026 15:17:07 +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 64fe1e882..2f4699746 100644 --- a/src/plfa/part2/Untyped.lagda.md +++ b/src/plfa/part2/Untyped.lagda.md @@ -586,7 +586,7 @@ traversal. 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. As previously, progress immediately yields an evaluator.