Giải tích Lambda là một hệ thống chính thức trong logic toán học để thể hiện các phép tính dựa trên trừu tượng và áp dụng các hàm sử dụng ràng buộc và thay thế biến. Đây là một mô hình phổ quát có thể được áp dụng cho thiết kế của bất kỳ máy Turing nào. Phép tính lambda lần đầu tiên được giới thiệu bởi Church, một nhà toán học nổi tiếng, vào những năm 1930.
Hệ thống bao gồm xây dựng các thành viên lambda và thực hiện các hoạt động giảm thiểu trên chúng.
Giải thích và Ứng dụng
Chữ cái Hy Lạp lambda (λ) được sử dụng trong các biểu thức lambda và các thuật ngữ lambda để biểu thị ràng buộc của một biến trong một hàm.
Giải tích Lambda có thể không định kiểu hoặc nhập kiểu. Trong biến thể đầu tiên, các hàm chỉ có thể được sử dụng nếu chúng có khả năng nhận dữ liệu thuộc loại này. Tính toán lambda được nhập yếu hơn, có thể biểu thị một giá trị nhỏ hơn. Tuy nhiên, mặt khác, chúng cho phép bạn chứng minh nhiều điều hơn.
Một lý do khiến có rất nhiều loại khác nhau là mong muốn của các nhà khoa học làm được nhiều hơn nữa mà không từ bỏ cơ hội chứng minh các định lý giải tích lambda mạnh mẽ.
Hệ thống có các ứng dụng trong nhiều lĩnh vực khác nhau của toán học, triết học, ngôn ngữ học và khoa học máy tính. Trước hết, phép tính lambda là một phép tính đã đóng một vai trò quan trọng trong sự phát triển lý thuyết của ngôn ngữ lập trình. Đó là các phong cách tạo chức năng mà các hệ thống thực hiện. Chúng cũng là một chủ đề nghiên cứu sôi nổi về lý thuyết của các danh mục này.
Dành cho hình nộm
Phép tính lambda được giới thiệu bởi nhà toán học Alonzo Church vào những năm 1930 như một phần trong nghiên cứu của ông về nền tảng khoa học. Hệ thống ban đầu được chứng minh là không nhất quán về mặt logic vào năm 1935 khi Stephen Kleen và J. B. Rosser phát triển nghịch lý Kleene-Rosser.
Sau đó, vào năm 1936, Church đã chọn lọc và chỉ xuất bản phần liên quan đến tính toán, cái mà ngày nay được gọi là phép tính lambda không có kiểu. Năm 1940, ông cũng đưa ra một lý thuyết yếu hơn nhưng nhất quán về mặt logic được gọi là hệ thống loại nguyên tố. Trong tác phẩm của mình, ông giải thích toàn bộ lý thuyết bằng những thuật ngữ đơn giản, vì vậy có thể nói rằng Church đã xuất bản lambda giải tích cho hình nộm.
Cho đến những năm 1960, khi mối quan hệ của nó với các ngôn ngữ lập trình trở nên rõ ràng, λ chỉ là một chủ nghĩa hình thức. Nhờ các ứng dụng của Richard Montagu và các nhà ngôn ngữ học khác trong ngữ nghĩa của ngôn ngữ tự nhiên, giải tích đã có vị trí tự hào trong cả ngôn ngữ học và khoa học máy tính.
Nguồn gốc của ký hiệu
Lambda không là viết tắt của một từ hay từ viết tắt, nó xuất phát từ một tham chiếu trong Toán học chính của Russell, sau đó là hai thay đổi về kiểu chữ. Ví dụ về ký hiệu: đối với một hàm f với f (y)=2y + 1 là 2ŷ + 1. Và ở đây chúng tôi sử dụng dấu mũ (“hat”) trên y để gắn nhãn cho biến đầu vào.
Ban đầu nhà thờ dự định sử dụng các biểu tượng tương tự, nhưng các máy sắp chữ không thể đặt biểu tượng "chiếc mũ" phía trên các chữ cái. Vì vậy, thay vào đó họ đã in nó ban đầu là "/\y.2y+1". Trong lần chỉnh sửa tiếp theo, nhân viên đánh máy đã thay thế "/ \" bằng một ký tự tương tự về mặt hình ảnh.
Giới thiệu về giải tích lambda
Hệ thống bao gồm một ngôn ngữ của các thuật ngữ, được chọn bởi một cú pháp chính thức nhất định và một tập hợp các quy tắc chuyển đổi cho phép chúng được thao tác. Điểm cuối cùng có thể được coi là một lý thuyết cân bằng hoặc như một định nghĩa hoạt động.
Tất cả các hàm trong phép tính lambda đều ẩn danh, nghĩa là chúng không có tên. Chúng chỉ nhận một biến đầu vào và currying được sử dụng để triển khai các âm mưu có nhiều biến.
điều khoản Lambda
Cú pháp tính toán xác định một số biểu thức là hợp lệ và những biểu thức khác là không hợp lệ. Cũng giống như các chuỗi ký tự khác nhau là chương trình C hợp lệ và một số thì không. Biểu thức thực tế của phép tính lambda được gọi là "số hạng lambda".
Ba quy tắc sau đây cung cấp một định nghĩa quy nạp có thểáp dụng cho việc xây dựng tất cả các khái niệm hợp lệ về mặt cú pháp:
Bản thân biến x là một thuật ngữ lambda hợp lệ:
- nếu T là LT và x không phải là hằng số thì (lambda xt) được gọi là trừu tượng.
- nếu T cũng như s là khái niệm thì (TS) được gọi là ứng dụng.
Không có gì khác là một thuật ngữ lambda. Do đó, một khái niệm có giá trị nếu và chỉ khi nó có thể đạt được bằng cách áp dụng lặp lại ba quy tắc này. Tuy nhiên, một số dấu ngoặc có thể bị bỏ qua theo các tiêu chí khác.
Định nghĩa
Biểu thức Lambda bao gồm:
- biến v 1, v 2,…, v n,…
- biểu tượng của sự trừu tượng 'λ' và dấu chấm '.'
- ngoặc ().
Tập hợp Λ có thể được định nghĩa một cách quy nạp:
- Nếu x là một biến thì x ∈ Λ;
- x không phải là hằng số và M ∈ Λ thì (λx. M) ∈ Λ;
- M, N ∈ Λ, thì (MN) ∈ Λ.
Chỉ định
Để giữ cho ký hiệu của biểu thức lambda không gọn gàng, các quy ước sau đây thường được sử dụng:
- Bỏ ngoặc ngoài: MN thay vì (MN).
- Các ứng dụng được cho là vẫn liên kết: người ta có thể viết MNP thay vì ((MN) P).
- Phần thân của phần trừu tượng mở rộng thêm về bên phải: λx. MN có nghĩa là λx. (MN), không phải (λx. M) N.
- Dãy số trừu tượng được rút gọn: λx.λy.λz. N có thể là λxyz. N.
Biến tự do và ràng buộc
Toán tử λ kết nối hằng số của nó ở bất cứ đâu trong phần thân của phép trừu tượng. Các biến rơi vào phạm vi được gọi là bị ràng buộc. Trong biểu thức λ x. M, phần λ x thường được coi là chất kết dính. Như thể gợi ý rằng các biến trở thành một nhóm với việc thêm X x vào M. Tất cả các biến không ổn định khác được gọi là miễn phí.
Ví dụ, trong biểu thức λ y. x x y, y - ràng buộc không vĩnh viễn và x - miễn phí. Và cũng cần lưu ý rằng biến được nhóm theo phần trừu tượng "gần nhất" của nó. Trong ví dụ sau, nghiệm giải tích lambda được biểu diễn bằng một lần xuất hiện duy nhất của x, liên quan đến số hạng thứ hai:
λ x. y (λ x. z x)
Tập hợp các biến tự do M được ký hiệu là FV (M) và được định nghĩa bằng đệ quy trên cấu trúc của các số hạng như sau:
- FV (x)={x}, trong đó x là một biến.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Một công thức không chứa các biến tự do được gọi là đóng. Biểu thức lambda đóng còn được gọi là tổ hợp và tương đương với các thuật ngữ trong logic tổ hợp.
Viết tắt
Ý nghĩa của các biểu thức lambda được xác định bởi cách chúng có thể được rút ngắn.
Có ba kiểu cắt:
- α-biến đổi: thay đổi các biến bị ràng buộc (alpha).
- β-Reduce: áp dụng các hàm cho các đối số của chúng (beta).
- η-biến đổi: bao hàm khái niệm về tính mở rộng.
Đây cũng làchúng ta đang nói về sự tương đương kết quả: hai biểu thức là tương đương β nếu chúng có thể được biến đổi β thành cùng một thành phần và tương đương α / η được định nghĩa tương tự.
Thuật ngữ redx, viết tắt của doanh thu có thể giảm, đề cập đến các chủ đề phụ có thể được giảm theo một trong các quy tắc. Phép tính Lambda cho hình nộm, ví dụ:
(λ x. M) N là một số dư beta trong biểu thức thay thế N bằng x trong M. Thành phần mà một số dư giảm xuống được gọi là tập bớt của nó. Giảm (λ x. M) N là M [x:=N].
Nếu x không tự do trong M thì λ x. M x cũng em-REDEX với bộ điều chỉnh M.
α-biến đổi
Đổi tên alpha cho phép bạn thay đổi tên của các biến bị ràng buộc. Ví dụ, x. x có thể cho λ y. y. Các thuật ngữ chỉ khác nhau về biến đổi alpha được cho là tương đương α. Thông thường, khi sử dụng phép tính lambda, các giá trị tương đương α được coi là tương hỗ.
Các quy tắc chính xác để chuyển đổi alpha không hoàn toàn tầm thường. Đầu tiên, với sự trừu tượng này, chỉ những biến được liên kết với cùng một hệ thống mới được đổi tên. Ví dụ, biến đổi alpha λ x.λ x. x có thể dẫn đến λ y.λ x. x, nhưng điều này có thể không dẫn đến λy.λx.y Giá trị thứ hai có nghĩa khác với ý nghĩa ban đầu. Điều này tương tự với khái niệm về lập trình tạo bóng thay đổi.
Thứ hai, một phép biến đổi alpha không thể thực hiện được nếu nó dẫn đến việc bị bắt bởi một phép trừu tượng khác không vĩnh viễn. Ví dụ: nếu bạn thay x bằng y trong λ x.λ y. x, sau đó bạn có thể nhận đượcλy.λy. u, không giống nhau chút nào.
Trong các ngôn ngữ lập trình có phạm vi tĩnh, chuyển đổi alpha có thể được sử dụng để đơn giản hóa việc phân giải tên. Đồng thời, hãy cẩn thận để khái niệm về một biến không che dấu chỉ định trong vùng chứa.
Trong ký hiệu chỉ mục De Bruyne, hai thuật ngữ tương đương alpha bất kỳ đều giống nhau về mặt cú pháp.
Thay
Các thay đổi được viết bởi E [V:=R] là quá trình thay thế tất cả các lần xuất hiện tự do của biến V trong biểu thức E với doanh thu R. Sự thay thế theo λ được xác định bởi lambda của đệ quy tính toán trên cấu trúc khái niệm như sau (lưu ý: x và y - chỉ các biến, và M và N - bất kỳ biểu thức λ nào).
x [x:=N] ≡ N
y [x:=N] ≡ y nếu x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) nếu x ≠ y, với điều kiện là y ∉ FV (N).
Để thay thế thành một trừu tượng lambda, đôi khi cần phải biến đổi α-một biểu thức. Ví dụ: không đúng khi (λ x. Y) [y:=x] dẫn đến (λ x. X) vì x thay thế lẽ ra là tự do, nhưng cuối cùng lại bị ràng buộc. Thay thế đúng trong trường hợp này là (λ z. X) lên đến tương đương α. Lưu ý rằng phép thay thế được xác định duy nhất cho đến lambda.
β-giảm
Giảm beta phản ánh ý tưởng áp dụng một chức năng. Beta-Reduce được định nghĩa trong các thuật ngữthay thế: ((X V. E) E ') là E [V:=E'].
Ví dụ: giả sử một số mã hóa 2, 7, ×, có sự khử β sau: ((λ n. N × 2) 7) → 7 × 2.
Giảm beta có thể được xem giống như khái niệm về khả năng giảm cục bộ theo suy luận tự nhiên thông qua phép đẳng cấu Curry-Howard.
η-biến đổi
Việc chuyển đổi này thể hiện ý tưởng về tính mở rộng, trong ngữ cảnh này là hai hàm bằng nhau khi chúng cho cùng một kết quả cho tất cả các đối số. Chuyển đổi này trao đổi giữa λ x. (F x) và f bất cứ khi nào x có vẻ không rảnh trong f.
Hành động này có thể được coi là giống như khái niệm về tính hoàn chỉnh cục bộ trong suy luận tự nhiên thông qua phép đẳng cấu Curry-Howard.
Dạng bình thường và dạng hợp nhất
Đối với phép tính lambda không có kiểu, quy tắc khử β thường không chuẩn hóa mạnh cũng không yếu.
Tuy nhiên, có thể chỉ ra rằng phép khử β hợp nhất khi chạy trước phép biến đổi α (tức là hai dạng thông thường có thể được coi là bằng nhau nếu có thể thực hiện phép chuyển đổi α từ dạng này sang dạng khác).
Do đó, cả các điều khoản chuẩn hóa mạnh và điều chỉnh yếu các điều khoản đều có một dạng chuẩn duy nhất. Đối với các điều khoản đầu tiên, mọi chiến lược giảm thiểu đều được đảm bảo dẫn đến cấu hình điển hình. Trong khi đối với các điều kiện bình thường hóa yếu, một số chiến lược giảm có thể không tìm thấy nó.
Phương pháp lập trình bổ sung
Có rất nhiều thành ngữ sáng tạo cho phép tính lambda. Nhiều người trong số họ ban đầu được phát triển trong bối cảnh sử dụng các hệ thống làm cơ sở cho ngữ nghĩa của một ngôn ngữ lập trình, áp dụng chúng một cách hiệu quả như một cấu trúc cấp thấp. Vì một số kiểu bao gồm phép tính lambda (hoặc một cái gì đó rất giống) dưới dạng một đoạn mã, các kỹ thuật này cũng được sử dụng trong sáng tạo thực tế, nhưng sau đó có thể bị coi là tối nghĩa hoặc xa lạ.
Hằng số được đặt tên
Trong giải tích lambda, một thư viện có dạng một tập hợp các hàm đã được xác định trước đó, trong đó các số hạng chỉ là các hằng số cụ thể. Giải tích thuần túy không có khái niệm về các bất biến được đặt tên vì tất cả các thuật ngữ lambda nguyên tử đều là các biến. Nhưng chúng cũng có thể được bắt chước bằng cách lấy biến có thể thay đổi làm tên của hằng số, sử dụng trừu tượng lambda để liên kết biến động đó trong phần thân và áp dụng tính trừu tượng đó vào định nghĩa dự định. Vì vậy, nếu bạn sử dụng f để biểu diễn M trong N, bạn có thể nói
(λ f. N) M.
Các tác giả thường đưa ra một khái niệm cú pháp như let để cho phép mọi thứ được viết theo cách trực quan hơn.
f=M đến N
Bằng cách xâu chuỗi các định nghĩa như vậy, người ta có thể viết một "chương trình" giải tích lambda dưới dạng không hoặc nhiều định nghĩa hàm theo sau bởi một thành viên lambda duy nhất, sử dụng các định nghĩa đó tạo nên phần lớn chương trình.
Một hạn chế đáng chú ý của phép này là tên f không được định nghĩa trong M,vì M nằm ngoài phạm vi ràng buộc của trừu tượng lambda f. Điều này có nghĩa là một thuộc tính hàm đệ quy không thể được sử dụng như M với let. Cú pháp letrec nâng cao hơn, cho phép bạn viết các định nghĩa hàm đệ quy theo kiểu này, thay vào đó sử dụng các tổ hợp điểm cố định.
Tương tự in
Loại này là một chủ nghĩa hình thức được đánh máy sử dụng một biểu tượng để đại diện cho một hàm ẩn danh trừu tượng. Trong ngữ cảnh này, các kiểu thường là các đối tượng có bản chất cú pháp được gán cho các điều khoản lambda. Bản chất chính xác phụ thuộc vào phép tính được đề cập. Từ một quan điểm nào đó, LI có định kiểu có thể được coi là sự sàng lọc của LI không định kiểu. Nhưng mặt khác, chúng cũng có thể được coi là một lý thuyết cơ bản hơn và phép tính lambda không có kiểu là một trường hợp đặc biệt chỉ có một loại.
Typed LI là nền tảng của các ngôn ngữ lập trình và là xương sống của các ngôn ngữ chức năng như ML và Haskell. Và, gián tiếp hơn, các phong cách sáng tạo bắt buộc. Gõ lambda Calculi đóng một vai trò quan trọng trong việc phát triển các hệ thống kiểu cho các ngôn ngữ lập trình. Ở đây, khả năng đánh máy thường nắm bắt các thuộc tính mong muốn của chương trình, chẳng hạn, nó sẽ không gây ra vi phạm quyền truy cập bộ nhớ.
Tính toán lambda được nhập có liên quan chặt chẽ đến logic toán học và lý thuyết chứng minh thông qua phép đẳng cấu Curry – Howard, và có thể được coi là ngôn ngữ nội bộ của các lớp danh mục, chẳng hạn,đơn giản là phong cách đóng cửa Descartes.
