Что можно вычислить?

☀️ Проблема разрешения и лямбда-исчисление: рождение теории вычислимости
В 1928 году Давид Гильберт поставил перед математиками грандиозную задачу: найти универсальный алгоритм, который для любой формулы логики первого порядка за конечное время определит, истинна она или нет. Это назвали Entscheidungsproblem — «проблемой разрешения».
Математическое ядро:
Чтобы решить эту проблему, нужно было сначала точно определить, что такое «алгоритм» или «механическая процедура». В 1936 году два математика независимо друг от друга предложили свои ответы.
Алонзо Черч создал лямбда-исчисление — формальную систему для описания вычислений через функции. В ней всё строится на трех элементах:
1. Переменные: x, y, z...
2. Абстракция: λx.M (функция от x, возвращающая M)
3. Аппликация: M N (применение функции M к аргументу N)
Например, функция «удвой число» записывается как:  λx. x + x 
А применение её к числу 3:  (λx. x + x) 3  →  3 + 3  →  6 
Зачем это нужно?
Лямбда-исчисление оказалось невероятно мощным. Черч доказал, что с его помощью можно выразить любую вычислимую функцию. Более того, он показал, что проблема разрешения неразрешима: не существует алгоритма, который определит истинность любой формулы логики первого порядка. Это был первый строгий результат о границах вычислений.