67 lines
1.8 KiB
Go
67 lines
1.8 KiB
Go
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
|
|
}
|
|
}
|
|
|
|
// 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 {
|
|
// 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 {
|
|
it.Back()
|
|
}
|
|
}
|
|
}
|
|
|
|
r.Emit(reducer.StopEvent)
|
|
}
|