tôi đang học phép tính lambda nhưng tôi không thể dường như hiểu được mã hóa cho số 0.Chữ số của Giáo hội: cách mã hóa số không trong phép tính lambda?
như thế nào là "chức năng mà mất trong một chức năng và giá trị thứ hai và áp dụng các chức năng zero lần trên lập luận" một số không? Có cách nào khác để mã hóa không? Bất cứ ai ở đây có thể giúp tôi mã hóa 0?
A "chức năng mà mất trong một chức năng và giá trị thứ hai và áp dụng các chức năng zero lần trên lập luận" là, tất nhiên, không phải bằng không. Đó là mã hóa bằng không. Khi bạn đối phó với phép tính lambda đơn giản, bạn phải mã hóa các số (cũng như các kiểu nguyên thủy khác) theo một cách nào đó và có một vài yêu cầu được quy định cho từng loại này. Ví dụ: một yêu cầu cho số tự nhiên là có thể thêm 1 vào một số cho sẵn và một số khác có thể phân biệt số không với số lớn hơn (nếu bạn muốn biết thêm, hãy tìm "Số học Peano"). Các mã hóa phổ biến mà Dario trích dẫn cung cấp cho bạn hai điều này, và nó cũng đại diện cho một số nguyên N bởi một hàm thực hiện điều gì đó (được mã hóa như đối số f) N lần - đó là một cách tự nhiên để sử dụng naturals.
Có mã hóa khác có thể - ví dụ, khi bạn có thể đại diện cho danh sách, bạn có thể đại diện cho N dưới dạng danh sách N mục. Những mã hóa này có ưu và khuyết điểm của chúng, nhưng cái trên là cái phổ biến nhất.
Xem wikipedia:
0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x
Nếu bạn học Lambda Calculus, có thể bạn đã biết rằng λxy.y arg1 arg2 * * sẽ giảm tới arg2, kể từ khi x được thay thế bằng gì, và phần còn lại (λy.y) là bản sắc chức năng.
Bạn có thể viết số không theo nhiều cách khác (ví dụ: đưa ra một quy ước khác), nhưng có lý do chính đáng để sử dụng λxy.y. Ví dụ, bạn muốn số không là số tự nhiên đầu tiên, do đó nếu bạn áp dụng hàm kế thừa cho nó, bạn nhận được 1, 2, 3 vv. Với hàm λabc.b (abc), bạn nhận được λxy.x (y)), λxy.x (x (y)), λxy.x (x (x (y))), nói cách khác, bạn nhận được một hệ thống số nguyên.
Ngoài ra, bạn muốn không là phần tử trung tính đối với phần bổ sung. Với chức năng kế nhiệm của chúng tôi S: = λabc.b (abc), chúng ta có thể xác định n + * m * như n S m, nghĩa là, n lần so với áp dụng các chức năng kế để m. Không λxy.y của chúng tôi thỏa mãn điều này, cả 0 S m và m S 0 giảm xuống m.
Đây là một câu hỏi liên quan mà tôi đã hỏi trong các nhóm google: Giả sử tôi có một hàm f. Làm thế nào để tôi cho thấy rằng điều này chuyển thành một số tự nhiên 0? Tôi cần những chức năng nào khác để suy ra rằng hàm f của tôi hoạt động giống như 0? – unj2
Nếu bạn muốn chứng minh rằng hàm 'f' bằng 0 theo mã hóa thông thường, bạn cần hiển thị rằng đối với tất cả' g' (f g x) == x. Bạn không cần phải biết gì ngoài điều này. –