I did an undergrad in computer science. I learned about deterministic finite automata, nondeterministic finite automata, Turing machines, universal Turing machines, diagonalization, countability, the halting problem, Chomsky's hierarchy, and pumping lemma. (I forget what the last one was about, I'll have to review)

After hearing about the superiority of functional programming, and developing a curiosity in it, I started studying it's foundations: the lambda calculus devised by Alonzo Church.

I just googled a few links and read up on things after the course of a week in order to get what's going on. (I like sleeping on things. I find it makes it easier to progress the very next day)

I was stuck today for about 20 minutes trying to understand how the successor function is defined.

I was stuck on the following. Actually, this is the example that helped to make things clear. Other examples use different notations and it was probably messing me up.

succ c2

= λn. λs. λz. s (n s z) (λs. λz. s (s z))

-> λs. λz. s ((λs. λz. s (s z)) s z)

-> λs. λz. s (s (s z))

We get from the first line to the second line with beta-redex and likewise from the second line to the third.

We have the form λx.y(z)

Where λ is the statement for a function. (functions are not named in this language, they are anonymous)

x is the formal parameter for the function. In lambda calculus, functions only have one parameter.

y is the body of the function.

z is an expression for which the function λ is applied to.

Alpha-equivalence

Any function of this form: λx.x is the identity function. Any expression that this function is applied to returns the expression.

λx.x(z) = z

λy.y(x) = x

The two functions above are both the identity function. Since they are functionally equivalent, we say that they are alpha-equivalent. Any two functions which act the same on all applications are said to be alpha-equivalent.

Beta-redex

The application of a function to an expression is a beta-redex.

λx.x(y)

To perform a beta-redex on the above, we substitute all occurences of the argument (the first x) in the body of the function (the second x) with the expression that the function is being applied to it (the y)

λx.x(y) = y

λx.z(y) = z

λy.y(x) = x

λw.y(y) = y

λx.xv(y) = yv

λp.qrtp(ff) = qrtff

and so on.

Will add more later on so that we can get back to my original problem.