diff --git a/LambdaInterpreter/LambdaInterpreter.Test/LambdaInterpreter.Test.fsproj b/LambdaInterpreter/LambdaInterpreter.Test/LambdaInterpreter.Test.fsproj new file mode 100644 index 0000000..71e94cd --- /dev/null +++ b/LambdaInterpreter/LambdaInterpreter.Test/LambdaInterpreter.Test.fsproj @@ -0,0 +1,26 @@ + + + + net6.0 + + false + false + + + + + + + + + + + + + + + + + + + diff --git a/LambdaInterpreter/LambdaInterpreter.Test/LambdaInterpreterTest1.fs b/LambdaInterpreter/LambdaInterpreter.Test/LambdaInterpreterTest1.fs new file mode 100644 index 0000000..0bfad9e --- /dev/null +++ b/LambdaInterpreter/LambdaInterpreter.Test/LambdaInterpreterTest1.fs @@ -0,0 +1,29 @@ +module LambdaInterpreter.Test + +open NUnit.Framework +open FsUnit +open Program + +[] +let TestAppWithVarTerm () = + let term = Term.Application(LambdaAbstraction("y", Variable("y")), Variable("z")) + + let result = betaReduction term + + result |> should equal (Variable("z")) + +[] +let TestAppWithTwoTerm () = + let term = Term.Application(LambdaAbstraction("y", Variable("y")), LambdaAbstraction("z", Variable("z"))) + + let result = term |> betaReduction + + result |> should equal (LambdaAbstraction("z", Variable("z"))) + +[] +let TestLambdaAbs () = + let term = Term.LambdaAbstraction("x", LambdaAbstraction("z", Variable("z"))) + + let result = term |> betaReduction + + result |> should equal (LambdaAbstraction("x", LambdaAbstraction("z", Variable("z")))) \ No newline at end of file diff --git a/LambdaInterpreter/LambdaInterpreter.sln b/LambdaInterpreter/LambdaInterpreter.sln new file mode 100644 index 0000000..07c0101 --- /dev/null +++ b/LambdaInterpreter/LambdaInterpreter.sln @@ -0,0 +1,22 @@ + +Microsoft Visual Studio Solution File, Format Version 12.00 +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "LambdaInterpreter", "LambdaInterpreter\LambdaInterpreter.fsproj", "{81D87A95-7386-4009-9E71-1E58B5966D23}" +EndProject +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "LambdaInterpreter.Test", "LambdaInterpreter.Test\LambdaInterpreter.Test.fsproj", "{0D2BE233-2834-448C-A50E-4644123FA525}" +EndProject +Global + GlobalSection(SolutionConfigurationPlatforms) = preSolution + Debug|Any CPU = Debug|Any CPU + Release|Any CPU = Release|Any CPU + EndGlobalSection + GlobalSection(ProjectConfigurationPlatforms) = postSolution + {81D87A95-7386-4009-9E71-1E58B5966D23}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {81D87A95-7386-4009-9E71-1E58B5966D23}.Debug|Any CPU.Build.0 = Debug|Any CPU + {81D87A95-7386-4009-9E71-1E58B5966D23}.Release|Any CPU.ActiveCfg = Release|Any CPU + {81D87A95-7386-4009-9E71-1E58B5966D23}.Release|Any CPU.Build.0 = Release|Any CPU + {0D2BE233-2834-448C-A50E-4644123FA525}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {0D2BE233-2834-448C-A50E-4644123FA525}.Debug|Any CPU.Build.0 = Debug|Any CPU + {0D2BE233-2834-448C-A50E-4644123FA525}.Release|Any CPU.ActiveCfg = Release|Any CPU + {0D2BE233-2834-448C-A50E-4644123FA525}.Release|Any CPU.Build.0 = Release|Any CPU + EndGlobalSection +EndGlobal diff --git a/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj new file mode 100644 index 0000000..761405f --- /dev/null +++ b/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -0,0 +1,13 @@ + + + + Exe + net6.0 + Windows + + + + + + + diff --git a/LambdaInterpreter/LambdaInterpreter/Program.fs b/LambdaInterpreter/LambdaInterpreter/Program.fs new file mode 100644 index 0000000..91dee12 --- /dev/null +++ b/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -0,0 +1,39 @@ +open System +open System.Collections.Generic +open System.Security.Principal + +type Term = + | Variable of string + | Application of Term * Term + | LambdaAbstraction of string * Term + +let getVar term = + let rec execute term list = + match term with + | Variable(v) -> v :: list + | Application(term1, term2) -> List.append (execute term1 list) (execute term2 list) + | LambdaAbstraction(v, term1) -> execute term1 (List.filter(fun x -> x <> v) list) + execute term [] +let checkFreeVar var term = term |> getVar |> List.exists(fun x -> x = var) + +let rec substitution var termOut termIn = + match termOut with + | Variable(v) -> if v = var then termIn else Variable(var) + | Application(termApp1, termApp2) -> Application(substitution var termApp1 termIn, substitution var termApp2 termIn) + | LambdaAbstraction(varInAbs, termInAbs) -> + match varInAbs with + | v when var = v -> LambdaAbstraction(varInAbs, termInAbs) + | v when (checkFreeVar varInAbs termIn) || (checkFreeVar var termInAbs) -> LambdaAbstraction(varInAbs, (substitution var termInAbs termIn)) + | _ -> + let newVar = (((getVar termInAbs) @ (getVar termIn)) |> List.toArray |> Array.max) + "1" + let newTerm = newVar |> Variable + let termWithNewVar = substitution var termInAbs newTerm + LambdaAbstraction(newVar, substitution var termWithNewVar termIn ) + + +let rec betaReduction term = + match term with + | Variable(v) -> Variable(v) + | Application(LambdaAbstraction(v, term), termForSubstitution) -> betaReduction (substitution v term termForSubstitution) + | Application(term1, term2) -> Application(betaReduction term1, betaReduction term2) + | LambdaAbstraction(v, term) -> LambdaAbstraction(v, betaReduction term)