Trong
logic toán học và
khoa học máy tính,
phép tính lambda (
tiếng Anh:lambda calculus) hay còn được viết là
λ-calculus, là một
hệ thống hình thức dùng trong việc định nghĩa
hàm số, ứng dụng hàm số và
đệ quy. Phép tính lambda được
Alonzo Church đề xuất vào những năm 193x như là một phần của một nghiên cứu về các
nền tảng toán học.
[1][2] Hệ thống nguyên thủy đã được chứng minh là xung khắc logic vào năm 1935 khi
Stephen Kleene và
J. B. Rosser phát triển
nghịch lý Kleene–Rosser. Phép tính lambda sau đó đã được phát triển để trở thành một công cụ quan trọng trong việc nghiên cứu các vấn đề
lý thuyết tính toán và
lý thuyết đệ quy, và hình thành nên nền tảng cơ bản của mô hình
lập trình hàm.
[3]Trong phép tính lambda, các hàm là
thực thể lớp nhất được truyền vào như các tham số, và trả lại kết quả. Bởi vậy các biểu thức lambda là một dạng của khái niệm thủ tục không có tên mà không tạo ra
hiệu ứng phụ. Giải tích hàm có thể được hiểu như là một ngôn ngữ lập trình lý tưởng và vô cùng nhỏ gọn. Nó có khả năng biểu diễn bất kỳ
giải thuật nào, và nó tạo ra mô hình
lập trình hàm. Các chương trình được tạo thành từ các hàm không có trạng thái và chỉ đơn giản nhận vào dữ liệu và trả lại đầu ra, không tạo ra các hiệu ứng phụ làm thay đổi dữ liệu đầu ra. Các ngôn ngữ lập trình hàm hiện đại, xây dựng dựa trên phép tính lambda gồm có
Erlang,
Haskell,
Lisp,
ML, và
Scheme, cũng như là các ngôn ngữ gần đây như
Clojure,
F#,
Nemerle, và
Scala.Phép tính lambda tiếp tục đóng vai trò quan trọng trong
các nghiên cứu cơ bản về toán học, thể hiện trong các thư từ trao đổi của
Curry-Howard. Tuy nhiên, phép tính lambda bất định kiểu không tránh khỏi các nghịch lý về lý thuyết tập hợp (xem
Nghịch lý Kleene-Rosser).