math posts

Read about our day to day discoveries, the trips we take around the world, our personal developments and news about the things we do at Manas.

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

  • Nov 13 2008
    Making a thesis

    In all previous posts I've tried to teach the different aspects inside my thesis. But after going deeper and deeper, the concepts tend to complicate too much, and much more dedication from the reader is needed. After trying to add another...

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

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

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