Homework3

Homework3/Homework3.Tests/Homework3.Tests.fsproj

@@ -0,0 +1,30 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+  <PropertyGroup>
+    <TargetFramework>net8.0</TargetFramework>
+
+    <IsPackable>false</IsPackable>
+    <GenerateProgramFile>false</GenerateProgramFile>
+    <IsTestProject>true</IsTestProject>
+  </PropertyGroup>
+
+  <ItemGroup>
+    <Compile Include="UnitTest1.fs" />
+    <Compile Include="Program.fs" />
+  </ItemGroup>
+
+  <ItemGroup>
+    <PackageReference Include="FsUnit" Version="6.0.0" />
+    <PackageReference Include="FsCheck" Version="2.16.6" />
+    <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.6.0" />
+    <PackageReference Include="NUnit" Version="4.1.0" />
+    <PackageReference Include="NUnit3TestAdapter" Version="4.5.0" />
+    <PackageReference Include="NUnit.Analyzers" Version="4.0.1" />
+    <PackageReference Include="coverlet.collector" Version="6.0.0" />
+  </ItemGroup>
+
+  <ItemGroup>
+    <ProjectReference Include="..\Homework3\Homework3.fsproj" />
+  </ItemGroup>
+
+</Project>

Homework3/Homework3.Tests/Program.fs

@@ -0,0 +1,4 @@
+module Program =
+
+    [<EntryPoint>]
+    let main _ = 0

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))
+
+
+[<TestCaseSource(nameof (testCases))>]
+let reduceTests expression expected =
+    reduce expression |> should equal expected

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

Homework3/Homework3/Homework3.fsproj

@@ -0,0 +1,12 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+  <PropertyGroup>
+    <OutputType>Library</OutputType>
+    <TargetFramework>net8.0</TargetFramework>
+  </PropertyGroup>
+
+  <ItemGroup>
+    <Compile Include="LambdaInterpreter.fs" />
+  </ItemGroup>
+
+</Project>

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)

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}