Lambda biểu hiện tính toán chức năng triển khai ứng dụng

Question

Tôi chỉ tìm thấy sự biểu hiện phép tính lambda sau:

(((λ f . (λ x . (f x))) (λ a . a)) (λ b . b)) 

Vì vậy, đó là một chức năng mà có một đối số f và trả về một chức năng mà có một đối số x và mang lại kết quả của x áp dụng cho f. Kết quả của biểu thức trên sẽ là (λ b. B).

Điều này nhắc tôi về ứng dụng một phần và currying, tuy nhiên ứng dụng chức năng "trong ra ngoài" (f x) là những gì piqued quan tâm của tôi.

Có ý nghĩa lý thuyết sâu sắc hơn đối với biểu thức đó không?

Answer 1

Biểu thức này thực sự khá thú vị, mặc dù đây là một thao tác khá đơn giản. Sau khi tất cả, chức năng chỉ là ứng dụng chức năng, phải không?

Đó là nơi mọi thứ trở nên thú vị. Trong phép tính lambda, ứng dụng là một quy tắc cú pháp, chỉ đơn giản là nói "Nếu f là một biểu thức và x là một biểu thức, thì f x là một biểu thức". Ứng dụng không phải là chức năng của bất kỳ loại nào. Điều này là không may: kể từ khi tính toán lambda là tất cả về chức năng, nó sẽ hút phải dựa rất nhiều vào một cái gì đó mà không phải là một chức năng!

Ví dụ của bạn là một loại biện pháp khắc phục cho điều này. Mặc dù chúng ta không thể loại bỏ ứng dụng, nhưng ít nhất chúng ta có thể định nghĩa một đối tác cho ứng dụng. Đối tác đó là hàm lambda (λ f . (λ x . (f x))) (hoặc tự nhiên hơn, λfx.f x). Điều này là một chức năng, vì vậy chúng tôi có thể giải thích về nó và sử dụng nó giống như bất kỳ chức năng nào khác. Chúng ta có thể chuyển nó thành các đối số cho các hàm khác, hoặc nó có thể được sử dụng như là kết quả của một hàm. Đột nhiên, ứng dụng chức năng đã trở nên dễ sử dụng hơn nhiều.

Đó là tất cả những gì tôi có được khi tính toán lambda đi, nhưng chức năng này, và những người khác thích nó, cũng khá hữu ích trong cuộc sống thực. Trong ngôn ngữ lập trình chức năng F #, chức năng này thậm chí có tên, "toán tử đường dẫn ngược", và chúng ta viết nó có toán tử infix <|. Vì vậy, thay thế cho việc viết f (x) trong đó x là một số biểu thức, chúng tôi có thể viết f <| x. Điều này là tốt đẹp vì nó thường có thể miễn phí cho chúng tôi bằng cách viết rất nhiều dấu ngoặc đơn gây phiền nhiễu. Điểm mấu chốt mà tôi đang cố gắng tạo ra ở đây là, mặc dù trong nháy mắt, ví dụ của bạn dường như là học thuật, hoặc có lẽ không phải là rất hữu ích, nó thực sự đã tìm thấy cách của nó thành một số ngôn ngữ lập trình chính thống.