Lambda Calculus Reduction steps

Question

Tôi đang nghiên cứu Lambda Calculus và tôi bị kẹt ở Giảm .... Bất cứ ai có thể giải thích các loại giảm với ví dụ này, đặc biệt là giảm beta theo cách đơn giản nhất có thể. Cũng sẽ không nhớ một hướng dẫn dễ hiểu.

(λxyz .xyz)(λx .xx)(λx .x)x 

Answer 1

Lambda calculus

Lambda calculus có một cách để vun vút vào rất nhiều bước, làm cho vấn đề giải quyết tẻ nhạt, và nó có thể trông thật nghiêm túc, nhưng nó không phải là thực sự là xấu. Trong tính toán lambda, chúng chỉ là lambdas, và tất cả những gì bạn có thể làm với chúng là thay thế. Lambdas giống như một hàm hoặc phương thức nếu bạn đã quen với lập trình, chúng là các hàm lấy hàm làm đầu vào và trả về một hàm mới làm đầu ra.

Về cơ bản có quá trình hai và một nửa trong phép tính lambda:

1) Chuyển đổi Alpha - nếu bạn đang áp dụng hai biểu thức lambda với tên biến tương tự bên trong, bạn thay đổi một trong số họ để một tên biến mới. Ví dụ (λx.xx) (λx.x) trở thành một cái gì đó như (λx.xx) (λy.y) hoặc (λx.xx) (λx'.x ') sau khi giảm. Kết quả tương đương với những gì bạn bắt đầu với, chỉ với các tên biến khác nhau.

2) Giảm Beta - Về cơ bản chỉ thay thế. Đây là quá trình gọi biểu thức lambda với đầu vào và nhận đầu ra. Một biểu thức lambda giống như một hàm, bạn gọi hàm bằng cách thay thế đầu vào trong suốt biểu thức. Lấy (λx.xy) z, nửa sau của (λx.xy), mọi thứ sau dấu chấm, là đầu ra, bạn giữ đầu ra, nhưng thay thế biến (được đặt tên trước dấu chấm) với đầu vào được cung cấp. z là đầu vào, x là tên thông số, xy là đầu ra. Tìm tất cả các lần xuất hiện của tham số trong đầu ra và thay thế chúng bằng đầu vào và đó là những gì nó giảm xuống, vì vậy (λx.xy)z =>xy với z được thay thế cho x, là zy.

2.5) Chuyển đổi Eta/giảm Eta - Đây là trường hợp giảm đặc biệt, tôi chỉ gọi một nửa quy trình, vì đó là giảm Beta, kinda, như trong về mặt kỹ thuật, không phải là. Bạn có thể thấy nó được viết trên wikipedia hoặc trong sách giáo khoa là "Chuyển đổi Eta chuyển đổi giữa λx. (F x) và f bất cứ khi nào x không xuất hiện tự do trong f", âm thanh thực sự gây nhầm lẫn. Tất cả điều đó thực sự có nghĩa là λx. (F x) = f nếu f không sử dụng x. nếu nó thực sự có ý nghĩa hoàn chỉnh nhưng được hiển thị tốt hơn thông qua một ví dụ. Hãy xem xét (λx. (Λy.yy) x), điều này tương đương với việc giảm eta thành (λy.yy), vì f = (λy.yy), không có x trong đó, bạn có thể hiển thị điều này bằng cách giảm nó , vì nó sẽ giải quyết (λx.xx), được quan sát giống nhau.Bạn cho biết tập trung vào giảm beta, và vì vậy tôi sẽ không để thảo luận về chuyển đổi eta trong các chi tiết nó xứng đáng, nhưng rất nhiều người đã gửi đi của họ vào nó on the cs theory stack exchange

Trên Notation về giảm Beta:

tôi 'm sẽ sử dụng các ký hiệu sau đây để thay thế đầu vào cung cấp vào đầu ra:

(λ param . output)input =>output [param := input] =>result

điều này có nghĩa chúng ta thay thế xuất hiện của param trong đầu ra, và đó là những gì nó làm giảm xuống

Ví dụ:

(λx.xy)z

= (xy)[x:=z]

= (zy)

= zy

lý thuyết Đủ rồi, chúng ta hãy giải quyết việc này. Lambda Calculus rất hay.

Sự cố bạn đã đưa ra có thể được giải quyết chỉ với Chuyển đổi Alpha và Giảm Beta, Đừng bị nản lòng bởi quá trình này diễn ra trong bao lâu. Nó khá dài, không nghi ngờ gì, nhưng không có bước giải quyết nó là thực sự khó khăn.

(λxyz.xyz) (λx.xx) (λx.x) x

= (((λxyz.xyz) (λx.xx)) (λx.x)) x - Hãy thêm dấu ngoặc trong "Thứ tự bình thường", liên kết bên trái, abc giảm xuống ((ab) c), trong đó b được áp dụng cho a và c được áp dụng cho kết quả đó

= (((λxyz.xyz) (λx .xx)) (λx.x)) x - Chọn ứng dụng lồng nhau sâu nhất và giảm ứng dụng đầu tiên.

Phần in đậm giảm như:

(λxyz.xyz) (λx.xx)

= (λx.λyz.xyz) (λx.xx) - có nghĩa là điều tương tự, nhưng chúng tôi kéo ra thông số đầu tiên vì chúng ta sẽ giảm nó đi và vì vậy tôi muốn nó rõ ràng

= (λx.λyz.xyz) (λx'.x'x ') - Chuyển đổi Alpha, một số người dính vào mới các chữ cái, nhưng tôi thích các số phụ ở cuối hoặc `s, một trong hai cách là tốt. Bởi vì cả hai biểu thức sử dụng tham số x, chúng ta phải đổi tên chúng thành một phía, bởi vì hai X là các biến cục bộ, và do đó không cần phải đại diện cho cùng một thứ.

= (λyz.xyz) [x: = λx'.x'x '] - Ký hiệu để giảm beta, chúng tôi xóa thông số đầu tiên và thay thế các lần xuất hiện trong đầu ra với những gì đang được áp dụng [a: = b] biểu thị rằng a được thay thế bằng b.

= (λyz. (Λx'.x'x ') yz) - Giảm thực tế, chúng tôi thay thế sự xuất hiện của x bằng biểu thức lambda được cung cấp.

= (λyz. ((λx '.x'x ') y) z) - Thứ tự bình thường cho dấu ngoặc đơn một lần nữa, và xem, một ứng dụng khác để giảm, lần này y được áp dụng cho (λx .x x`), vì vậy hãy giảm ngay bây giờ

= (λyz ((x'x ') [x': = y]) z) - Đặt ký hiệu này thành ký hiệu để giảm beta.

= (λyz. (yy) z) - chúng tôi trao đổi hai lần xuất hiện của x'x 'cho Y và điều này hiện đã được giảm hoàn toàn.

Thêm này trở lại vào biểu hiện ban đầu:

(((λxyz.xyz) (λx.xx)) (λx.x)) x

= ((λyz (yy). z) (λx.x)) x - Đây không phải là mới, chỉ cần đặt những gì chúng tôi đã tìm thấy trước đó trở lại.

= ((λyz. (yy) z) (λx.x)) x - Lấy ứng dụng lồng nhau sâu nhất, nó là (λx.x) được áp dụng cho (λyz. (yy) z)

Chúng tôi sẽ giải quyết việc này ra riêng một lần nữa:

(. Λyz (yy) z) (λx.x)

= (λy.λz. (yy) z) (λx.x) - Chỉ cần đưa thông số đầu tiên ra để làm sáng tỏ.

= (λz. (Yy) z) [y: = (λx.x)] - Đưa vào ký hiệu giảm beta, chúng tôi bật tham số đầu tiên và lưu ý rằng Y sẽ được chuyển sang (λx.x)

= (λz ((λx.x) (λx.x)) z.) - việc giảm thực tế/thay thế, phần in đậm bây giờ có thể được giảm

= (λz ((x.) [x: = λx.x]) z) - Hy vọng rằng bạn có được hình ảnh ngay bây giờ, chúng tôi đang bắt đầu giảm beta (λx.x) (λx.x) bằng cách đặt nó vào biểu mẫu (x) [x: = λx.x]

= (λz. ((λx.x)) z) - Và có sự thay thế

= (λz. (λx.x) z) - Làm sạch dấu ngoặc đơn thừa và chúng tôi tìm thấy gì, nhưng một ứng dụng khác để xử lý

= (λz. (X) [x: = z]) - Bật x tham số, đưa vào ký hiệu

= (λz (z).) - Thực hiện các thay

= (λz.z) - Làm sạch ra khỏi quá mức ngoặc

đặt nó trở lại vào biểu hiện chính:

((. Λyz (yy) z) (λx.x)) x

= ((λz.z)) x - Điền vào những gì chúng tôi đã chứng minh ở trên

= (λz.z) x - làm sạch tắt quá nhiều dấu ngoặc đơn, điều này bây giờ được giảm xuống một ứng dụng cuối cùng, x áp dụng cho (λz.z)

= (z) [z: = x] - giảm beta, đưa vào ký hiệu

= (x) - làm cho việc thay thế

= x - sạch khỏi ngoặc quá

Vì vậy, vâng. Câu trả lời là x, nó giảm xuống chỉ hấp dẫn.