phép tính lambda: đi qua hai giá trị cho một tham số duy nhất mà không tách lạng bộ

Question

Tôi không thể hiểu tại sao việc giảm beta sau đây được cho phép trong untyped phép tính lambda:

(λx.x y) (u v) -> ((u v) y) 

Cụ thể là tôi không thể hiểu tại sao người ta có thể vượt qua hai tham số u và v vào một tham số x trong phần λx.x. Để cho phép những điều trên tôi không nên sử dụng currying và có hai tham số? Như thế này —

(λx.(λy.(x y))) (u v) 

Answer 1

đặc biệt Tôi không thể hiểu tại sao người ta có thể vượt qua hai tham số u và v

Bạn đang không đi qua hai tham số u và v. Bạn đang vượt qua (u v), là một giá trị hoặc thuật ngữ duy nhất: giá trị của u được áp dụng cho v.

Hãy so sánh điều này với số học bình thường: bạn có thể áp dụng một chức năng như sin đến một thuật ngữ hợp chất như sin(x + 1) vì x+1 biểu thị một giá trị duy nhất, mặc dù nó là việc áp dụng chức năng + để hai đối x và 1.