Tag Archives: Lambda Calculus

In this post I will show two different sets of properties that any variation of λ-calculus with explicit substitutions may or must have. The must: 1) Any substitution must end, i. e. the process of change a variable by a term must always end, no matter how you do it. Put it in another way, … more

As I told you before, performance is something desirable when programming a λ interpreter. The sustitutions we saw are made in one step. I will note the beta step as →β and a substitution step as →. For instance, (λx.x) z  →β  x[x/z]  →  z. The computations of the traditional lambda calculus are always: T … more

With this cite of Monthy Python, I will move into another family of calculi. What’s wrong with our good ol’ λ-calculus? Nearly nothing, except if you want to implement it in a real PC. In one of the firsts posts I’ve mentioned the α-congruence. The idea is that terms that only differs in the name … more

As you probably already now, recursive function are those that call them self. For instance, you can define the factorial function as: fact(0) = 1 fact(n) = n*fact(n-1) This doesn’t look like something you can say with the small syntaxis of the λ-calculus. That is right, but I will prove that you can say something … more

This new post is intended to summarize all what is written in this page. First of all, an errata from the previous post: I encourage the reader to define other functions, like the predecesor of a number… Well, I can’t remember if I planned to be that evil, or if I was just too drunk … more

One simple way to make arithmetic expressions in lambda calculus, is just to extend the calculus with the arithmetic rules: (λx.(λy. x+y)) 2 3 → (λy. 2+y) 3 → 2+3 = 5 But that’s pretty easy for us, and (as you problably have already noticed) we like to complicate what’s easy. So let’s try to … more

From the Wikipedia: “calculus can refer to any method or system of calculation”, and that’s not an exception for the Lambda Calculus. First of all, lets define the terms of this calculus: A Lambda Term is something with the form x where x is in V a set of variables. (u v) where u and … more

A Term Rewriting System (TRS) is a very powerful yet simple math tool used, for instance, for the creation of computational models. Given a set of function symbols S, and an (uncountable) set of variables V, I will define rewriting rule by example. Suppose we have the “constant” function (function without parameters) 0 (representing a … more

This blog will contain all the news about my progress in my master thesis, entirely sponsored by Manas Technology Solutions. The idea will be to translate a lambda calculus with explicit substitutions with named variables to a calculus à la de Bruijn. If you have no idea what I’m talking about, don’t be afraid, wait … more