![]() ![]() | otherwise = error $ "Cannot substitute '" ++ show x ++ "' in term '" ++ show (TmAbs y t1) ++ "'" | x /= y & (y `notElem` freeVars newVal) = TmAbs y (subst x t1 newVal) We can convert the definitions to Haskell code easily: In an application, we recursively substitute all bound variables In an abstraction, as long as the variable in the argument is different, we can recursively substitute the terms Renaming all occurences of “x” to “s” within “y” (which doesn’t contain any “x”) is just “x” Renaming all occurences of “x” to “s” within “x” is just “s” The only thing left for us to implement is subst, and we should be good. ![]() ![]() We do that because we didn’t “treat” variables separately in our data definition. Note how we pattern match against _ _) to detect a variable. Įval (TmApp (TmAbs x t12) _ _)) = subst x t12 v2 - E-AppAbsĮval (TmApp _ _) t2) = let t2' = eval t2 in TmApp v1 t2' - E-App2Įval (TmApp t1 t2) = let t1' = eval t1 in TmApp t1' t2 - E-App1 It looks like we have a new notation here: means that we change all occurences of with within. We set variables to additionally hold VarName (which is a string in this case) for pretty printing and comparison of variables. Note that a value in the system is just an abstraction. Our syntax, per BNF is defined as follows: ::= x It was introduced by the mathematician Alonzo Church in the 1930s as part of his research of the foundations of mathematics. The equality sign = is replaced with a dot, and instead of writing we write. For example is a function abstraction and is a function application. Function abstraction defines what a function does, and function application “computes” a function. The grammar rules are divided in two parts: function abstraction and function application. Lambda calculus is a formal system for expressing computation. It provides an interesting overview of some design decisions particularly for the lambda calculus. This post is more focused on building the lambda calculus from scratch. My previous post was a general overview of how we can design an evaluator and a type checker. This tutorial serves as a very short and quick summary of the first few chapters of TAPL. ![]()
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |