From 528956b03394844064544eaac27aa0fa04245bd5 Mon Sep 17 00:00:00 2001 From: "M.V. Hutz" Date: Fri, 16 Jan 2026 19:36:05 -0500 Subject: [PATCH 1/2] feat: add De Bruijn indexed reduction engine Add a new interpreter option (-i debruijn) that uses De Bruijn indices for variable representation, eliminating the need for variable renaming during substitution. - Add -i flag to select interpreter (lambda or debruijn) - Create debruijn package with Expression types (Variable with index, Abstraction without parameter, Application) - Implement shift and substitute operations for De Bruijn indices - Add conversion functions between lambda and De Bruijn representations - Update CLI to support switching between interpreters - Add De Bruijn tests to verify all samples pass Closes #26 --- cmd/lambda/lambda.go | 34 +++++++-- cmd/lambda/lambda_test.go | 80 ++++++++++++++++++- internal/config/config.go | 9 +++ internal/config/parse_from_args.go | 13 ++++ pkg/convert/debruijn_to_lambda.go | 82 ++++++++++++++++++++ pkg/convert/lambda_to_debruijn.go | 44 +++++++++++ pkg/debruijn/expression.go | 119 +++++++++++++++++++++++++++++ pkg/debruijn/iterator.go | 76 ++++++++++++++++++ pkg/debruijn/reducer.go | 72 +++++++++++++++++ pkg/debruijn/shift.go | 32 ++++++++ pkg/debruijn/stringify.go | 35 +++++++++ pkg/debruijn/substitute.go | 34 +++++++++ 12 files changed, 621 insertions(+), 9 deletions(-) create mode 100644 pkg/convert/debruijn_to_lambda.go create mode 100644 pkg/convert/lambda_to_debruijn.go create mode 100644 pkg/debruijn/expression.go create mode 100644 pkg/debruijn/iterator.go create mode 100644 pkg/debruijn/reducer.go create mode 100644 pkg/debruijn/shift.go create mode 100644 pkg/debruijn/stringify.go create mode 100644 pkg/debruijn/substitute.go diff --git a/cmd/lambda/lambda.go b/cmd/lambda/lambda.go index 843897d..f61b538 100644 --- a/cmd/lambda/lambda.go +++ b/cmd/lambda/lambda.go @@ -7,7 +7,9 @@ import ( "git.maximhutz.com/max/lambda/internal/config" "git.maximhutz.com/max/lambda/internal/plugins" "git.maximhutz.com/max/lambda/pkg/convert" + "git.maximhutz.com/max/lambda/pkg/debruijn" "git.maximhutz.com/max/lambda/pkg/lambda" + "git.maximhutz.com/max/lambda/pkg/reducer" "git.maximhutz.com/max/lambda/pkg/saccharine" ) @@ -33,35 +35,51 @@ func main() { compiled := convert.SaccharineToLambda(ast) logger.Info("compiled λ expression", "tree", compiled.String()) - // Create reducer with the compiled expression. - reducer := lambda.NewNormalOrderReducer(&compiled) + // Create reducer based on the selected interpreter. + var red reducer.Reducer + switch options.Interpreter { + case config.DeBruijnInterpreter: + dbExpr := convert.LambdaToDeBruijn(compiled) + logger.Info("converted to De Bruijn", "tree", dbExpr.String()) + red = debruijn.NewNormalOrderReducer(&dbExpr) + default: + red = lambda.NewNormalOrderReducer(&compiled) + } // If the user selected to track CPU performance, attach a profiler. if options.Profile != "" { - plugins.NewPerformance(options.Profile, reducer) + plugins.NewPerformance(options.Profile, red) } // If the user selected to produce a step-by-step explanation, attach an // observer. if options.Explanation { - plugins.NewExplanation(reducer) + plugins.NewExplanation(red) } // If the user opted to track statistics, attach a tracker. if options.Statistics { - plugins.NewStatistics(reducer) + plugins.NewStatistics(red) } // If the user selected for verbose debug logs, attach a reduction tracker. if options.Verbose { - plugins.NewLogs(logger, reducer) + plugins.NewLogs(logger, red) } // Run reduction. - reducer.Reduce() + red.Reduce() // Return the final reduced result. - result := reducer.Expression().String() + // For De Bruijn, convert back to lambda for consistent output. + var result string + if options.Interpreter == config.DeBruijnInterpreter { + dbExpr := red.Expression().(debruijn.Expression) + lambdaExpr := convert.DeBruijnToLambda(dbExpr) + result = lambdaExpr.String() + } else { + result = red.Expression().String() + } err = options.Destination.Write(result) cli.HandleError(err) } diff --git a/cmd/lambda/lambda_test.go b/cmd/lambda/lambda_test.go index 8f671d9..2c463a3 100644 --- a/cmd/lambda/lambda_test.go +++ b/cmd/lambda/lambda_test.go @@ -7,6 +7,7 @@ import ( "testing" "git.maximhutz.com/max/lambda/pkg/convert" + "git.maximhutz.com/max/lambda/pkg/debruijn" "git.maximhutz.com/max/lambda/pkg/lambda" "git.maximhutz.com/max/lambda/pkg/saccharine" "github.com/stretchr/testify/assert" @@ -36,7 +37,36 @@ func runSample(samplePath string) (string, error) { return reducer.Expression().String() + "\n", nil } -// Test that all samples produce expected output. +// Helper function to run a single sample through the De Bruijn interpreter. +func runSampleDeBruijn(samplePath string) (string, error) { + // Read the sample file. + input, err := os.ReadFile(samplePath) + if err != nil { + return "", err + } + + // Parse code into syntax tree. + ast, err := saccharine.Parse(string(input)) + if err != nil { + return "", err + } + + // Compile expression to lambda calculus. + compiled := convert.SaccharineToLambda(ast) + + // Convert to De Bruijn and run reducer. + dbExpr := convert.LambdaToDeBruijn(compiled) + reducer := debruijn.NewNormalOrderReducer(&dbExpr) + reducer.Reduce() + + // Convert back to lambda for output. + result := reducer.Expression().(debruijn.Expression) + lambdaResult := convert.DeBruijnToLambda(result) + + return lambdaResult.String() + "\n", nil +} + +// Test that all samples produce expected output with lambda interpreter. func TestSamplesValidity(t *testing.T) { // Discover all .test files in the tests directory. testFiles, err := filepath.Glob("../../tests/*.test") @@ -65,6 +95,35 @@ func TestSamplesValidity(t *testing.T) { } } +// Test that all samples produce expected output with De Bruijn interpreter. +func TestSamplesValidityDeBruijn(t *testing.T) { + // Discover all .test files in the tests directory. + testFiles, err := filepath.Glob("../../tests/*.test") + assert.NoError(t, err, "Failed to read tests directory.") + assert.NotEmpty(t, testFiles, "No '*.test' files found in directory.") + + for _, testPath := range testFiles { + // Build expected file path. + expectedPath := strings.TrimSuffix(testPath, filepath.Ext(testPath)) + ".expected" + + name := strings.TrimSuffix(filepath.Base(testPath), filepath.Ext(testPath)) + + t.Run(name, func(t *testing.T) { + // Run the sample and capture output. + actual, err := runSampleDeBruijn(testPath) + assert.NoError(t, err, "Failed to run sample.") + + // Read expected output. + expectedBytes, err := os.ReadFile(expectedPath) + assert.NoError(t, err, "Failed to read expected output.") + expected := string(expectedBytes) + + // Compare outputs. + assert.Equal(t, expected, actual, "Output does not match expected.") + }) + } +} + // Benchmark all samples using sub-benchmarks. func BenchmarkSamples(b *testing.B) { // Discover all .test files in the tests directory. @@ -83,3 +142,22 @@ func BenchmarkSamples(b *testing.B) { }) } } + +// Benchmark all samples using De Bruijn interpreter. +func BenchmarkSamplesDeBruijn(b *testing.B) { + // Discover all .test files in the tests directory. + testFiles, err := filepath.Glob("../../tests/*.test") + assert.NoError(b, err, "Failed to read tests directory.") + assert.NotEmpty(b, testFiles, "No '*.test' files found in directory.") + + for _, path := range testFiles { + name := strings.TrimSuffix(filepath.Base(path), filepath.Ext(path)) + + b.Run(name, func(b *testing.B) { + for b.Loop() { + _, err := runSampleDeBruijn(path) + assert.NoError(b, err, "Failed to run sample.") + } + }) + } +} diff --git a/internal/config/config.go b/internal/config/config.go index 063ee2e..d77b799 100644 --- a/internal/config/config.go +++ b/internal/config/config.go @@ -1,6 +1,14 @@ // Package "config" parses ad handles the user settings given to the program. package config +// Interpreter specifies the reduction engine to use. +type Interpreter string + +const ( + LambdaInterpreter Interpreter = "lambda" + DeBruijnInterpreter Interpreter = "debruijn" +) + // Configuration settings for the program. type Config struct { Source Source // The source code given to the program. @@ -9,4 +17,5 @@ type Config struct { Explanation bool // Whether or not to print an explanation of the reduction. Profile string // If not nil, print a CPU profile during execution. Statistics bool // Whether or not to print statistics. + Interpreter Interpreter // The interpreter engine to use. } diff --git a/internal/config/parse_from_args.go b/internal/config/parse_from_args.go index 908e7e1..d73b7b1 100644 --- a/internal/config/parse_from_args.go +++ b/internal/config/parse_from_args.go @@ -14,8 +14,20 @@ func FromArgs() (*Config, error) { profile := flag.String("p", "", "CPU profiling. If an output file is defined, the program will profile its execution and dump its results into it.") file := flag.String("f", "", "File. If set, read source from the specified file.") output := flag.String("o", "", "Output. If set, write result to the specified file. Use '-' for stdout (default).") + interpreter := flag.String("i", "lambda", "Interpreter. The reduction engine to use: 'lambda' or 'debruijn'.") flag.Parse() + // Validate interpreter flag. + var interpType Interpreter + switch *interpreter { + case "lambda": + interpType = LambdaInterpreter + case "debruijn": + interpType = DeBruijnInterpreter + default: + return nil, fmt.Errorf("invalid interpreter: %s (must be 'lambda' or 'debruijn')", *interpreter) + } + // Parse source type. var source Source if *file != "" { @@ -52,5 +64,6 @@ func FromArgs() (*Config, error) { Explanation: *explanation, Profile: *profile, Statistics: *statistics, + Interpreter: interpType, }, nil } diff --git a/pkg/convert/debruijn_to_lambda.go b/pkg/convert/debruijn_to_lambda.go new file mode 100644 index 0000000..0077015 --- /dev/null +++ b/pkg/convert/debruijn_to_lambda.go @@ -0,0 +1,82 @@ +package convert + +import ( + "fmt" + + "git.maximhutz.com/max/lambda/pkg/debruijn" + "git.maximhutz.com/max/lambda/pkg/lambda" + "git.maximhutz.com/max/lambda/pkg/set" +) + +// DeBruijnToLambda converts a De Bruijn indexed expression back to named lambda calculus. +func DeBruijnToLambda(expr debruijn.Expression) lambda.Expression { + return deBruijnToLambdaWithContext(expr, []string{}) +} + +func deBruijnToLambdaWithContext(expr debruijn.Expression, context []string) lambda.Expression { + switch e := expr.(type) { + case *debruijn.Variable: + index := e.Index() + if index < len(context) { + // Bound variable: look up name in context. + name := context[len(context)-1-index] + return lambda.NewVariable(name) + } + // Free variable: use the label if available. + if e.Label() != "" { + return lambda.NewVariable(e.Label()) + } + // Generate a name for free variables without labels. + return lambda.NewVariable(fmt.Sprintf("free%d", index)) + + case *debruijn.Abstraction: + // Generate a fresh parameter name. + used := collectUsedNames(e.Body(), context) + paramName := generateFreshName(used) + newContext := append(context, paramName) + body := deBruijnToLambdaWithContext(e.Body(), newContext) + return lambda.NewAbstraction(paramName, body) + + case *debruijn.Application: + abs := deBruijnToLambdaWithContext(e.Abstraction(), context) + arg := deBruijnToLambdaWithContext(e.Argument(), context) + return lambda.NewApplication(abs, arg) + + default: + panic("unknown expression type") + } +} + +// collectUsedNames gathers all variable labels used in an expression. +func collectUsedNames(expr debruijn.Expression, context []string) *set.Set[string] { + used := set.New[string]() + for _, name := range context { + used.Add(name) + } + collectUsedNamesHelper(expr, used) + return used +} + +func collectUsedNamesHelper(expr debruijn.Expression, used *set.Set[string]) { + switch e := expr.(type) { + case *debruijn.Variable: + if e.Label() != "" { + used.Add(e.Label()) + } + case *debruijn.Abstraction: + collectUsedNamesHelper(e.Body(), used) + case *debruijn.Application: + collectUsedNamesHelper(e.Abstraction(), used) + collectUsedNamesHelper(e.Argument(), used) + } +} + +// generateFreshName creates a fresh variable name not in the used set. +func generateFreshName(used *set.Set[string]) string { + for i := 0; ; i++ { + name := fmt.Sprintf("_%d", i) + if !used.Has(name) { + return name + } + } +} diff --git a/pkg/convert/lambda_to_debruijn.go b/pkg/convert/lambda_to_debruijn.go new file mode 100644 index 0000000..a5cd20d --- /dev/null +++ b/pkg/convert/lambda_to_debruijn.go @@ -0,0 +1,44 @@ +package convert + +import ( + "git.maximhutz.com/max/lambda/pkg/debruijn" + "git.maximhutz.com/max/lambda/pkg/lambda" +) + +// LambdaToDeBruijn converts a lambda calculus expression to De Bruijn indexed form. +// The context parameter tracks bound variables from outer abstractions. +func LambdaToDeBruijn(expr lambda.Expression) debruijn.Expression { + return lambdaToDeBruijnWithContext(expr, []string{}) +} + +func lambdaToDeBruijnWithContext(expr lambda.Expression, context []string) debruijn.Expression { + switch e := expr.(type) { + case *lambda.Variable: + name := e.Value() + // Search for the variable in the context (innermost to outermost). + for i := len(context) - 1; i >= 0; i-- { + if context[i] == name { + index := len(context) - 1 - i + return debruijn.NewVariable(index, name) + } + } + // Free variable: use a negative index to mark it. + // We encode free variables with index = len(context) + position. + // For simplicity, we use a large index that won't conflict. + return debruijn.NewVariable(len(context), name) + + case *lambda.Abstraction: + // Add the parameter to the context. + newContext := append(context, e.Parameter()) + body := lambdaToDeBruijnWithContext(e.Body(), newContext) + return debruijn.NewAbstraction(body) + + case *lambda.Application: + abs := lambdaToDeBruijnWithContext(e.Abstraction(), context) + arg := lambdaToDeBruijnWithContext(e.Argument(), context) + return debruijn.NewApplication(abs, arg) + + default: + panic("unknown expression type") + } +} diff --git a/pkg/debruijn/expression.go b/pkg/debruijn/expression.go new file mode 100644 index 0000000..7f0169e --- /dev/null +++ b/pkg/debruijn/expression.go @@ -0,0 +1,119 @@ +// Package debruijn provides De Bruijn indexed lambda calculus expressions. +// De Bruijn indices eliminate the need for variable names by using numeric +// indices to refer to bound variables, avoiding capture issues during substitution. +package debruijn + +import "git.maximhutz.com/max/lambda/pkg/expr" + +// Expression is the interface for all De Bruijn indexed expression types. +// It embeds the general expr.Expression interface for cross-mode compatibility. +type Expression interface { + expr.Expression + Accept(Visitor) +} + +/** ------------------------------------------------------------------------- */ + +// Abstraction represents a lambda abstraction without a named parameter. +// In De Bruijn notation, the parameter is implicit and referenced by index 0 +// within the body. +type Abstraction struct { + body Expression +} + +// Body returns the body of the abstraction. +func (a *Abstraction) Body() Expression { + return a.body +} + +// Accept implements the Visitor pattern. +func (a *Abstraction) Accept(v Visitor) { + v.VisitAbstraction(a) +} + +// String returns the De Bruijn notation string representation. +func (a *Abstraction) String() string { + return Stringify(a) +} + +// NewAbstraction creates a new De Bruijn abstraction with the given body. +func NewAbstraction(body Expression) *Abstraction { + return &Abstraction{body: body} +} + +/** ------------------------------------------------------------------------- */ + +// Application represents the application of one expression to another. +type Application struct { + abstraction Expression + argument Expression +} + +// Abstraction returns the function expression being applied. +func (a *Application) Abstraction() Expression { + return a.abstraction +} + +// Argument returns the argument expression. +func (a *Application) Argument() Expression { + return a.argument +} + +// Accept implements the Visitor pattern. +func (a *Application) Accept(v Visitor) { + v.VisitApplication(a) +} + +// String returns the De Bruijn notation string representation. +func (a *Application) String() string { + return Stringify(a) +} + +// NewApplication creates a new application expression. +func NewApplication(abstraction Expression, argument Expression) *Application { + return &Application{abstraction: abstraction, argument: argument} +} + +/** ------------------------------------------------------------------------- */ + +// Variable represents a De Bruijn indexed variable. +// The index indicates how many binders to skip to find the binding abstraction. +// The label is an optional hint for display purposes. +type Variable struct { + index int + label string +} + +// Index returns the De Bruijn index. +func (v *Variable) Index() int { + return v.index +} + +// Label returns the optional variable label. +func (v *Variable) Label() string { + return v.label +} + +// Accept implements the Visitor pattern. +func (v *Variable) Accept(visitor Visitor) { + visitor.VisitVariable(v) +} + +// String returns the De Bruijn notation string representation. +func (v *Variable) String() string { + return Stringify(v) +} + +// NewVariable creates a new De Bruijn variable with the given index and label. +func NewVariable(index int, label string) *Variable { + return &Variable{index: index, label: label} +} + +/** ------------------------------------------------------------------------- */ + +// Visitor interface for traversing De Bruijn expressions. +type Visitor interface { + VisitAbstraction(*Abstraction) + VisitApplication(*Application) + VisitVariable(*Variable) +} diff --git a/pkg/debruijn/iterator.go b/pkg/debruijn/iterator.go new file mode 100644 index 0000000..d4386b6 --- /dev/null +++ b/pkg/debruijn/iterator.go @@ -0,0 +1,76 @@ +package debruijn + +// Iterator provides depth-first traversal of De Bruijn expressions. +type Iterator struct { + trace []*Expression +} + +// NewIterator creates a new iterator starting at the given expression. +func NewIterator(expr *Expression) *Iterator { + return &Iterator{[]*Expression{expr}} +} + +// Done returns true when the iterator has finished traversal. +func (i *Iterator) Done() bool { + return len(i.trace) == 0 +} + +// Current returns a pointer to the current expression. +func (i *Iterator) Current() *Expression { + if i.Done() { + return nil + } + + return i.trace[len(i.trace)-1] +} + +// Parent returns a pointer to the parent expression. +func (i *Iterator) Parent() *Expression { + if len(i.trace) < 2 { + return nil + } + + return i.trace[len(i.trace)-2] +} + +// Swap replaces the current expression with the given expression. +func (i *Iterator) Swap(with Expression) { + current := i.Current() + if current != nil { + *current = with + } +} + +// Back moves the iterator back to the parent expression. +func (i *Iterator) Back() bool { + if i.Done() { + return false + } + + i.trace = i.trace[:len(i.trace)-1] + return true +} + +// Next advances the iterator to the next expression in leftmost-outermost order. +func (i *Iterator) Next() { + switch typed := (*i.Current()).(type) { + case *Abstraction: + i.trace = append(i.trace, &typed.body) + case *Application: + i.trace = append(i.trace, &typed.abstraction) + case *Variable: + for len(i.trace) > 1 { + if app, ok := (*i.Parent()).(*Application); ok { + if app.abstraction == *i.Current() { + i.Back() + i.trace = append(i.trace, &app.argument) + return + } + } + + i.Back() + } + + i.trace = []*Expression{} + } +} diff --git a/pkg/debruijn/reducer.go b/pkg/debruijn/reducer.go new file mode 100644 index 0000000..40a5c82 --- /dev/null +++ b/pkg/debruijn/reducer.go @@ -0,0 +1,72 @@ +package debruijn + +import ( + "git.maximhutz.com/max/lambda/pkg/emitter" + "git.maximhutz.com/max/lambda/pkg/expr" + "git.maximhutz.com/max/lambda/pkg/reducer" +) + +// NormalOrderReducer implements normal order (leftmost-outermost) reduction +// for De Bruijn indexed lambda calculus expressions. +type NormalOrderReducer struct { + emitter.BaseEmitter[reducer.Event] + expression *Expression +} + +// NewNormalOrderReducer creates a new normal order reducer. +func NewNormalOrderReducer(expression *Expression) *NormalOrderReducer { + return &NormalOrderReducer{ + BaseEmitter: *emitter.New[reducer.Event](), + expression: expression, + } +} + +// Expression returns the current expression state. +func (r *NormalOrderReducer) Expression() expr.Expression { + return *r.expression +} + +// isViable checks if an expression is a redex (reducible expression). +// A redex is an application of an abstraction to an argument. +func isViable(e *Expression) (*Abstraction, Expression, bool) { + if e == nil { + return nil, nil, false + } else if app, appOk := (*e).(*Application); !appOk { + return nil, nil, false + } else if fn, fnOk := app.abstraction.(*Abstraction); !fnOk { + return nil, nil, false + } else { + return fn, app.argument, true + } +} + +// 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) + it := NewIterator(r.expression) + + for !it.Done() { + if fn, arg, ok := isViable(it.Current()); !ok { + it.Next() + } else { + it.Swap(betaReduce(fn, arg)) + r.Emit(reducer.StepEvent) + + if _, _, ok := isViable(it.Parent()); ok { + it.Back() + } + } + } + + r.Emit(reducer.StopEvent) +} diff --git a/pkg/debruijn/shift.go b/pkg/debruijn/shift.go new file mode 100644 index 0000000..e836b6a --- /dev/null +++ b/pkg/debruijn/shift.go @@ -0,0 +1,32 @@ +package debruijn + +// Shift increments all free variable indices in an expression by the given amount. +// A variable is free if its index is >= the cutoff (depth of nested abstractions). +// This is necessary when substituting an expression into a different binding context. +func Shift(expr Expression, amount int, cutoff int) Expression { + switch e := expr.(type) { + case *Variable: + if e.index >= cutoff { + return NewVariable(e.index+amount, e.label) + } + return e + + case *Abstraction: + newBody := Shift(e.body, amount, cutoff+1) + if newBody == e.body { + return e + } + return NewAbstraction(newBody) + + case *Application: + newAbs := Shift(e.abstraction, amount, cutoff) + newArg := Shift(e.argument, amount, cutoff) + if newAbs == e.abstraction && newArg == e.argument { + return e + } + return NewApplication(newAbs, newArg) + + default: + return expr + } +} diff --git a/pkg/debruijn/stringify.go b/pkg/debruijn/stringify.go new file mode 100644 index 0000000..573d216 --- /dev/null +++ b/pkg/debruijn/stringify.go @@ -0,0 +1,35 @@ +package debruijn + +import ( + "strconv" + "strings" +) + +type stringifyVisitor struct { + builder strings.Builder +} + +func (v *stringifyVisitor) VisitVariable(a *Variable) { + v.builder.WriteString(strconv.Itoa(a.index)) +} + +func (v *stringifyVisitor) VisitAbstraction(f *Abstraction) { + v.builder.WriteRune('\\') + v.builder.WriteRune('.') + f.body.Accept(v) +} + +func (v *stringifyVisitor) VisitApplication(c *Application) { + v.builder.WriteRune('(') + c.abstraction.Accept(v) + v.builder.WriteRune(' ') + c.argument.Accept(v) + v.builder.WriteRune(')') +} + +// Stringify converts a De Bruijn expression to its string representation. +func Stringify(e Expression) string { + b := &stringifyVisitor{builder: strings.Builder{}} + e.Accept(b) + return b.builder.String() +} diff --git a/pkg/debruijn/substitute.go b/pkg/debruijn/substitute.go new file mode 100644 index 0000000..d3bc841 --- /dev/null +++ b/pkg/debruijn/substitute.go @@ -0,0 +1,34 @@ +package debruijn + +// Substitute replaces the variable at the given index with the replacement expression. +// The replacement is shifted appropriately as we descend into nested abstractions. +func Substitute(expr Expression, index int, replacement Expression) Expression { + switch e := expr.(type) { + case *Variable: + if e.index == index { + return replacement + } + return e + + case *Abstraction: + // When entering an abstraction, increment the target index and shift the + // replacement to account for the new binding context. + shiftedReplacement := Shift(replacement, 1, 0) + newBody := Substitute(e.body, index+1, shiftedReplacement) + if newBody == e.body { + return e + } + return NewAbstraction(newBody) + + case *Application: + newAbs := Substitute(e.abstraction, index, replacement) + newArg := Substitute(e.argument, index, replacement) + if newAbs == e.abstraction && newArg == e.argument { + return e + } + return NewApplication(newAbs, newArg) + + default: + return expr + } +} -- 2.49.1 From 21ae2ca91cd449ece43430ee16a3e2fc9d16d181 Mon Sep 17 00:00:00 2001 From: "M.V. Hutz" Date: Sat, 17 Jan 2026 14:53:09 -0500 Subject: [PATCH 2/2] 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 { -- 2.49.1