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...

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...

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...

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...

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...