Lambda Calculus was invented by Alonzo Church as a formal system to model computations using functions to define abstractions and applications. It is the most simplest programming language.
Symbols or keywords:
Lambda Calculus reserves very few symbols for use.
The Greek letter
λ has become the unofficial keyword to represent start of a function.
. is used to separate function parameter and function body.
() is optionally used to group function application.
In Lambda Calculus, unlike other programming languages, any sequence of non-blank characters can be used as identifiers.
λ expression may be a name to identify an abstraction point, a function to introduce an abstraction or a function application to specialize an abstraction.
<expression> ::= <name> | <function> | <application>
name may be any sequence of non-blank characters.
example: "lambda", "calculus", "10", "15", "+", "-->"
λ function is an abstraction over a
<function> ::= λ<name>.<body>
λ expression is a function abstraction(or simply a function) generally knows as an
identity function which returns the parameter passed to the function.
x after the
λ represents the name of the parameter used in the function abstraction.
. after name
x separates it from the expression
x which is called function's body.
<body> can be a
λ expression including another function or
<body> ::= <expression>
λx.λy.x is a function where
λy.x is the function body which is another function.
A function's name is also called as the function's
bound variable and it is like a parameter in a function.
function application has the following syntax:
<application> ::= (<function expression> <argument expression>)
<function expression> ::= <expression> <argument expression> ::= <expression>
example: (λx.x λa.λb.b)
In a function application the function expression(or function abstraction) is applied to the argument expression.
There are two approaches to evaluate a function application,
applicative order and
applicative order all occurrences of the function expression's bound variable is replaced by the value of the argument expression.
normal order all occurrences of the function expression's bound variable is replaced by unevaluated argument expression.
we will see more about functions and function applications in the next post