From bd8ac2c5280ad074233543bc981e49bb0ea51436 Mon Sep 17 00:00:00 2001 From: IgnatSergeev Date: Thu, 30 May 2024 19:46:03 +0300 Subject: [PATCH 1/4] Added realisation --- .../LambdaInterpreter.Test.fsproj | 29 ++++++++ .../LambdaInterpreterTest.fs | 29 ++++++++ F#/LambdaInterpreter/LambdaInterpreter.fs | 72 +++++++++++++++++++ F#/LambdaInterpreter/LambdaInterpreter.fsproj | 12 ++++ F#/forSpbu.sln | 14 +++- F#/forSpbu.sln.DotSettings.user | 6 -- 6 files changed, 154 insertions(+), 8 deletions(-) create mode 100644 F#/LambdaInterpreter.Test/LambdaInterpreter.Test.fsproj create mode 100644 F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs create mode 100644 F#/LambdaInterpreter/LambdaInterpreter.fs create mode 100644 F#/LambdaInterpreter/LambdaInterpreter.fsproj delete mode 100644 F#/forSpbu.sln.DotSettings.user 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..22f96ac --- /dev/null +++ b/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs @@ -0,0 +1,29 @@ +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 I = Abstr("x", Var("x")) + +[] +let VarTest () = + Var("a") |> normalize |> should equal (Var("a")) + +[] +let AbstrTest () = + I |> normalize |> should equal I + +[] +let KIKStarTest () = + App(K, I) |> normalize |> should equal KStar + +[] +let SKKTest () = + App(App(S, K), K) |> normalize |> should equal I + +[] +let RenameTest () = + App(Abstr("a", Abstr("b", App(Var("a"),Var("b")))), Var("b")) |> normalize |> should equal I diff --git a/F#/LambdaInterpreter/LambdaInterpreter.fs b/F#/LambdaInterpreter/LambdaInterpreter.fs new file mode 100644 index 0000000..029ad24 --- /dev/null +++ b/F#/LambdaInterpreter/LambdaInterpreter.fs @@ -0,0 +1,72 @@ +module LambdaInterpreter + +type LambdaTerm = + | Var of string + | App of LambdaTerm * LambdaTerm + | Abstr of string * LambdaTerm + +let rec mapTerm mapping term = + match term with + | Var _ -> mapping term + | App (lhs, rhs) -> mapping (App(mapTerm mapping lhs, mapTerm mapping rhs)) + | Abstr (param, rhs) -> mapping (Abstr(param, mapTerm mapping rhs)) + +let bfsFoldTerm fold acc term = + let rec bfsFoldHelper fold acc queue = + match queue with + | [] -> acc + | Var(var)::tail -> + bfsFoldHelper fold acc tail |> fold (Var(var)) + | App(lhs, rhs)::tail -> + bfsFoldHelper fold acc (tail @ [ lhs; rhs ]) |> fold (App(lhs, rhs)) + | Abstr(param, rhs)::tail -> + bfsFoldHelper fold acc (tail @ [ rhs ]) |> fold (Abstr(param, rhs)) + bfsFoldHelper fold acc [ term ] + +let generateName oldName mainTerm = + let fold term acc = + match term with + | Var v -> Set.add v acc + | Abstr(param, _) -> Set.remove param acc + | _ -> acc + let freeNames = bfsFoldTerm fold Set.empty mainTerm + let rec generateNameHelper counter = + let newName = oldName + counter.ToString() + if freeNames.Contains(newName) then generateNameHelper (counter + 1) else newName + + generateNameHelper 1 + +let alphaTransform term = + match term with + | Abstr(param, subterm) -> + let newName = generateName param subterm + let mapping mappingTerm = + match mappingTerm with + | Var v -> if v.Equals(param) then Var(newName) else term + | _ -> term + + mapTerm mapping term + | _ -> term + +let betaReduce 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 reduceMapping term = + match term with + | Var v when v.Equals(param) -> appTerm + | Abstr(p, _) when p.Equals(param) -> alphaTransform term + | _ -> term + + let reducedTerm = mapTerm reduceMapping abstrTerm + mapTerm (fun x -> if x = reduceTerm.Value then reducedTerm else x) mainTerm + | _ -> mainTerm + +let rec normalize term = + let reduced = betaReduce term + if term = reduced then term else betaReduce 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 From b7e54125e5be4f90e1360a82fda51a40de6d54e1 Mon Sep 17 00:00:00 2001 From: IgnatSergeev Date: Fri, 31 May 2024 15:59:27 +0300 Subject: [PATCH 2/4] Added comments and tests --- .../LambdaInterpreterTest.fs | 32 ++++--- F#/LambdaInterpreter/LambdaInterpreter.fs | 86 +++++++++++++++---- 2 files changed, 89 insertions(+), 29 deletions(-) diff --git a/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs b/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs index 22f96ac..7be72ae 100644 --- a/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs +++ b/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs @@ -9,21 +9,33 @@ let KStar = Abstr("y", Abstr("x", Var("x"))) let I = Abstr("x", Var("x")) [] -let VarTest () = - Var("a") |> normalize |> should equal (Var("a")) +let getAllNamesTest () = + App(Abstr("a", Abstr("x", App(Var("a"), Var("x")))), Var("b")) |> getAllNames |> should equal (Set.ofList [ "a"; "x"; "b"]) [] -let AbstrTest () = - I |> normalize |> should equal I +let getNameTest () = + App(Abstr("a", Abstr("b", App(App(Var("a"), Var("b1")), Var("b")))), Var("b")) |> generateName "b" |> should equal "b2" [] -let KIKStarTest () = - App(K, I) |> normalize |> should equal KStar +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")) |> betaReduce |> should equal (Abstr("b2", App(App(Var("b"), Var("b1")), Var("b2")))) + +[] +let varNormalizeTest () = + Var("a") |> normalize |> should equal (Var("a")) [] -let SKKTest () = - App(App(S, K), K) |> normalize |> should equal I +let INormalizeTest () = + I |> normalize |> should equal I [] -let RenameTest () = - App(Abstr("a", Abstr("b", App(Var("a"),Var("b")))), Var("b")) |> normalize |> should equal I +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, I) |> normalize |> should equal KStar diff --git a/F#/LambdaInterpreter/LambdaInterpreter.fs b/F#/LambdaInterpreter/LambdaInterpreter.fs index 029ad24..4f2b13f 100644 --- a/F#/LambdaInterpreter/LambdaInterpreter.fs +++ b/F#/LambdaInterpreter/LambdaInterpreter.fs @@ -1,16 +1,36 @@ 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 = - match term with - | Var _ -> mapping term - | App (lhs, rhs) -> mapping (App(mapTerm mapping lhs, mapTerm mapping rhs)) - | Abstr (param, rhs) -> mapping (Abstr(param, mapTerm mapping rhs)) + 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 @@ -23,32 +43,54 @@ let bfsFoldTerm fold acc term = bfsFoldHelper fold acc (tail @ [ rhs ]) |> fold (Abstr(param, rhs)) bfsFoldHelper fold acc [ term ] -let generateName oldName mainTerm = +/// +/// 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.remove param acc + | Abstr(param, _) -> Set.add param acc | _ -> acc - let freeNames = bfsFoldTerm fold Set.empty mainTerm + 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 -> if v.Equals(param) then Var(newName) else term - | _ -> term - - mapTerm mapping term + | Var v when v.Equals(param)-> (Var(newName), false) + | _ -> (mappingTerm, false) + Abstr(newName, mapTerm mapping subterm) | _ -> term -let betaReduce mainTerm = +/// +/// 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) @@ -57,16 +99,22 @@ let betaReduce 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 - | Abstr(p, _) when p.Equals(param) -> alphaTransform term - | _ -> term + | 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 else x) mainTerm + 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 = betaReduce term - if term = reduced then term else betaReduce reduced + let reduced = betaTransform term + if term = reduced then term else betaTransform reduced From 1f7ff0b115f88361516b7e93cd6ffce0fe2f35a5 Mon Sep 17 00:00:00 2001 From: IgnatSergeev Date: Fri, 31 May 2024 16:01:26 +0300 Subject: [PATCH 3/4] Fixed tests --- F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs b/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs index 7be72ae..526f05a 100644 --- a/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs +++ b/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs @@ -22,7 +22,7 @@ let alphaTest () = [] let betaTest () = - App(Abstr("a", Abstr("b", App(App(Var("a"), Var("b1")), Var("b")))), Var("b")) |> betaReduce |> should equal (Abstr("b2", App(App(Var("b"), Var("b1")), Var("b2")))) + 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 () = From 70ee270004982f93ae74e5298e4849d441c41000 Mon Sep 17 00:00:00 2001 From: "ignat.sergeev" Date: Sat, 1 Jun 2024 12:54:15 +0300 Subject: [PATCH 4/4] Fixed SKK --- F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs | 11 ++++++++--- F#/LambdaInterpreter/LambdaInterpreter.fs | 8 ++++---- 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs b/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs index 526f05a..04ec0f5 100644 --- a/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs +++ b/F#/LambdaInterpreter.Test/LambdaInterpreterTest.fs @@ -6,7 +6,8 @@ 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 I = Abstr("x", Var("x")) +let Ix = Abstr("x", Var("x")) +let Iz = Abstr("z", Var("z")) [] let getAllNamesTest () = @@ -30,7 +31,7 @@ let varNormalizeTest () = [] let INormalizeTest () = - I |> normalize |> should equal I + Ix |> normalize |> should equal Ix [] let renameNormalizeTest () = @@ -38,4 +39,8 @@ let renameNormalizeTest () = [] let KIKStarTest () = - App(K, I) |> normalize |> should equal KStar + 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 index 4f2b13f..60086d3 100644 --- a/F#/LambdaInterpreter/LambdaInterpreter.fs +++ b/F#/LambdaInterpreter/LambdaInterpreter.fs @@ -36,11 +36,11 @@ let bfsFoldTerm fold acc term = match queue with | [] -> acc | Var(var)::tail -> - bfsFoldHelper fold acc tail |> fold (Var(var)) + bfsFoldHelper fold (fold (Var(var)) acc) tail | App(lhs, rhs)::tail -> - bfsFoldHelper fold acc (tail @ [ lhs; rhs ]) |> fold (App(lhs, rhs)) + bfsFoldHelper fold (fold (App(lhs, rhs)) acc) (tail @ [ lhs; rhs ]) | Abstr(param, rhs)::tail -> - bfsFoldHelper fold acc (tail @ [ rhs ]) |> fold (Abstr(param, rhs)) + bfsFoldHelper fold (fold (Abstr(param, rhs)) acc) (tail @ [ rhs ]) bfsFoldHelper fold acc [ term ] /// @@ -117,4 +117,4 @@ let betaTransform mainTerm = /// Transformed term let rec normalize term = let reduced = betaTransform term - if term = reduced then term else betaTransform reduced + if term = reduced then term else normalize reduced