A conceptual model of computers based on defining and evaluating functions. Of the current ProgrammingLanguages, LISP, Scheme, Haskell and other Category:FunctionalProgrammingLanguages best expose this conceptual model.

One of the fundamental proofs in ComputerScience is that any result calculable in LambdaCalculus is calculable on a FiniteStateMachine.

(From memory:)

LambdaCalculus is based on the idea that you have two types of rewrite rules, one where you change the names of variables, and one where you replace a variable with its expansion. And that's it.

For instance, if we define "one" as a function which outputs its argument once, we have

one = λx(x)

then the successor function might be defined as

successor = λx.y(x y y)

so "successor one" is

two = successor one two = λx.y(x y y) λx(x)

now we do an alpha reduction (rename some variables)

two = λx.y(x y y) λz(z)

now we do a beta reduction (replace x with its value (λz(z))

two = λy(λz(z) y y)

and a beta reduction on z

two = λy(y y)

we now have a function that outputs its argument twice.

Three is obvious

three = sucessor two

which eventually expands to

three = λx(x x x)

Addition is easy

add = λx.y.z(x z y z)

five = add two three five = λx.y.z(x z y z) λa(a a) λa(a a a) five = λz(Λa(a a) z λa(a a a) z) five = λz(z z z z z)