We find that the interpreter does implement the expected result. Now let us see what our interpreter actually implements.ĮvalCBN (EApp (EAbs (Id "x") (EAbs (Id "x") (EVar (Id "x")))) (EVar (Id "a"))) = - line 6ĮvalCBN(subst (Id "x") (EVar (Id "a")) (EAbs (Id "x") (EVar (Id "x")))) = - line 22ĮvalCBN(EAbs (Id "y") (subst (Id "x") (EVar (Id "a")) (EVar (Id "y")))) = - line 16ĮvalCBN(EAbs (Id "y") (EVar (Id "y"))) = - line 8 **Activity:** Discuss which of the two possible choices is taken in the programming languages you know. This makes a difference, because in the first case $(\lambda x.\lambda x. $$(\lambda \color$ is bound by the red or by the blue one. Our next example is $(\lambda x.\lambda x. We will continue this on Thursday, but try to do similar examples yourself before. Then, for the pattern matching my eyes only need to be able to identify what the "variable", the "argument" and the "body" are in the term at hand. For example, the equation of `line 6` I remember as "substitute the variable by the argument in the body". **Tip:** It is easier to apply an equation if one has an English phrase for it. x) a$$ Following the steps specified in the interpreter, we compute (line numbers refer to ()):ĮvalCBN (EApp (EAbs (Id "x") (EVar (Id "x"))) (EVar (Id "a"))) = - line 6ĮvalCBN (subst (Id "x") (EVar (Id "a")) (EVar (Id "x"))) = - line 15 We do some computations by hand to convince ourselves that the substitution function `subst` is doing its job. In the following we will execute the interpreter pen-and-paper, both using concrete syntax and abstract syntax. This semantics has been implemented by (). Mathematically, the semantics of $\lambda$-calculus is given by the $\beta$-rule, which is to say, by capture avoiding substitution. If you know the order of operations and how to translate concrete syntax to ASTs, you don't need to make a detour via CSTs. If you want to design your own grammar, you need to understand CSTs in order to get the order of operation right. Why do I need to understand what a CST is? The parser creates first a CST and then turns it into an AST. What are they for then?ĬSTs are an intermediate representation used by the parser. But I remember there was also sth like concrete syntax trees. The AST is used by the interpreter to evaluate (=run=execute) the program. The parser is needed to turn a program into its AST. The grammar is needed to generate the parser. For readability, in the following, it is tempting to abbreviate these trees as inīut it is safer to do this only after we gained some practice. (I ignore noreduce as a mere instruction to the interpreter.) Lambda. Prog (EApp (EAbs (Id "x") (EVar (Id "x"))) (EVar (Id "a"))) The lambda calculus is a universal model of computation. TestLambdaNat` gives us the linearized AST Parsing this program via `echo "(\ x.x)a" |. The $\lambda$-caclulus term $(\lambda x.x) a$ is written in our programming language LambdaNat as `(\x.x)a`. We review one example to remind us of the relevant notation. how our Haskell implementation of the interpreter for $\lambda$-calculus works. to execute by hand $\lambda$-calculus programs according to its operatial semantics the formal definition of capture avoiding substitution Refer back to the earlier parts of these lecture notes for full detail. Quite some material has accumulated, so I here summarize some salient points and then discuss the interpreter in more detail. We’ve ended up with a weird constraint on our m, though: (MonadReader m).# Interpreting Lambda Calculus Pen-and-Paper So we just want a normal catamorphism which computes monadic values. Take the un-evaluated computation for the body of an abstraction and save it to evaluate later in a differentĮnvironment. But this is not what we want, because we want to Us to automatically evaluate all the monadic computations for sub-terms before evaluating the With monadic catamorphisms the idea is that the Traversable constraint allows Initially I thought that I would want to write this as a monadic Later, when evaluating anĪpplication we can just fish out the monadic computation and evaluate it in the Which we can just put into the closure value. This is pretty neat - the body of an abstraction has been evaluated to a m (Value m), Type Algebra f a = f a -> a - specialisation of the real signature - cata :: Algebra f a -> Fix f -> a - note the weird contstraint evalAlgebra :: ( MonadReader m ) => Algebra LambdaF ( m ( Value m )) evalAlgebra term = case term of Index i -> do e do - capture the environment e do - this will cause pattern match failures if the term - isn't well-typed Clos ctx t ( c : ctx )) t
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |