Lập trình hàm - Giải tích Lambda

Giải tích Lambda là một khung được phát triển bởi Alonzo Church vào những năm 1930 để nghiên cứu các phép tính với các hàm.

Function creation - Church giới thiệu ký hiệu λx.Eđể biểu thị một hàm trong đó 'x' là đối số chính thức và 'E' là phần thân của hàm. Các hàm này có thể không có tên và đối số đơn lẻ.
Function application - Church đã sử dụng ký hiệu E₁.E₂ để biểu thị ứng dụng của chức năng E₁ đối số thực tế E₂. Và tất cả các hàm đều nằm trên một đối số.

Cú pháp của Lambda Calculus

Phép tính Lamdba bao gồm ba loại biểu thức khác nhau, tức là

E :: = x (biến)

| E ₁ E ₂(ứng dụng chức năng)

| λx.E (tạo hàm)

Ở đâu λx.E được gọi là trừu tượng Lambda và E được gọi là biểu thức λ.

Giải tích lambda thuần túy không có chức năng cài sẵn. Chúng ta hãy đánh giá biểu thức sau:

(+ (* 5 6) (* 8 3))

Ở đây, chúng ta không thể bắt đầu bằng '+' vì nó chỉ hoạt động trên các con số. Có hai biểu thức rút gọn: (* 5 6) và (* 8 3).

Chúng ta có thể giảm một trong hai trước. Ví dụ -

(+ (* 5 6) (* 8 3)) 
(+ 30 (* 8 3)) 
(+ 30 24) 
= 54

Chúng ta cần một quy tắc rút gọn để xử lý λs

(λx . * 2 x) 4 
(* 2 4) 
= 8

Đây được gọi là quá trình khử β.

Tham số chính thức có thể được sử dụng nhiều lần -

(λx . + x x) 4 
(+ 4 4) 
= 8

Khi có nhiều điều khoản, chúng tôi có thể xử lý chúng như sau:

(λx . (λx . + (− x 1)) x 3) 9

Bên trong x thuộc về bên trong λ còn x thuộc ngoài cùng thuộc x ngoài cùng.

(λx . + (− x 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
= 11

Trong một biểu thức, mỗi lần xuất hiện của một biến là "tự do" (với λ) hoặc "bị ràng buộc" (với λ).

β-giảm của (λx . E) y thay thế mọi x điều đó xảy ra miễn phí trong E với y. Ví dụ -

Rút gọn alpha rất đơn giản và nó có thể được thực hiện mà không làm thay đổi ý nghĩa của biểu thức lambda.

λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x)

Ví dụ -

(λx . (λx . + (− x 1)) x 3) 9 
(λx . (λy . + (− y 1)) x 3) 9 
(λy . + (− y 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
11

Định lý Church-Rosser phát biểu như sau:

Nếu E1 ↔ E2, thì tồn tại một E sao cho E1 → E và E2 → E. "Giảm theo bất kỳ cách nào cuối cùng có thể tạo ra cùng một kết quả."
Nếu E1 → E2, và E2 là dạng chuẩn thì có sự giảm bậc bình thường của E1 thành E2. "Giảm bậc bình thường sẽ luôn tạo ra dạng bình thường, nếu tồn tại."