there is no way to answer the question of whether two lambda calculus expressions are the same as each other (in more specific words, there is no general algorithm that can show that two lambda expressions are equivalent). this was the first problem where the idea of undecidability could be proven. later, undecidability was also proven for the halting problem, where it was shown that there is no general way to show whether or not a program will keep running forever. lambda calculus has had large effects on lots of functional programming languages, such as lisp, ml, and haskell.