Let's have a look a bit more in depth at this concept of computation as rewriting. First of all, the beta-rule. As we have shown in the previous slide, we call beta-rule this rewriting rule; we call redex a string that is an abstraction followed by another term. Now, a beta-rule may even be applied inside a term. So, whenever we find an application, a l something applied to an argument, then we may rewrite the term. We say that we may reduce, we may contract the redex.

---