Conversation
lambda_calculus.tex
Outdated
| \begin{math}((\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 a. a) \ b) \ \rightarrow_{\beta} ((\lambda b.b \ b) \ (\lambda b.b \ b)) \ b | ||
| \section{SKK} | ||
| \begin{math}((\lambda x\ y\ z.x\ z\ (y\ z))\ (\lambda x\ y . x))\ (\lambda x\ y . x)\ \rightarrow_{\alpha} ((\lambda x\ y\ z.x\ z\ (y\ z))\ (\lambda a\ b . a))\ (\lambda m\ p . m)\ \rightarrow_{\beta} ((\lambda y\ z.(\lambda a \ b.a)\ z\ (y\ z))\ (\lambda m\ p . m)\ \rightarrow_{\beta} \lamda z.(\lambda a \ b.a)\ z \ ((\lamda m\ p. m)\ z)) \ \rightarrow{\beta} \lambda z.z\end{math} | ||
| \end{document} |
There was a problem hiding this comment.
Компилится с ошибками, стоит от них избавиться.
И в SKK чем дальше, тем хуже форматирование: пропали некоторые лямбды, символы betta-редукции увеличиваются. Надо привести в читабельный вид, чтобы каждый новый терм после применения правила оказывался на новой строке
| module Program = | ||
|
|
||
| [<EntryPoint>] | ||
| let main _ = 0 |
There was a problem hiding this comment.
Я предпочитаю это не писать, а делать GenerateProgramFile>true</GenerateProgramFile>
| [<Test>] | ||
| let Test1 () = | ||
| Assert.Pass() | ||
|
|
| <Project Sdk="Microsoft.NET.Sdk"> | ||
|
|
||
| <PropertyGroup> | ||
| <TargetFramework>net7.0</TargetFramework> |
| module Program = | ||
|
|
||
| [<EntryPoint>] | ||
| let main _ = 0 |
| Assert.AreEqual(expected, result) | ||
| [<Test>] |
There was a problem hiding this comment.
| Assert.AreEqual(expected, result) | |
| [<Test>] | |
| Assert.AreEqual(expected, result) | |
| [<Test>] |
И ниже.
| @@ -0,0 +1,63 @@ | |||
| namespace Lambda_Interpreter | |||
|
|
|||
| module lambdaInterpreter = | |||
| | Abstraction of string * LambdaTerm | ||
| | Application of LambdaTerm * LambdaTerm | ||
|
|
||
| type Substitution = (string * LambdaTerm) list |
| | Variable name -> | ||
| if List.contains name boundVariables then | ||
| let newName = name + "'" | ||
| Variable newName |
There was a problem hiding this comment.
А почему newName не может быть в boundVariables?
| | Variable _ -> term | ||
| | Abstraction (arg, body) -> Abstraction (arg, betaReduce body) | ||
| | Application (Abstraction (arg, body), argValue) -> | ||
| let substitutedBody = substitute [(arg, argValue)] body |
There was a problem hiding this comment.
Я так и не понял, зачем substitute список принимает
| match term with | ||
| | Variable name -> name | ||
| | Abstraction (arg, body) -> sprintf "(λ%s.%s)" arg (toString body) | ||
| | Application (func, arg) -> sprintf "(%s %s)" (toString func) (toString arg) No newline at end of file |
There was a problem hiding this comment.
CI ругается, что main-а нет. Собирали бы библиотеку, не ругался бы
| open HW_3.LambdaInterpreter | ||
|
|
||
| [<Test>] | ||
| let ``isFreeVariable: check free variable`` () = |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
HW_3/HW_3/LambdaInterpreter.fs
Outdated
| | Variable v -> | ||
| if v = variable then | ||
| if not (isFreeVariable v value) then | ||
| let newName = v + "'" |
There was a problem hiding this comment.
А правда ли, что newName гарантированно не входит свободно в value? Тут и ниже.
| @@ -0,0 +1,80 @@ | |||
| namespace HW_3 | |||
|
|
|||
| module LambdaInterpreter = | |||
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| | Abstraction of string * LambdaTerm | ||
| | Application of LambdaTerm * LambdaTerm | ||
|
|
||
|
|
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
HW_3/HW_3.Tests/UnitTests.fs
Outdated
|
|
||
| let expr = | ||
| Application ( | ||
| Abstraction ("x", (Abstraction("y", Application( Variable "x", Variable "y")))), |
There was a problem hiding this comment.
Пробелы неконсистентно расставлены
HW_3/HW_3/LambdaInterpreter.fs
Outdated
|
|
||
|
|
||
| let isFreeVariable (variable: string) (expression: LambdaTerm) : bool = | ||
| let rec isFreeVariableReq (variable: string) (bounded : string list) (expression: LambdaTerm) : bool = |
HW_3/HW_3/LambdaInterpreter.fs
Outdated
| if v = oldName then Variable newName else term | ||
| | Abstraction (v, body) -> | ||
| if v = oldName then | ||
| if (isFreeVariable newName body) then |
| if (isFreeVariable newName body) then | ||
| Abstraction (newName, alphaConvert oldName newName body) | ||
| else | ||
| Abstraction (v, body) |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
HW_3/HW_3/LambdaInterpreter.fs
Outdated
| | Abstraction (v, body) -> | ||
| if v = variable then | ||
| Abstraction (v, body) | ||
| elif not(isFreeVariable v value) then |
There was a problem hiding this comment.
| elif not(isFreeVariable v value) then | |
| elif not (isFreeVariable v value) then |
Скобки в F# не ограничивают список параметров, а обозначают границы одного параметра, так что с пробелом
There was a problem hiding this comment.
И почему not? Если переменная под лямбдой не входит свободно в подставляемый терм, её как раз можно не трогать, она ничего там не свяжет. В определении подстановки не так было
yurii-litvinov
left a comment
There was a problem hiding this comment.
Идеологически всё так, но оооочень неаккуратно
HW_3/HW_3.Tests/HW_3.Tests.fsproj
Outdated
| <Project Sdk="Microsoft.NET.Sdk"> | ||
|
|
||
| <PropertyGroup> | ||
| <TargetFramework>net7.0</TargetFramework> |
There was a problem hiding this comment.
На .NET 8 так и не удалось мигрировать? IRL Вы могли бы оказаться в забавной ситуации, когда Вы начинаете деплой в инфраструктуре заказчика, а там рантайм только .NET 8 и нет возможности сказать .NET 7 (например, по политикам безопасности). И программа вообще не запускается. И заказчик такой "Ну вот же, замечания с первой приёмки, целевую платформу поменять, почему не сделали?". И срыв приёмо-сдаточных испытаний, неустойка, позорное увольнение.
HW_3/HW_3.Tests/UnitTests.fs
Outdated
|
|
||
| let expr = | ||
| Application ( | ||
| Abstraction ("x", (Abstraction("y", Application( Variable "x", Variable "y")))), |
HW_3/HW_3/LambdaInterpreter.fs
Outdated
|
|
||
| module LambdaInterpreter = | ||
|
|
||
| /// <summary>The type which expresses the lambda-term.</summary> |
There was a problem hiding this comment.
В F#, кстати, более принято просто /// The type which expresses the lambda-term., без тэгов, где они не нужны.
HW_3/HW_3/LambdaInterpreter.fs
Outdated
| /// <param name="variable">The variable name.</param> | ||
| ///<param name="expression">The lambda-term of an expression.</param> |
There was a problem hiding this comment.
Тут то есть пробел после ///, то нет
HW_3/HW_3/LambdaInterpreter.fs
Outdated
| /// <param name="variable">The variable name.</param> | ||
| ///<param name="expression">The lambda-term of an expression.</param> | ||
| ///<returns>The truth if the variable is in the expression, otherwise false.</returns> | ||
| let rec isVaraibleInExpression (variable: string) (expression: LambdaTerm) : bool = |
HW_3/HW_3/LambdaInterpreter.fs
Outdated
| ///<param name="expression">The lambda-term of an expression.</param> | ||
| ///<returns>The truth if the variable is bounded, otherwise false.</returns> | ||
| let isFreeVariable (variable: string) (expression: LambdaTerm) : bool = | ||
| let rec isFreeVariableRec (variable: string) (bounded : string list) (expression: LambdaTerm): bool = |
There was a problem hiding this comment.
bounded ("ограниченный") лучше переименовать в bound ("связанный")
HW_3/HW_3/LambdaInterpreter.fs
Outdated
| | Application (e1, e2) -> | ||
| Application (substitute variable value e1, substitute variable value e2) | ||
|
|
||
| ///<summary>Performes a one step of beta-reduction.</summary> |
yurii-litvinov
left a comment
There was a problem hiding this comment.
Мелкие замечания остались, но Вы смогли победить переход на .NET 8 с CI, так что зачтена
| let expr = | ||
| Application ( | ||
| Abstraction ("x", | ||
| (Abstraction("y", Application( Variable "x", Variable "y")))), |
There was a problem hiding this comment.
Ну так и всё равно тут скобка с пробелом местами поменяны
|
|
||
| module LambdaInterpreter = | ||
|
|
||
| ///The type which expresses the lambda-term. |
There was a problem hiding this comment.
У Вас был выбор, либо вставить пробел везде, либо удалить везде. Вы выбрали неправильно (ну, не по стайлгайду) :)
No description provided.