WIXLIB

Chapter 4ELM Quality MeasuresElm has recently been updated to version 0.191 and introduced breaking changes,which means some of the plugins and tools are not compatible anymore. However, since the project should last for a while we decided to still go with the latestversion. We will regularly check for updated versions for the broken plugins andif it makes sense we will include them in our development process.4.1IDEAs an IDE we decided to use Visual Studio Code2 with the elm-lang extension3 . This combination provides everything we expect from a code editor likesyntax highlighting, compiler warnings and much more. Additionally, it easilyintegrates with the other tools we decided to use. Unfortunately, there are norefactoring tools included in the extension.4.2FormattingWe decided to follow the style guide of elm-lang4 . There is a npm package5which formats the elm-files according to the standard guide and integrates wellwith the elm-lang extension for Visual Studio Code.4.3TestingFor everything except the UI, we will write unit tests with elm-test6 . If we finda bug at a later stage we first will write a test before we fix the code.Since the user interface changes a lot during the development process, we willnot write unit tests for the UI. Doing otherwise would cause too much overhead1 [9]Elm release notesVisual Studio Code3 [14] ELM Extension for Visual Studio Code4 [17] ELM Style Guide5 [15] ELM-Format tool6 [18] ELM Testing Library2 [38]10

in our opinion. We will however, test the UI by hand after every feature we implement. Testing the UI is also part of the merge-request review process.Code Coverage With the change to elm 0.19 a new of the testing libraryhas been introduced and therefore the code coverage plugin7 is not compatibleanymore. However, as previously mentioned, we will regularly check for anupdate.7 [13]Elm Test Coverage Library11

Chapter 5Introduction to LambdaCalculusIn this section we will explore Lambda Calculus in order to define the functional requirements for this application. The topics are based on the booklet”Introduction to Formal Proof and the Lambda Calculus” by Prof. Dr. FarhadMehta1 .5.1IntroductionLambda calculus was invented by Alonso Church in the 1930s. It is formalmathematical system and was proven to be Turing complete by Alan Turing in1937.2With a syntax that can be described with only two definitions, it is a veryminimal and elegant programming language.Lambda calculus is the basis of functional programming and often used as away to teach this programming paradigm.5.2SyntaxLambda Calculus divides its syntax in the two components: Predicates (P) andλ-Terms (M).P :: M MM :: x λx.M M MThe Term ”x” represents a variable, the term ”λx.M ” is an abstraction withthe parameter x and the body M. An abstraction is usually called a functionin programming languages. ”M M” stands for the application of one term to1 [24]2 [37]Lecture NotesAlan M. Turing: Computability and λ-Definability12

the other. Application is left associative which means M1 M2 M3 is equivalentto((M1 M2 )M3 ). Furthermore, application binds stronger than function, e.gλx.M1 M2 is interpreted as (λx.(M1 M2 ))5.3Alpha ConversionAn alpha conversion or α-conversion, is the action of renaming a bound variable in an abstraction. It only changes the textual representation of a term,functionally the term will still be equivalent.λx.x x λy.y y5.4Beta ReductionBeta reduction or β-reduction is the application of a term to an abstraction. Theequivalent in programming is usually called ”calling a function”. For M1 M2 ,this means to use the λ-term M2 as the argument of the λ-term M1 where M1is an abstraction.(λx.negate 5.5x)10 0.βnegate 1Delta ReductionLambda Calculus provides the option of naming λ-terms using predicates, e.g.x M . A δ-reduction is the action of replacing a (free) variable with itsdefinition.negate λx.(( 0)x) 5.6negate 10 0(λx.( 0) x) 10 0( 0) 10 0.δ.β.βNormal FormA λ-term is in its normal form, if there are no further reductions possible. Theexample in the section Beta Reduction is in its normal form. A property ofLambda Calculus is, that there is at most one normal form. This means thatit is also possible that a term has no normal form, as shown in the followingexample3 :3 Underlinemarks redex, selected for reduction.13

5.7(λx.xx)(λx.xx)0 0 (λx.xx)(λx.xx)0 0 .β.βEvaluation StrategiesA term that can be reduced by either β or δ reduction is also called a redex(short for reducible expression).A λ-term can have several redexes and there are several evaluation strategies todecide which redex to reduce next.This is important because not all strategies will always find a normal form. Inthis chapter we will only look at the two strategies which were part of the lectureat HSR.5.7.1Innermost Leftmost FirstAn innermost redex is a term that does not contain any more redexes. Therecan be multiple innermost redexes in a λ-term.1. Choose the innermost redex2. If there are more than one innermost redexes, choose the leftmost innermost redexThis means that an argument gets reduced before it gets applied. The innermostfirst strategy does not find a normal form for every case as shown in the followingexample:(λy.a)((λx.xx)(λx.xx))0 0(λy.a)((λx.xx)(λx.xx))0 0 5.7.2.β.β.Outermost Leftmost FirstAn outermost redex is not contained in any redexes. There can be multipleoutermost redexes in a λ-term.1. Choose the outermost redex2. If there are more than one outermost redexes, choose the leftmost outermost redexThis means that an argument gets reduced only after it has been applied. Theoutermost strategy will always find the normal form if the term has one. Letslook at how the outermost first strategy would solve the term that the innermoststrategy was unable to reduce to its normal form:(λy.a)((λx.xx)(λx.xx))0 0a0 0 14.β.β

Chapter 6De Bruijn Index6.1The Problem with α-conversionsDe Bruijn Indexing1 is a way to remove the need for α-conversions on nameclashes.Let us look at an example where alpha conversion is required:((λy.λx.y) x) a α((λy.λz.y) x) a β(λz.x) a βxIf we had omitted the alpha conversion, this would have been the result:((λy.λx.y) x) a β(λx.x) a βaAs seen, it would not have produced the correct result x but a. The problemhere is (λx.x) on the second line. The second x is not actually the boundvariable x but a free variable x that just happens to have the same name as thefirst x but we have no way of differentiating the two.There are many rules that say when an α-conversion is needed and when it isnot, but fortunately we do not have to take any of them into consideration whenusing De Bruijn Indices.6.2Encoding Variables with De Bruijn IndexDe Bruijn Indices only affect how abstractions and variables are written.1 [26]De Bruijn indexing in the untyped Lambda-Calculus15

Instead of writing the name of a bound variable, we only write a pointer toits binder. The binder is the abstraction to which the variable is bound. Forexample, in λx.x, λx. is the binder for x.The pointer is a number which indicates in how many abstraction the variableis enclosed in, starting at 0. E.g. λx.x becomes λ.0 and λx.λy.x y becomesλ.λ.1 0.Free variables do not belong to a binder. The number of abstractions the freevariable is enclosed in, is smaller than the index of the variable. The indexvalue is calculated by adding a number found in a lookup table and the numberof abstractions the free variable is surrounded by. For example a becomes 1and λx.a becomes λ.2. However, this encoding has no benefit and therefore, wedecided to not use it in the project.A lambda term encoded using De Bruijn Indices is definitely less human readablethan named bound variables, but that is not relevant. The goal is to make αreductions redundant and therefore simplify β- and δ-reductions.While displaying the term to the user it will be converted into a readable, namedparameter representation.6.3Shift OperationsDuring β-reductions it often happens that the number of abstractions in whicha bound variable is enclosed varies. Lets look at the following example, first inthe named parameter form to make it easier to read:λx.((λy.x) a) βλx.xThe same thing using De Bruijn Indices looks like this:λ.((λ.1) a) βλ.0Note that the shift operation was already applied in the example above, if wewould not have done so, the result would have been λ.1, which is not equivalentto the desired result of λx.x.The shift operation corrects the index, when the number of enclosing abstractions changes.16

Chapter 7Architectural OverviewThe architecture consists of the three main components the parser, the reducerand the frontend. These three components interact with each other to form theapplication.Frontend As the name suggests, the frontend is responsible to render the userinterface and handling user inputs. Based on the term entered by the user. Thefrontend first calls the parser to convert the input text into a data structurebefore calling the reducer with that data structure for the reduction operations.See chapter 10 ”Frontend” on page 30.Parser The parser receives a String from the frontend and tries to parse itto a LambdaTerm which will be returned back to the frontend. If the parserfails, an error will be returned. See chapter 8 ”Parser” on page 18.Reducer As the name implied the reducer is responsible to apply reductionsto lambda terms. It receives a LambdaTerm and some additional inputs andreturns the reduced LambdaTerm . See chapter 9 ”Reducer” on page 25.17

Chapter 8ParserThe job of a parser is to convert a string to a data structure, that can be usedfor further processing.In our case, it should convert a lambda calculus term, entered by the user, intoa data structure, which will be used as the input for the reducer described inthe next chapter.8.1SyntaxBefore discussing the parser, we need to define the syntax we will be using. Wewant it to be as close to the syntax described in chapter 5 as possible. As areminder, this is what that syntax looks like:P :: M MM :: x λx.M M M8.1.1Letter Lambda λInstead of encoding the lambda symbol with another symbol, we decided to usethe UTF-8 symbol λ directlyFor usability reasons, we will allow the user to use backslashes instead of the λsymbol. The conversion will be done in the UI and the parser does not need toknow about that.8.1.2Variable NamesVariable names (x) can consist of one or more UTF-8 characters, except forsome reserved characters like ”(”, ”)”, ”.” and ”λ”.8.1.3White SpacesWhite spaces are used to separate variable names, all other occurrences will beignored.18

8.1.4PredicatesThe definition of P :: M M quite straight forward to implement whenwe already have an implementation of M . The problem with that simple definition is that we do not have a way to differentiate between free variables andconstants.The following two examples demonstrate why that is important:Example 1 Assume we have a predicate (y y a) and a lambda term (b y).If we interpret y as a free variable, then the whole term (b y) can be unifiedwith y and the resulting term will be (b y a).If, on the other hand, we interpret y as a constant, then only y in (b y) unifieswith y and the reduced term will be (b y).Example 2 Maybe a more relatable example is the predicate (plusOne x x 1). Here we want plusOne to be a constant, but x to be a free variable sothat (plusOne 10) results in ( 10 1) when the delta reduction is appliedNow we know why we need to differentiate between constants and free variables,we need to decide on how to do so. It could either be done by having a listof constants or by having a list of free variables. We decided on the list offree variables, on the basis, that usually in programming languages we definevariables and not the things that are not variables.Syntax This is how the before mentioned plusOne predicate would looks likein our syntax: x.plusOne x x 1All free variables need to be defined between the universal quantifier symbol ( )and the the dot (.). Multiple free variables can be separated by whitespaces. Ifa symbol is not defined as a free variable, it will be interpreted as a constant,e.g. plusOne. The free variable definition block is optional. If it is omitted, allvariables will be interpreted as constants.8.28.2.1Resulting Data StructureFunction HeadersThe LambdaParser elm module exposes two functions: parseLambdaTerm andparsePredicate. This is how their type definitions look like:parseLambdaTerm : String - Result ParserError LambdaTermparsePredicate : String - Result ParserError PredicateBoth functions take a String and produce a Result of the respective type( LambdaTerm or Predicate ).19

The result type is part of the elm/core library (standard library) and can eitherbe an error or a result. In contrast to the Maybe type it cannot only represent whether there is a result or not, but also what went wrong in case of anerror.8.2.2Predicate and LambdaTerm TypesP :: M MM :: x λx.M M MThis is the syntax that we want to represent with the following types:type alias Predicate { freeVariables : Set String, left : LambdaTerm, right : LambdaTerm}type LambdaTerm Abstraction UniqueVariableName LambdaTerm BoundVariable BoundIndex FreeVariable VariableName Application LambdaTerm LambdaTermM is equivalent to LambdaTerm , Abstraction is λx.M and Application isM M.Instead of having one constructor for variables, we have two: BoundVariableand FreeVariable . The reason why we decided to do that is, that the differentiation of the two gives us some advantages in the reducer. Only variables oftype BoundVariable are encoded using de Bruijn index, see chapter 6. For thefree variables it does not make much sense to do so, because in the reducer wefrequently compare the value of multiple free variables which would generatetoo much overhead due to all the lookups.In addition to a LambdaTerm left and a LambdaTerm right the Predicate typealso includes the set of free variables inside this predicate, described in thesection before this.8.38.3.1Parser Implementationelm/parser LibraryThanks to the elm/parser 1 library, the implementation turned out to be simplerthan we anticipated. It took us a while to find out the best way to use it butafter that it was quite straight forward.The way a parser is written using elm/parser is very declarative:type alias LambdaTermList 1 [16]elm/parser library20

List LambdaTermParsedtype LambdaTermParsed Abstraction VariableName LambdaTermParsed Variable VariableName TermList LambdaTermList -- type definitiontermInParenthesis inContext ParsingTermInParenthesis -- only for error messagessucceed LambdaTermParsed.TermList . symbol "(" . spaces lazy (\ - inContext ParsingTermInParenthesis lambdaTermList) . spaces . symbol ")"This is an example of how a term in parenthesis, like (a b), is parsed. Theoptional inCotext . is there to generate more precise error messages. Theimportant bit starts with the succeed function. Its first argument is a function,in our case a type constructor function. This is the type that the parser shouldproduce if it is successful.After the required return type comes the actual parsing code. There are twodifferent functions we need to differentiate here: . means expect somethingbut ignore it and means expect something and memorise it. If you arefamiliar with regular expressions, is comparable to a capturing group.If we look at the termInParenthesis we see that it starts with an open parenthesis "(" , followed by an arbitrary amount of whitespaces. This is followedby the important part, a lambdaTermList, which will be handled in its ownfunction. The lazy part is there for back propagation. In this case, the lambdaTermList is the only part that we keep.When we look at the definition of LambdaTermBeforeLeftAssociation.TermList ,we see that it takes a single argument of type LambdaTermList , so the parsingdefinition has to return exactly one element of that type. If LambdaTermBeforeLeftAssociation.TermListhad more than one parameter, we would have to have more than one element.8.3.2Parsing StepsDue to some limitation in the parsing library and requirements of the reducer,we split the parsing into the three steps: Parsing, resolving left associativelyand finally conversion to De Bruijn encoded terms.8.3.3ParsingThe first step is to convert a String , entered by a user, to a LambdaTermParseddata structure using the elm/parser library described above.21

Data Structure This step results in the data structure we have seen in theelm/parser example above:type alias VariableName Stringtype alias LambdaTermList List LambdaTermParsedtype LambdaTermParsed Abstraction VariableName LambdaTermParsed Variable VariableName TermList LambdaTermListExample"λx.a b"-- will be converted to:Abstraction "x" (TermList [Variable "a", Variable "b"])8.3.4Left AssociationLambdaTermParsed does not yet include a representation for applications. Instead it contains a list of lambda terms. The goal of this step is to convert thisLambdaTermList to nested Application s.Data Structure Abstraction and Variable are basically the same as in theprevious data structure. The difference lies in the Application , which replacesTermList :type LambdaTermLeftAssociated Abstraction VariableName LambdaTermLeftAssociated Variable VariableName Application LambdaTermLeftAssociated LambdaTermLeftAssociatedExampleTermList [Variable "a", Variable "b", Variable "c"]-- will be converted to:Application (Application (Variable "a") (Variable "b")) (Variable "c")22

8.3.5De Bruijn IndexThe final step of the parser is to split the variables into bound- and free variables, while encoding the bound variables using De Bruijn Indices in the sameprocess.In the end, the resulting data structure will be traversed one final time to makeevery variable name unique by incrementing a counter every time the samevariable name occurs. This counter can then be used in the UI to help usersdifferentiate between multiple variables with the same name.Data Structure The Variable constructor from the previous step has beensplit into separate constructors for BoundVariable and FreeVariable . Toincorporate the requiremen

There are currently a few lambda calculus interpreters avail-able, but all of them su er from a complicated user experience, an unappealing user interface and require too much e ort to understand. The purpose of the term project "Lambda Calculus Calculator" is to write a user friendly lambda calculus interpreter, which can be used to teach lambda