Phép Tính Lambda – Wikipedia Tiếng Việt

Bước tới nội dung

Nội dung

chuyển sang thanh bên ẩn
  • Đầu
  • 1 Chú thích
  • Bài viết
  • Thảo luận
Tiếng Việt
  • Đọc
  • Sửa đổi
  • Sửa mã nguồn
  • Xem lịch sử
Công cụ Công cụ chuyển sang thanh bên ẩn Tác vụ
  • Đọc
  • Sửa đổi
  • Sửa mã nguồn
  • Xem lịch sử
Chung
  • Các liên kết đến đây
  • Thay đổi liên quan
  • Trang đặc biệt
  • Thông tin trang
  • Trích dẫn trang này
  • Lấy URL ngắn gọn
  • Tải mã QR
In và xuất
  • Tạo một quyển sách
  • Tải dưới dạng PDF
  • Bản để in ra
Tại dự án khác
  • Wikimedia Commons
  • Khoản mục Wikidata
Giao diện chuyển sang thanh bên ẩn Bách khoa toàn thư mở Wikipedia

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, Python, 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).

Chú thích

[sửa | sửa mã nguồn]
  1. ^ A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
  2. ^ For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
  3. ^ Henk Barendregt, The Impact of the Lambda Calculus in Logic and Computer Science. The Bulletin of Symbolic Logic, Volume 3, Number 2, tháng 6 năm 1997.
Bài viết này vẫn còn sơ khai. Bạn có thể giúp Wikipedia mở rộng nội dung để bài được hoàn chỉnh hơn.
  • x
  • t
  • s
Lấy từ “https://vi.wikipedia.org/w/index.php?title=Phép_tính_lambda&oldid=71803379” Thể loại:
  • Logic toán
  • Khoa học máy tính
  • Phương pháp hình thức
  • Khoa học máy tính lý thuyết
  • Phát minh của Hoa Kỳ
  • Mô hình tính toán
Thể loại ẩn:
  • Tất cả bài viết sơ khai
  • Sơ khai

Từ khóa » định Lý Kleene