Bộ kết hợp "kiểu Y" hai lớp. Điều này có phổ biến không? Điều này có một tên chính thức?

Question

Tôi đã xem xét cách ngôn ngữ cấm sử dụng trước và không có các ô có thể thay đổi (không có số set! hoặc setq) có thể cung cấp đệ quy. Tôi dĩ nhiên chạy băng qua combinator Y và bạn bè, ví dụ (nổi tiếng khét tiếng?):

• http://www.ece.uc.edu/~franco/C511/html/Scheme/ycomb.html
• http://okmij.org/ftp/Computation/fixed-point-combinators.html
• http://www.angelfire.com/tx4/cus/combinator/birds.html
• http://en.wikipedia.org/wiki/Fixed-point_combinator

Khi tôi đến thực hiện " letrec "ngữ nghĩa trong phong cách này (có nghĩa là, cho phép một biến địa phương được định nghĩa sao cho nó có thể là một hàm đệ quy, trong đó dưới sự che chở nó không bao giờ ám chỉ tên riêng của mình), các combinator tôi đã kết thúc bằng văn bản trông như thế này:

Y_letrec = λf . (λx.x x) (λs . (λa . (f ((λx.x x) s)) a)) 

Hoặc, bao thanh toán ra U combinator:

U = λx.x x 
Y_letrec = λf . U (λs . (λa . (f (U s)) a)) 

đọc này như: Y_letrec là một chức năng mà phải mất một đến chức năng được đệ trình lại f. f phải là một hàm đối số duy nhất chấp nhận s, trong đó s là hàm rằng f có thể gọi để đạt được tự đệ quy. f dự kiến ​​sẽ xác định và trả lại một hàm "bên trong" thực hiện thao tác "thực". Hàm bên trong đó chấp nhận đối số a (hoặc trong trường hợp chung là danh sách đối số, nhưng không thể được biểu thị theo ký pháp truyền thống). Kết quả của việc gọi Y_letrec là kết quả của việc gọi số f và được coi là chức năng "bên trong", sẵn sàng để được gọi.

Lý do tôi thiết lập những điều theo cách này là vì vậy mà tôi có thể sử dụng các hình thức cây phân tích cú pháp của to-be-recursed chức năng trực tiếp, mà không sửa đổi, chỉ đơn thuần gói thêm một lớp chức năng xung quanh nó trong chuyển đổi khi xử lý letrec . Ví dụ: nếu mã gốc là:

(letrec ((foo (lambda (a) (foo (cdr a)))))) 

sau đó các hình thức chuyển đổi sẽ là dọc theo dòng:

(define foo (Y_letrec (lambda (foo) (lambda (a) (foo (cdr a)))))) 

Lưu ý rằng các cơ quan chức năng bên trong là giống hệt nhau giữa hai người.

Câu hỏi của tôi là:

• là chức năng Y_letrec tôi thường được sử dụng?
• Nó có tên được thiết lập tốt không?

Lưu ý: Liên kết đầu tiên ở trên đề cập đến chức năng tương tự (trong "bước 5") là "bộ kết hợp Y theo đơn đặt hàng" mặc dù tôi đang gặp khó khăn khi tìm nguồn có thẩm quyền cho việc đặt tên đó.

CẬP NHẬT 28 tháng tư năm 2013:

tôi nhận ra rằng Y_letrec như đã định nghĩa ở trên là rất gần với nhưng không giống với các combinator Z theo quy định tại Wikipedia. Mỗi Wikipedia, bộ kết hợp Z và "bộ kết hợp Y theo giá trị" đều giống nhau, và có vẻ như đó thực sự là thứ có thể được gọi chung là "bộ kết hợp Y theo đơn đặt hàng".

Vì vậy, những gì tôi có ở trên là không giống như bộ kết hợp Y theo đơn đặt hàng thường được viết, nhưng gần như chắc chắn là một cảm giác mà chúng liên quan. Đây là cách tôi đã so sánh:

Bắt đầu với:

Y_letrec = λf . (λx.x x) (λs . (λa . (f ((λx.x x) s)) a)) 

Áp dụng U bên trong:

Y_letrec = λf . (λx.x x) (λs . (λa . (f (s s)) a)) 

Áp dụng U ngoài:

Y_letrec = λf . (λs . (λa . (f (s s)) a)) (λs . (λa . (f (s s)) a)) 

Rename để phù hợp với định nghĩa của Wikipedia của bộ tổ hợp Z:

Y_letrec = λf . (λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v)) 

Hãy so sánh này đến Z combinator Wikipedia:

Z  = λf . (λx . f (λv . ((x x) v))) (λx . f (λv . ((x x) v))) 

Sự khác biệt nổi bật là nơi mà các chức năng f đang được áp dụng. Nó có quan trọng không? Hai hàm này có tương đương với bất chấp sự khác biệt này không?

Answer 1

Có, nó là một bộ kết hợp Y theo yêu cầu. Sử dụng chữ U bên trong nó là hoàn toàn OK, tôi cũng làm như vậy (xem fixed point combinator in lisp). Cho dù việc sử dụng U để rút ngắn mã có tên hay không, tôi không nghĩ như vậy. Nó chỉ là một ứng dụng của một lambda hạn, và có, nó làm cho nó rõ ràng hơn IMO quá.

Tên có gì, là eta-conversion, được sử dụng trong mã của bạn để trì hoãn việc đánh giá theo thứ tự ứng dụng, trong đó các giá trị của đối số phải được biết trước ứng dụng chức năng.

Với U áp dụng thông qua và thông qua và eta-giảm thực hiện trên mã của bạn ((λa.(f (s s)) a) ==>f (s s)), nó trở nên quen thuộc bình thường bậc Y Combinator - tức là như vậy mà làm việc được đánh giá bình thường theo đơn đặt hàng, nơi tranh cãi giá trị không được yêu cầu trước khi ứng dụng chức năng, mà có thể kết thúc không cần họ (hoặc một số trong số họ) sau khi tất cả:

Y = λf . (λs.f (s s)) (λs.f (s s)) 

BTW sự trì hoãn có thể được áp dụng theo cách hơi khác nhau,

Y_ = λf . (λx.x x) (λs.f (λa.(s s) a)) 

cũng hoạt động theo các quy tắc đánh giá đơn đặt hàng.

Sự khác biệt là gì? chúng ta hãy so sánh các trình tự giảm. Phiên bản của bạn,

Y_ = λf . (λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v)) 

((Y_ f) a) = 
    = ((λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))) a 
    = (λv . (f (x x)) v) a { x := (λx . (λv . (f (x x)) v)) } 
    = (f (x x)) a 
    = | ; here (f (x x)) application must be evaluated, so 
    | ; the value of (x x) is first determined 
    | (x x) 
    | = ((λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))) 
    | = (λv . (f (x x)) v)  { x := (λx . (λv . (f (x x)) v)) } 

và tại đây f được nhập. Vì vậy, ở đây, chức năng được xử lý tốt f nhận được đối số đầu tiên của nó và nó không được phép làm bất cứ điều gì với nó. Vì vậy, có lẽ cả hai là chính xác tương đương sau khi tất cả.Nhưng thực sự, minutia của định nghĩa biểu thức lambda không quan trọng khi nói đến việc thực hiện thực tế, bởi vì ngôn ngữ thực hiện thực sự sẽ có con trỏ và chúng tôi sẽ thao tác chúng để trỏ đúng vào nội dung biểu hiện có chứa, chứ không phải vào bản sao của nó. Tính toán lambda được thực hiện bằng bút chì và giấy sau khi tất cả, như sao chép văn bản và thay thế. Y combinator trong tính toán lambda chỉ giả lập đệ quy. Đúng đệ quy là đúng tự tham khảo; không phải nhận bản sao bằng bản thân, thông qua tự ứng dụng (tuy nhiên thông minh).

TL; DR: mặc dù ngôn ngữ được xác định có thể không có các công cụ thú vị như gán và con trỏ bình đẳng, ngôn ngữ mà chúng tôi xác định chắc chắn sẽ có, vì chúng tôi cần chúng cho hiệu quả. Ít nhất, việc triển khai của chúng tôi sẽ có, dưới mui xe.

xem thêm: fixed point combinator in lisp, đặc biệt. In Scheme, how do you use lambda to create a recursive function?.