diff --git a/Homework3/Homework3.Tests/Homework3.Tests.fsproj b/Homework3/Homework3.Tests/Homework3.Tests.fsproj new file mode 100644 index 0000000..9d248e4 --- /dev/null +++ b/Homework3/Homework3.Tests/Homework3.Tests.fsproj @@ -0,0 +1,30 @@ + + + + net8.0 + + false + false + true + + + + + + + + + + + + + + + + + + + + + + diff --git a/Homework3/Homework3.Tests/Program.fs b/Homework3/Homework3.Tests/Program.fs new file mode 100644 index 0000000..e5bfa1b --- /dev/null +++ b/Homework3/Homework3.Tests/Program.fs @@ -0,0 +1,4 @@ +module Program = + + [] + let main _ = 0 diff --git a/Homework3/Homework3.Tests/UnitTest1.fs b/Homework3/Homework3.Tests/UnitTest1.fs new file mode 100644 index 0000000..5bf7677 --- /dev/null +++ b/Homework3/Homework3.Tests/UnitTest1.fs @@ -0,0 +1,24 @@ +module Homework3.Tests + +open NUnit.Framework +open FsUnit +open Homework3.LambdaInterpreter + +let testCases () = + [ Var "x", Var "x" + Application((LambdaAbstraction("x", Var "x"), Var "z")), Var "z" + LambdaAbstraction("x", Var "a"), LambdaAbstraction("x", Var "a") + Application( + LambdaAbstraction("x", Var "y"), + Application( + LambdaAbstraction("x", LambdaAbstraction("x", Var "x")), + LambdaAbstraction("x", Application(Var "x", Var "x")) + ) + ), + Var "y" ] + |> List.map (fun (expression, result) -> TestCaseData(expression, result)) + + +[] +let reduceTests expression expected = + reduce expression |> should equal expected diff --git a/Homework3/Homework3.sln b/Homework3/Homework3.sln new file mode 100644 index 0000000..de421fb --- /dev/null +++ b/Homework3/Homework3.sln @@ -0,0 +1,28 @@ + +Microsoft Visual Studio Solution File, Format Version 12.00 +# Visual Studio Version 17 +VisualStudioVersion = 17.0.31903.59 +MinimumVisualStudioVersion = 10.0.40219.1 +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Homework3", "Homework3\Homework3.fsproj", "{A028FB7A-9B06-4781-9985-0AA7A0B9C68E}" +EndProject +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Homework3.Tests", "Homework3.Tests\Homework3.Tests.fsproj", "{D41BFD88-A6C5-4065-B518-C1DC2DBCFD2D}" +EndProject +Global + GlobalSection(SolutionConfigurationPlatforms) = preSolution + Debug|Any CPU = Debug|Any CPU + Release|Any CPU = Release|Any CPU + EndGlobalSection + GlobalSection(SolutionProperties) = preSolution + HideSolutionNode = FALSE + EndGlobalSection + GlobalSection(ProjectConfigurationPlatforms) = postSolution + {A028FB7A-9B06-4781-9985-0AA7A0B9C68E}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {A028FB7A-9B06-4781-9985-0AA7A0B9C68E}.Debug|Any CPU.Build.0 = Debug|Any CPU + {A028FB7A-9B06-4781-9985-0AA7A0B9C68E}.Release|Any CPU.ActiveCfg = Release|Any CPU + {A028FB7A-9B06-4781-9985-0AA7A0B9C68E}.Release|Any CPU.Build.0 = Release|Any CPU + {D41BFD88-A6C5-4065-B518-C1DC2DBCFD2D}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {D41BFD88-A6C5-4065-B518-C1DC2DBCFD2D}.Debug|Any CPU.Build.0 = Debug|Any CPU + {D41BFD88-A6C5-4065-B518-C1DC2DBCFD2D}.Release|Any CPU.ActiveCfg = Release|Any CPU + {D41BFD88-A6C5-4065-B518-C1DC2DBCFD2D}.Release|Any CPU.Build.0 = Release|Any CPU + EndGlobalSection +EndGlobal diff --git a/Homework3/Homework3/Homework3.fsproj b/Homework3/Homework3/Homework3.fsproj new file mode 100644 index 0000000..996c09f --- /dev/null +++ b/Homework3/Homework3/Homework3.fsproj @@ -0,0 +1,12 @@ + + + + Library + net8.0 + + + + + + + diff --git a/Homework3/Homework3/LambdaInterpreter.fs b/Homework3/Homework3/LambdaInterpreter.fs new file mode 100644 index 0000000..c5243b5 --- /dev/null +++ b/Homework3/Homework3/LambdaInterpreter.fs @@ -0,0 +1,41 @@ +module Homework3.LambdaInterpreter + +type LambdaTerm = + | Var of string + | Application of LambdaTerm * LambdaTerm + | LambdaAbstraction of string * LambdaTerm + +let rec getFV term = + match term with + | Var x -> Set.singleton (x) + | Application(term1, term2) -> Set.union (getFV term1) (getFV term2) + | LambdaAbstraction(x, term) -> getFV term |> Set.remove x + +let isFV var term = getFV (term) |> Set.contains var + +let rec renameVar usedVars = + let rec changeVar v = + if Set.contains v usedVars then changeVar v + "'" else v + + changeVar "x" + +let rec substitute var term substTerm = + match term with + | Var x when x = var -> substTerm + | Var _ -> term + | Application(term1, term2) -> Application(substitute var term1 substTerm, substitute var term2 substTerm) + | LambdaAbstraction(x, _) when x = var -> term + | LambdaAbstraction(x, t) when isFV x substTerm |> not || isFV var t |> not -> + LambdaAbstraction(x, substitute var t substTerm) + | LambdaAbstraction(x, t) -> + let newVar = Set.union (getFV t) (getFV substTerm) |> renameVar + LambdaAbstraction(newVar, substitute var (substitute x t (Var(newVar))) substTerm) + +let rec reduce term = + match term with + | Var x -> term + | LambdaAbstraction(var, t) -> LambdaAbstraction(var, reduce t) + | Application(term1, term2) -> + match term1 with + | LambdaAbstraction(var, t) -> substitute var t term2 + | _ -> Application(reduce term1, reduce term2) diff --git a/Homework3/task1and2.pdf b/Homework3/task1and2.pdf new file mode 100644 index 0000000..445734d Binary files /dev/null and b/Homework3/task1and2.pdf differ diff --git a/Homework3/task1and2.tex b/Homework3/task1and2.tex new file mode 100644 index 0000000..daf25ae --- /dev/null +++ b/Homework3/task1and2.tex @@ -0,0 +1,38 @@ +\documentclass{article} + +\usepackage{amsmath} +\usepackage[T2A]{fontenc} +\usepackage[russian]{babel} + +\begin{document} + +\section{Normalization} + +\begin{align*} +& ((\lambda a. (\lambda b. b\ b)\ (\lambda b. b\ b))\ b)\ ((\lambda c. (c\ b)) (\lambda a. a)) +\rightarrow_\beta +((\lambda b. b\ b)\ (\lambda b. b\ b))\ ((\lambda c. (c\ b)) (\lambda a. a)) +\rightarrow_\beta \\ +&((\lambda b. b\ b)\ (\lambda b. b\ b))\ ((\lambda c. (c\ b)) (\lambda a. a)) +\end{align*} + +Нормальная стратегия не сработала $\Rightarrow$ +по теореме о нормализации (Карри) не приводится к нормальной форме. + +\section{S K K = I} + +\begin{align*} +& S\ K\ K = (\lambda x\ y\ z.x\ z\ (y\ z))\ (\lambda x\ y. x)\ (\lambda x\ y. x) +\rightarrow_\beta +(\lambda y\ z.(\lambda x\ y.x)\ z\ (y\ z))\ (\lambda x\ y. x) +\rightarrow_\beta \\ +&(\lambda z.(\lambda x\ y.x)\ z\ ((\lambda x\ y.x)\ z)) +\rightarrow_\beta +(\lambda z.(\lambda y.z)\ ((\lambda x\ y.x)\ z)) +\rightarrow_\beta +(\lambda z.(\lambda y.z)\ (\lambda y.z)) +\rightarrow_\beta \\ +&(\lambda z.z) = I +\end{align*} + +\end{document}