# Lambda Calculus

Lambda Calculus is a formal language to define computations. In Lambda Calculus any computation is defined in terms of evaluation of Lambda Abstractions - application of procedures. Evaluation is defined as substitution of terms.

The fundamental, unique property is that the order of evaluation (substitution) does not matter as long as procedures are pure functions (same input - same output. Always) and referential transparency is maintained.

## The Substitution Model

In Math, which is the science of abstract patterns, only `equal` quantities (the same entity) could be substituted for an equal (same).

Each occurrence of a Number 2 is a reference to the same unique concept (abstract entity) of a Number 2.

In Nature, in What Is, only `equivalent` could be substituted to equivalent. Two hydrogen atoms (or two water molecules) are not the same, but they are equivalent. Two water molecules have the same structure, but this very notion of sameness is an abstraction of the mind. Structures are equivalent.

In programming Equivalence is defined by behavioral traits using Duck Typing (if it walks like duck and quacks like a duck). The key abstractions are Interfaces (a set of function signatures) and Protocols (a set of named if-then-else rules).

## Equations

Assert what is equal (or equivalent).

## Programming languages

Good programming languages provide means to model (using protocols and interfaces) the domain of a program and to define embedded DSLs for subdomains. DSLs usually from a hierarchy of layers.

Scheme is an implementation of Untyped Lambda Calculus. So are Common Lisp and other Lisps.

Erlang could be considered as an implementation of Untyped Lambda Calculus.

Haskell is an implementation of Typed Lambda Calculus. So are Scala and other Standard ML descendants.