Существует две распространенные (*) модели вычисления : модель Lambda Calculus (LC) и модель Тьюринга (TM).
Лямбда-исчисление подходит к вычислениям, представляя их с помощью математического формализма, в котором результаты создаются композицией функций в области типов.LC также относится к Combinatory Logic , который считается более обобщенным подходом к той же теме.
Модель машины Тьюринга подходит к вычислениям, представляя их как манипуляциюсимволов, хранящихся в идеализированном хранилище с использованием набора основных операций (таких как сложение, мутация и т. д.).
Эти разные модели вычислений являются основой для разных семейств языков программирования.Лямбда-исчисление породило такие языки, как ML , Scheme и Haskell .Модель Тьюринга породила C , C ++ , Pascal и другие.Как обобщение, большинство языков функционального программирования имеют теоретическую основу в лямбда-исчислении.
Из-за природы лямбда-исчисления возможны определенные доказательства поведения систем, построенных на его принципах.Фактически доказуемость (т. Е. правильность ) является важной концепцией в LC и делает возможными определенные виды рассуждений и выводов о системах LC.LC также связана (и опирается на) теорию типов и теорию категорий.
В отличие от этого, модели Тьюринга в меньшей степени полагаются на теорию типов, а больше на структурирование вычислений как серии переходов состояний в базовой модели.Модели вычислений Тьюринга более сложны в утверждениях и не поддаются тем же видам математических доказательств и манипуляций, что и программы на основе LC.Однако это не означает, что такой анализ невозможен - некоторые важные аспекты моделей TM используются при изучении виртуализации и статического анализа программ.
Поскольку функциональное программирование основывается на тщательном отборе типов и преобразовании между типами,FP может восприниматься как более «математический».
(*) Существуют и другие модели вычислений, но они менее актуальны для этого обсуждения.