diff --git a/pkg/convert/saccharine_to_lambda.go b/pkg/convert/saccharine_to_lambda.go index a76a968..77f2753 100644 --- a/pkg/convert/saccharine_to_lambda.go +++ b/pkg/convert/saccharine_to_lambda.go @@ -21,7 +21,7 @@ func encodeAbstraction(n *saccharine.Abstraction) lambda.Expression { // If the function has no parameters, it is a thunk. Lambda calculus still // requires _some_ parameter exists, so generate one. if len(parameters) == 0 { - freeVars := result.GetFree() + freeVars := lambda.GetFree(result) freshName := lambda.GenerateFreshName(freeVars) parameters = append(parameters, freshName) } @@ -65,7 +65,7 @@ func reduceLet(s *saccharine.LetStatement, e lambda.Expression) lambda.Expressio } func reduceDeclare(s *saccharine.DeclareStatement, e lambda.Expression) lambda.Expression { - freshVar := lambda.GenerateFreshName(e.GetFree()) + freshVar := lambda.GenerateFreshName(lambda.GetFree(e)) return lambda.Application{ Abstraction: lambda.Abstraction{Parameter: freshVar, Body: e}, diff --git a/pkg/engine/normalorder/reduce_once.go b/pkg/engine/normalorder/reduce_once.go index 50d4d5a..241c01a 100644 --- a/pkg/engine/normalorder/reduce_once.go +++ b/pkg/engine/normalorder/reduce_once.go @@ -18,7 +18,7 @@ func ReduceOnce(e lambda.Expression) (lambda.Expression, bool) { case lambda.Application: if fn, fnOk := e.Abstraction.(lambda.Abstraction); fnOk { - return fn.Body.Substitute(fn.Parameter, e.Argument), true + return lambda.Substitute(fn.Body, fn.Parameter, e.Argument), true } abs, reduced := ReduceOnce(e.Abstraction) diff --git a/pkg/lambda/codec.go b/pkg/lambda/codec.go index 04cd83c..c1c96bb 100644 --- a/pkg/lambda/codec.go +++ b/pkg/lambda/codec.go @@ -6,14 +6,14 @@ import ( "git.maximhutz.com/max/lambda/pkg/codec" ) -type Marshaler struct{} +type Codec struct{} -func (m Marshaler) Decode(string) (Expression, error) { +func (m Codec) Decode(string) (Expression, error) { return nil, fmt.Errorf("unimplemented") } -func (m Marshaler) Encode(e Expression) (string, error) { - return e.String(), nil +func (m Codec) Encode(e Expression) (string, error) { + return Stringify(e), nil } -var _ codec.Codec[Expression] = (*Marshaler)(nil) +var _ codec.Codec[Expression] = (*Codec)(nil) diff --git a/pkg/lambda/get_free_variables.go b/pkg/lambda/get_free_variables.go index dbed3e5..71d15a1 100644 --- a/pkg/lambda/get_free_variables.go +++ b/pkg/lambda/get_free_variables.go @@ -1,19 +1,27 @@ package lambda -import "git.maximhutz.com/max/lambda/pkg/set" +import ( + "fmt" -func (e Variable) GetFree() set.Set[string] { - return set.New(e.Name) -} + "git.maximhutz.com/max/lambda/pkg/set" +) -func (e Abstraction) GetFree() set.Set[string] { - vars := e.Body.GetFree() - vars.Remove(e.Parameter) - return vars -} - -func (e Application) GetFree() set.Set[string] { - vars := e.Abstraction.GetFree() - vars.Merge(e.Argument.GetFree()) - return vars +// GetFree returns the set of all free variable names in the expression. +// This function does not mutate the input expression. +// The returned set is newly allocated and can be modified by the caller. +func GetFree(e Expression) set.Set[string] { + switch e := e.(type) { + case Variable: + return set.New(e.Name) + case Abstraction: + vars := GetFree(e.Body) + vars.Remove(e.Parameter) + return vars + case Application: + vars := GetFree(e.Abstraction) + vars.Merge(GetFree(e.Argument)) + return vars + default: + panic(fmt.Errorf("unknown expression type: %v", e)) + } } diff --git a/pkg/lambda/is_free_variable.go b/pkg/lambda/is_free_variable.go index 5db42a6..a965668 100644 --- a/pkg/lambda/is_free_variable.go +++ b/pkg/lambda/is_free_variable.go @@ -1,12 +1,18 @@ package lambda -func (e Variable) IsFree(n string) bool { - return e.Name == n -} +import "fmt" -func (e Abstraction) IsFree(n string) bool { - return e.Parameter != n && e.Body.IsFree(n) -} -func (e Application) IsFree(n string) bool { - return e.Abstraction.IsFree(n) || e.Argument.IsFree(n) +// IsFree returns true if the variable name n occurs free in the expression. +// This function does not mutate the input expression. +func IsFree(e Expression, n string) bool { + switch e := e.(type) { + case Variable: + return e.Name == n + case Abstraction: + return e.Parameter != n && IsFree(e.Body, n) + case Application: + return IsFree(e.Abstraction, n) || IsFree(e.Argument, n) + default: + panic(fmt.Errorf("unknown expression type: %v", e)) + } } diff --git a/pkg/lambda/lambda.go b/pkg/lambda/lambda.go index b3680c5..d92ca4d 100644 --- a/pkg/lambda/lambda.go +++ b/pkg/lambda/lambda.go @@ -1,56 +1,27 @@ package lambda -import ( - "fmt" - - "git.maximhutz.com/max/lambda/pkg/set" -) - // Expression is the interface for all lambda calculus expression types. // It embeds the general expr.Expression interface for cross-mode compatibility. type Expression interface { - fmt.Stringer - - // Substitute replaces all free occurrences of the target variable with the - // replacement expression. Alpha-renaming is performed automatically to - // avoid variable capture. - Substitute(target string, replacement Expression) Expression - - // GetFree returns the set of all free variable names in the expression. - // This function does not mutate the input expression. - // The returned set is newly allocated and can be modified by the caller. - GetFree() set.Set[string] - - // Rename replaces all occurrences of the target variable name with the new name. - Rename(target string, newName string) Expression - - // IsFree returns true if the variable name n occurs free in the expression. - // This function does not mutate the input expression. - IsFree(n string) bool + expression() } -/** ------------------------------------------------------------------------- */ - type Abstraction struct { Parameter string Body Expression } -var _ Expression = Abstraction{} - -/** ------------------------------------------------------------------------- */ +func (a Abstraction) expression() {} type Application struct { Abstraction Expression Argument Expression } -var _ Expression = Application{} - -/** ------------------------------------------------------------------------- */ +func (a Application) expression() {} type Variable struct { Name string } -var _ Expression = Variable{} +func (v Variable) expression() {} diff --git a/pkg/lambda/rename.go b/pkg/lambda/rename.go index 10e438d..eaa31ca 100644 --- a/pkg/lambda/rename.go +++ b/pkg/lambda/rename.go @@ -1,28 +1,31 @@ package lambda +import "fmt" + // Rename replaces all occurrences of the target variable name with the new name. -func (e Variable) Rename(target string, newName string) Expression { - if e.Name == target { - return Variable{Name: newName} +func Rename(e Expression, target string, newName string) Expression { + switch e := e.(type) { + case Variable: + if e.Name == target { + return Variable{Name: newName} + } + + return e + case Abstraction: + newParam := e.Parameter + if e.Parameter == target { + newParam = newName + } + + newBody := Rename(e.Body, target, newName) + + return Abstraction{Parameter: newParam, Body: newBody} + case Application: + newAbs := Rename(e.Abstraction, target, newName) + newArg := Rename(e.Argument, target, newName) + + return Application{Abstraction: newAbs, Argument: newArg} + default: + panic(fmt.Errorf("unknown expression type: %v", e)) } - - return e -} - -func (e Abstraction) Rename(target string, newName string) Expression { - newParam := e.Parameter - if e.Parameter == target { - newParam = newName - } - - newBody := e.Body.Rename(target, newName) - - return Abstraction{Parameter: newParam, Body: newBody} -} - -func (e Application) Rename(target string, newName string) Expression { - newAbs := e.Abstraction.Rename(target, newName) - newArg := e.Argument.Rename(target, newName) - - return Application{Abstraction: newAbs, Argument: newArg} } diff --git a/pkg/lambda/stringify.go b/pkg/lambda/stringify.go index a83ff48..6baaef0 100644 --- a/pkg/lambda/stringify.go +++ b/pkg/lambda/stringify.go @@ -1,13 +1,17 @@ package lambda -func (a Abstraction) String() string { - return "\\" + a.Parameter + "." + a.Body.String() -} +import "fmt" -func (a Application) String() string { - return "(" + a.Abstraction.String() + " " + a.Argument.String() + ")" -} - -func (v Variable) String() string { - return v.Name +// Stringify turns an expression as a string. +func Stringify(e Expression) string { + switch e := e.(type) { + case Variable: + return e.Name + case Abstraction: + return "\\" + e.Parameter + "." + Stringify(e.Body) + case Application: + return "(" + Stringify(e.Abstraction) + " " + Stringify(e.Argument) + ")" + default: + panic(fmt.Errorf("unknown expression type: %v", e)) + } } diff --git a/pkg/lambda/substitute.go b/pkg/lambda/substitute.go index 238b77b..8627edf 100644 --- a/pkg/lambda/substitute.go +++ b/pkg/lambda/substitute.go @@ -1,35 +1,41 @@ package lambda -func (e Variable) Substitute(target string, replacement Expression) Expression { - if e.Name == target { - return replacement - } +import "fmt" - return e -} +// Substitute replaces all free occurrences of the target variable with the +// replacement expression. Alpha-renaming is performed automatically to +// avoid variable capture. +func Substitute(e Expression, target string, replacement Expression) Expression { + switch e := e.(type) { + case Variable: + if e.Name == target { + return replacement + } -func (e Abstraction) Substitute(target string, replacement Expression) Expression { - if e.Parameter == target { return e + case Abstraction: + if e.Parameter == target { + return e + } + + body := e.Body + param := e.Parameter + if IsFree(replacement, param) { + freeVars := GetFree(replacement) + freeVars.Merge(GetFree(body)) + freshVar := GenerateFreshName(freeVars) + body = Rename(body, param, freshVar) + param = freshVar + } + + newBody := Substitute(body, target, replacement) + return Abstraction{Parameter: param, Body: newBody} + case Application: + abs := Substitute(e.Abstraction, target, replacement) + arg := Substitute(e.Argument, target, replacement) + + return Application{Abstraction: abs, Argument: arg} + default: + panic(fmt.Errorf("unknown expression type: %v", e)) } - - body := e.Body - param := e.Parameter - if replacement.IsFree(param) { - freeVars := replacement.GetFree() - freeVars.Merge(body.GetFree()) - freshVar := GenerateFreshName(freeVars) - body = body.Rename(param, freshVar) - param = freshVar - } - - newBody := body.Substitute(target, replacement) - return Abstraction{Parameter: param, Body: newBody} -} - -func (e Application) Substitute(target string, replacement Expression) Expression { - abs := e.Abstraction.Substitute(target, replacement) - arg := e.Argument.Substitute(target, replacement) - - return Application{Abstraction: abs, Argument: arg} }