# Counting Calculus

# Counting Calculus

#### Note: this is not finished yet!

A programming language of which the primary way of doing mathematical calculation is by counting the amount of α-conversions done in a lambda-calculus expression. An example of such an expression:

(λy.λx.yx)(λx.x)

*Counting Calculus* works with expressions that were fully β-reduced. The example above would become:

λx.(λx.x)x

Now the language α-converts the expression into this:

λx^{0}.(λx^{1}.x^{1})x^{0}

Next, the language counts all of the variables with the same base (e.g. *x*). The only variable in the example above is *x*, and there are exactly 4 of *x*s.
After the replacement is completed, the compiler/interpreter change all of the *x*s to *4*s:

λ4^{0}.(λ4^{1}.4^{1})4^{0}

Finally, the language removes all of the *λ* symbols and replaces the dots with *+*s:

4^{0}+ (4^{1}+ 4^{1})4^{0}

Now we have a mathematical expression, the result of which is 9 (1 + [4 + 4] * 1 = 9)