A simple input sample: (lambda x.(x x))(lambda x.(x x)). Or type help to learn more.
Try fix-point combinator: (lambda f. ((lambda x.(f (x x))) (lambda x.(f (x x))))) (lambda x.x)

What is λ Calculus?

• λ Calculus is considered as the smallest universal programming language.
• The λ calculus is developed as a theory of functions for manipulating functions in a purely syntactic manner.
• All functional programming languages can be viewed as syntactic variations of the lambda calculus, so that both their semantics and implementation can be analysed in the context of the lambda calculus.
• Church's Thesis: The effectively computable functions on the positive integers are precisely those functions definable in the pure lambda calculus (and computable by Turing machines).
  The term "thesis" means a conjecture. But since all methods developed for computing functions have been proved to be no more powerful than the lambda calculus, it captures the idea of computable functions as well as we can hope.
• Introduction to λ Calculus is publicly available here and here.

Features

• Automatic formatting
• Check unbound variables
• Alpha reduction (eliminate duplicated variable name)
• Normal order reduction and normal order evaluation
• Identify infinite reduction
• More features on the way...
  Let me know if you have new ideas or suggestions.