diff --git a/F#/LambdaInterpreter.Test/LambdaInterpreter.Test.fsproj b/F#/LambdaInterpreter.Test/LambdaInterpreter.Test.fsproj new file mode 100644 index 0000000..2ef4927 --- /dev/null +++ b/F#/LambdaInterpreter.Test/LambdaInterpreter.Test.fsproj @@ -0,0 +1,29 @@ + + + + net8.0 + + false + true + true + + + + + + + + + + + + + + + + + + + + + diff --git a/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs b/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs new file mode 100644 index 0000000..04ec0f5 --- /dev/null +++ b/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs @@ -0,0 +1,46 @@ +module LambdaInterpreter.Test + +open NUnit.Framework +open FsUnit + +let S = Abstr("x", Abstr("y", Abstr("z", App(App(Var("x"), Var("z")), App(Var("y"), Var("z")))))) +let K = Abstr("x", Abstr("y", Var("x"))) +let KStar = Abstr("y", Abstr("x", Var("x"))) +let Ix = Abstr("x", Var("x")) +let Iz = Abstr("z", Var("z")) + +[] +let getAllNamesTest () = + App(Abstr("a", Abstr("x", App(Var("a"), Var("x")))), Var("b")) |> getAllNames |> should equal (Set.ofList [ "a"; "x"; "b"]) + +[] +let getNameTest () = + App(Abstr("a", Abstr("b", App(App(Var("a"), Var("b1")), Var("b")))), Var("b")) |> generateName "b" |> should equal "b2" + +[] +let alphaTest () = + Abstr("b", App(Var("a"), Var("b"))) |> alphaTransform |> should equal (Abstr("b1", App(Var("a"), Var("b1")))) + +[] +let betaTest () = + App(Abstr("a", Abstr("b", App(App(Var("a"), Var("b1")), Var("b")))), Var("b")) |> betaTransform |> should equal (Abstr("b2", App(App(Var("b"), Var("b1")), Var("b2")))) + +[] +let varNormalizeTest () = + Var("a") |> normalize |> should equal (Var("a")) + +[] +let INormalizeTest () = + Ix |> normalize |> should equal Ix + +[] +let renameNormalizeTest () = + App(Abstr("a", Abstr("b", App(Var("a"),Var("b")))), Var("b")) |> normalize |> should equal (Abstr("b1", App(Var("b"),Var("b1")))) + +[] +let KIKStarTest () = + App(K, Ix) |> normalize |> should equal KStar + +[] +let SkkTest () = + App(App(S, K), K) |> normalize |> should equal Iz diff --git a/F#/LambdaInterpreter/LambdaInterpreter.fs b/F#/LambdaInterpreter/LambdaInterpreter.fs new file mode 100644 index 0000000..60086d3 --- /dev/null +++ b/F#/LambdaInterpreter/LambdaInterpreter.fs @@ -0,0 +1,120 @@ +module LambdaInterpreter + +/// +/// Represents lamda term +/// +type LambdaTerm = + | Var of string + | App of LambdaTerm * LambdaTerm + | Abstr of string * LambdaTerm + +/// +/// Recursively maps given function to the lamda term, skipping recursive mapping, when needed +/// +/// The function to produce a new term from the given one, and the condition of whether recursion inside current term should be skipped +/// Term to map +/// Mapped term +let rec mapTerm mapping term = + let (mappedTerm, skip) = mapping term + if not skip then + match mappedTerm with + | Var _ -> mappedTerm + | App(lhs, rhs) -> App(mapTerm mapping lhs, mapTerm mapping rhs) + | Abstr (param, rhs) -> Abstr(param, mapTerm mapping rhs) + else + mappedTerm + +/// +/// Applies function to each term recursively threading an accumulator argument through computation +/// +/// Function to update accumulator based on term value +/// The initial state +/// Term to fold +/// Mapped term +let bfsFoldTerm fold acc term = + let rec bfsFoldHelper fold acc queue = + match queue with + | [] -> acc + | Var(var)::tail -> + bfsFoldHelper fold (fold (Var(var)) acc) tail + | App(lhs, rhs)::tail -> + bfsFoldHelper fold (fold (App(lhs, rhs)) acc) (tail @ [ lhs; rhs ]) + | Abstr(param, rhs)::tail -> + bfsFoldHelper fold (fold (Abstr(param, rhs)) acc) (tail @ [ rhs ]) + bfsFoldHelper fold acc [ term ] + +/// +/// Returns set of all variable names in term +/// +/// Term to search names from +/// Set of names +let getAllNames mainTerm = + let fold term acc = + match term with + | Var v -> Set.add v acc + | Abstr(param, _) -> Set.add param acc + | _ -> acc + bfsFoldTerm fold Set.empty mainTerm + +/// +/// Generates new variable name based on give one, which doesnt interrupt with given term +/// +/// Name to base new one from +/// Term to search names from +/// New name +let generateName oldName mainTerm = + let freeNames = getAllNames mainTerm + let rec generateNameHelper counter = + let newName = oldName + counter.ToString() + if freeNames.Contains(newName) then generateNameHelper (counter + 1) else newName + generateNameHelper 1 + +/// +/// Applies alpha transformation on given term +/// +/// Term to apply transofrmation to +/// Transformed term +let alphaTransform term = + match term with + | Abstr(param, subterm) -> + let newName = generateName param subterm + let mapping mappingTerm = + match mappingTerm with + | Var v when v.Equals(param)-> (Var(newName), false) + | _ -> (mappingTerm, false) + Abstr(newName, mapTerm mapping subterm) + | _ -> term + +/// +/// Applies beta transformation based on normal strategy on given term +/// +/// Term to apply transofrmation to +/// Transformed term +let betaTransform mainTerm = + let reduceMatch term acc = + match (term, acc) with + | (App(Abstr(_,_), _), None) -> Some(term) + | _ -> acc + let reduceTerm = bfsFoldTerm reduceMatch None mainTerm + match reduceTerm with + | None -> mainTerm + | Some(App(Abstr(param, abstrTerm), appTerm)) -> + let allNames = getAllNames appTerm + let reduceMapping term = + match term with + | Var v when v.Equals(param) -> (appTerm, true) + | Abstr(p, _) when allNames.Contains(p) -> (alphaTransform term, false) + | _ -> (term, false) + + let reducedTerm = mapTerm reduceMapping abstrTerm + mapTerm (fun x -> if x = reduceTerm.Value then (reducedTerm, true) else (x, false)) mainTerm + | _ -> mainTerm + +/// +/// Normalizes term if possible based on normal reduction strategy +/// +/// Term to normalize +/// Transformed term +let rec normalize term = + let reduced = betaTransform term + if term = reduced then term else normalize reduced diff --git a/F#/LambdaInterpreter/LambdaInterpreter.fsproj b/F#/LambdaInterpreter/LambdaInterpreter.fsproj new file mode 100644 index 0000000..006fc20 --- /dev/null +++ b/F#/LambdaInterpreter/LambdaInterpreter.fsproj @@ -0,0 +1,12 @@ + + + + net8.0 + true + + + + + + + diff --git a/F#/forSpbu.sln b/F#/forSpbu.sln index 9d54d03..37f29b5 100644 --- a/F#/forSpbu.sln +++ b/F#/forSpbu.sln @@ -17,10 +17,12 @@ Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "PriorityQueue", "PriorityQu EndProject Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "PriorityQueue.Test", "PriorityQueue.Test\PriorityQueue.Test.fsproj", "{89A935E8-B5F3-435D-ACC3-A99DD7C66178}" EndProject -Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "07.03", "07.03", "{5CA9053B-DE9B-4824-9F19-AEB464E3B9D8}" -EndProject Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Homework1", "Homework1\Homework1.fsproj", "{04B15EE4-079A-42ED-ACC8-E2DCD25281C6}" EndProject +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "LambdaInterpreter", "LambdaInterpreter\LambdaInterpreter.fsproj", "{E83E0AE3-A385-497B-9F64-A9FD42A33D8E}" +EndProject +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "LambdaInterpreter.Test", "LambdaInterpreter.Test\LambdaInterpreter.Test.fsproj", "{C2A83553-3EDE-4BA1-B185-9339BC42C2E0}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|Any CPU = Debug|Any CPU @@ -58,6 +60,14 @@ Global {89A935E8-B5F3-435D-ACC3-A99DD7C66178}.Debug|Any CPU.Build.0 = Debug|Any CPU {89A935E8-B5F3-435D-ACC3-A99DD7C66178}.Release|Any CPU.ActiveCfg = Release|Any CPU {89A935E8-B5F3-435D-ACC3-A99DD7C66178}.Release|Any CPU.Build.0 = Release|Any CPU + {E83E0AE3-A385-497B-9F64-A9FD42A33D8E}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {E83E0AE3-A385-497B-9F64-A9FD42A33D8E}.Debug|Any CPU.Build.0 = Debug|Any CPU + {E83E0AE3-A385-497B-9F64-A9FD42A33D8E}.Release|Any CPU.ActiveCfg = Release|Any CPU + {E83E0AE3-A385-497B-9F64-A9FD42A33D8E}.Release|Any CPU.Build.0 = Release|Any CPU + {C2A83553-3EDE-4BA1-B185-9339BC42C2E0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {C2A83553-3EDE-4BA1-B185-9339BC42C2E0}.Debug|Any CPU.Build.0 = Debug|Any CPU + {C2A83553-3EDE-4BA1-B185-9339BC42C2E0}.Release|Any CPU.ActiveCfg = Release|Any CPU + {C2A83553-3EDE-4BA1-B185-9339BC42C2E0}.Release|Any CPU.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(NestedProjects) = preSolution {7937CDA8-8285-4E23-AD1A-FC0F04FEEFE6} = {91E3BDA2-0836-46C2-95F0-02513FD7F13F} diff --git a/F#/forSpbu.sln.DotSettings.user b/F#/forSpbu.sln.DotSettings.user deleted file mode 100644 index dab14af..0000000 --- a/F#/forSpbu.sln.DotSettings.user +++ /dev/null @@ -1,6 +0,0 @@ - - <SessionState ContinuousTestingMode="0" IsActive="True" Name="Test" xmlns="urn:schemas-jetbrains-com:jetbrains-ut-session"> - <TestAncestor> - <TestId>NUnit3x::89A935E8-B5F3-435D-ACC3-A99DD7C66178::net8.0::PriorityQueue.Test</TestId> - </TestAncestor> -</SessionState> \ No newline at end of file