Thống nhất bậc cao hơn

Question

Tôi đang làm việc trên một định lý lý thuyết bậc cao hơn, trong đó sự hợp nhất có vẻ là bài toán khó nhất.

Nếu thuật toán của Huet vẫn được coi là nhà nước-of-the-nghệ thuật, không ai có bất kỳ liên kết để giải thích của nó được viết để được hiểu bởi một lập trình viên chứ không phải là một nhà toán học?

Hoặc thậm chí bất kỳ ví dụ nào về vị trí hoạt động và thuật toán đơn đặt hàng thông thường không?

Answer 1

Nhà nước của nghệ thuật — có, cho đến nay như tôi biết tất cả các thuật toán nhiều hơn hoặc ít hơn có hình dạng giống như (tôi làm theo lý thuyết của chương trình logic, mặc dù chuyên môn của tôi là tiếp tuyến) cung cấp bạn cần đầy đủ bậc cao Huet của phù hợp: các vấn đề con như kết hợp thứ tự cao hơn (thống nhất trong đó một cụm từ được đóng), và phép tính mẫu của Dale Miller, có thể giải quyết được.

Lưu ý rằng thuật toán của Huet là tốt nhất theo nghĩa sau — nó giống như thuật toán bán quyết định, ở chỗ nó sẽ tìm thấy bộ lọc nếu chúng tồn tại, nhưng không đảm bảo chấm dứt nếu chúng không. Vì chúng ta biết rằng sự thống nhất bậc cao hơn (thực sự, sự thống nhất thứ hai) là không thể giải quyết được, bạn không thể làm tốt hơn thế.

Giải thích: Bốn chương đầu tiên của luận án tiến sĩ của Conal Elliott, Extensions and Applications of Higher-Order Unification phải phù hợp với hóa đơn. Đó là một phần nặng gần 80 trang, với một số lý thuyết loại dày đặc, nhưng nó có động lực tốt, và là tài khoản dễ đọc nhất mà tôi đã nhìn thấy.

Ví dụ: Thuật toán của Huet sẽ đưa ra hàng hóa cho ví dụ này: [X (o), Y (succ (0))]; điều cần thiết sẽ làm lúng túng thuật toán thống nhất bậc nhất.

Answer 2

Ví dụ về thống nhất bậc cao hơn (thực sự khớp thứ hai) là: f 3 == 3 + 3, trong đó == là modulo alpha, beta và eta-conversion (nhưng không gán bất kỳ ý nghĩa nào cho "+"). Có bốn giải pháp:

\ x -> x + x 
\ x -> x + 3 
\ x -> 3 + x 
\ x -> 3 + 3 

Ngược lại, thống nhất/khớp thứ tự sẽ không đưa ra giải pháp.

HOU là rất tiện dụng khi sử dụng với HOAS (bậc cao cú pháp trừu tượng), để mã hóa ngôn ngữ với biến ràng buộc trong khi tránh sự phức tạp của chụp biến, vv

tiếp xúc đầu tiên của tôi đến chủ đề là giấy "Chứng minh và áp dụng các chuyển đổi chương trình được thể hiện với các mẫu thứ tự thứ hai "của Gerard Huet và Bernard Lang. Khi tôi nhớ lại, bài báo này đã được "viết để được hiểu bởi một lập trình viên". Và một khi bạn hiểu được sự khớp lệnh thứ hai, HOU không còn xa hơn nữa. Một kết quả chính của Huet là trường hợp linh hoạt/linh hoạt (các biến làm người đứng đầu của một thuật ngữ và trường hợp duy nhất không xuất hiện trong kết hợp) luôn luôn có thể giải quyết được.

Answer 3

Tôi sẽ thêm vào danh sách đọc một chương trong quyển 2 của Sổ tay về lý do tự động. Chương này có lẽ là dễ tiếp cận hơn đối với người mới bắt đầu và kết thúc bằng λΠ-calculus, nơi Giấy Conal Elliott bắt đầu.

Một bản thảo được tìm thấy ở đây:

bậc cao Thống Nhất và Matching
Gilles Dowek, 2001
http://www.lsv.fr/~dowek/Publi/unification.ps

giấy

Conal Elliott là chính thức hơn và concerntrated trên một biến thể, và cũng giới thiệu một λΠΣ-calculus cuối cùng, mà cũng có tổng hợp các loại bên cạnh các loại sản phẩm.

Bye

Answer 4

Ngoài ra còn có 1.993 giấy Functional Unification of Higher-Order Patterns (chỉ có 11 trang, 4 trong số đó là thư mục và phụ lục code) Tobias Nipkow của. Bản tóm tắt:

Sự phát triển hoàn toàn của một thuật toán thống nhất cho cái gọi là mẫu bậc cao, một lớp con của $ \ lambda $ -terms, được trình bày. Điểm khởi đầu là một công thức thống nhất bằng cách chuyển đổi, kết quả là một chương trình chức năng thực thi trực tiếp. Trong bước phát triển cuối cùng, kết quả được điều chỉnh theo $ \ lambda $ -terms trong ký hiệu de Bruijn. Các thuật toán hoạt động cho cả các thuật ngữ đơn giản và không được nhập.