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:

λx0.(λx1.x1)x0

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 xs. After the replacement is completed, the compiler/interpreter change all of the xs to 4s:

λ40.(λ41.41)40

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

40 + (41 + 41)40

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