From 21ae2ca91cd449ece43430ee16a3e2fc9d16d181 Mon Sep 17 00:00:00 2001 From: "M.V. Hutz" Date: Sat, 17 Jan 2026 14:53:09 -0500 Subject: [PATCH] feat: progress --- pkg/debruijn/reducer.go | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/pkg/debruijn/reducer.go b/pkg/debruijn/reducer.go index 40a5c82..4cfb15e 100644 --- a/pkg/debruijn/reducer.go +++ b/pkg/debruijn/reducer.go @@ -40,16 +40,6 @@ func isViable(e *Expression) (*Abstraction, Expression, bool) { } } -// betaReduce performs a single beta reduction step. -// Given (\. body) arg, it substitutes arg for index 0 in body, -// then shifts the result down to account for the removed abstraction. -func betaReduce(fn *Abstraction, arg Expression) Expression { - // Substitute arg for variable 0 in the body. - substituted := Substitute(fn.body, 0, Shift(arg, 1, 0)) - // Shift down to account for the removed abstraction. - return Shift(substituted, -1, 0) -} - // Reduce performs normal order reduction on a De Bruijn expression. func (r *NormalOrderReducer) Reduce() { r.Emit(reducer.StartEvent) @@ -59,7 +49,11 @@ func (r *NormalOrderReducer) Reduce() { if fn, arg, ok := isViable(it.Current()); !ok { it.Next() } else { - it.Swap(betaReduce(fn, arg)) + // Substitute arg for variable 0 in the body. + substituted := Substitute(fn.body, 0, Shift(arg, 1, 0)) + // Shift down to account for the removed abstraction. + it.Swap(Shift(substituted, -1, 0)) + r.Emit(reducer.StepEvent) if _, _, ok := isViable(it.Parent()); ok {