Skip to content

Commit

Permalink
Merge pull request #3 from kazbekovruslan/Homework3
Browse files Browse the repository at this point in the history
Homework3
  • Loading branch information
kazbekovruslan authored Jun 1, 2024
2 parents b3849f8 + f46cb57 commit e358ebf
Show file tree
Hide file tree
Showing 8 changed files with 177 additions and 0 deletions.
30 changes: 30 additions & 0 deletions Homework3/Homework3.Tests/Homework3.Tests.fsproj
Original file line number Diff line number Diff line change
@@ -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>
4 changes: 4 additions & 0 deletions Homework3/Homework3.Tests/Program.fs
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
module Program =

[<EntryPoint>]
let main _ = 0
24 changes: 24 additions & 0 deletions Homework3/Homework3.Tests/UnitTest1.fs
Original file line number Diff line number Diff line change
@@ -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
28 changes: 28 additions & 0 deletions Homework3/Homework3.sln
Original file line number Diff line number Diff line change
@@ -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
12 changes: 12 additions & 0 deletions Homework3/Homework3/Homework3.fsproj
Original file line number Diff line number Diff line change
@@ -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>
41 changes: 41 additions & 0 deletions Homework3/Homework3/LambdaInterpreter.fs
Original file line number Diff line number Diff line change
@@ -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)
Binary file added Homework3/task1and2.pdf
Binary file not shown.
38 changes: 38 additions & 0 deletions Homework3/task1and2.tex
Original file line number Diff line number Diff line change
@@ -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}

0 comments on commit e358ebf

Please sign in to comment.